OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalStoppedBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

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.physicalStoppedBoundAt line 24

    Source documentation

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

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