OAI/Analysis/LipschitzHilbert/Trees/SourceOriginalParentMarkedPath.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual source cell marks and local original-packet estimates supply the remaining hypotheses of the stopped-path theorem.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.originalParentMarkedPathBoundAt line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_original_parent_marked_path_bound line 134