OAI/Analysis/LipschitzHilbert/Trees/SourceParentStoppedBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Parent-cone version of the stopped physical path estimate. The two literal physical reference events discharge the square and variation inputs of the stopped path estimate. The propagated unary residual and mass power estimates follow from the active mass path itself. The remaining local hypotheses concern marking and off-child amplitudes.

  1. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalParentStoppedBoundAt line 25

    Source documentation

    The exact physical stopped-path statement at one manuscript scale. Separating its dependent data from the eventual proof keeps elaboration local.

    def physicalParentStoppedBoundAt (q D Cmass qoff A_M L : ℝ) (Klocal Hlocal : ℕ) : Prop :=
…
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_physical_parent_stopped_bound line 125