SourceShiftedDrop.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The path mass at shifted block endpoints is set to zero as soon as the distinguished top becomes ineligible, even if other tops continue. The actual drop has the same factor-two reference-window comparison, including this terminal block.

def OAI.LipschitzHilbert.AngularGrid.shiftedPathMass line 17
theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathMass_nonneg line 24
theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathMass_pos line 34
theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathMass_le_total line 43
theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathMass_antitone line 54
theorem OAI.LipschitzHilbert.AngularGrid.shiftedPathDrop_terminal line 69

theorem OAI.LipschitzHilbert.AngularGrid.source_shifted_path_drop_motion line 85

Source documentation

Exact shifted source blocks satisfy the drop comparison used in the stopped error budget. A final block with no eligible path child has drop one at both endpoints and needs no fictitious child top.

theorem source_shifted_path_drop_motion {ι : Type*} {K : ℕ}
    (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox)
    (w B Kw D : ℝ) (hw : 0 < w) (hB : 1 ≤ B) (hKw : 0 < Kw) (hD : 0 ≤ D)
    (hwidth : ∀ t ∈ tops, B^2*w ≤ (T t).width)
    (hK : 0 < K) (σ : Fin K) (j : ℕ) (top : ι) (htop : top ∈ tops)
    (he : g.eligible (g.rootWidth/B^2) (w/(T top).length) (ShiftedBlocks.endpoint σ j))
    (h : ℕ) (hbase : h ≤ ShiftedBlocks.endpoint σ j)
    (sR : ℝ) (hs : g.index h (T top).slope = g.index h sR)
    (hblock : g.width h ≤ B*g.width (ShiftedBlocks.endpoint σ (j+1)))
    (b : ℝ) (hb : |b| ≤ w/(g.width (ShiftedBlocks.endpoint σ (j+1))*Real.sqrt (g.branching:ℝ)))
    (z : ℝ × ℝ)
    (hsmall : Real.exp ((5*D/Kw)/Real.sqrt (g.branching:ℝ))*
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.AngularGrid.width, OAI.LipschitzHilbert.ShiftedBlocks.endpoint