SourcePathDropMotion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The path drop in §9 is comparable throughout the reference cell. The complement may be empty: relative motion then fixes its zero mass.

theorem OAI.LipschitzHilbert.complementary_mass_drop_motion line 12

theorem OAI.LipschitzHilbert.AngularGrid.source_path_drop_motion line 42

Source documentation

Actual child and complementary top sums give the source's pred:drop-comparability, retaining the exact drop in the error.

theorem source_path_drop_motion {ι : Type*}
    (g : AngularGrid) (tops : Finset ι) (T : ι → SlopeBox)
    (w B K D : ℝ) (hw : 0 < w) (hB : 1 ≤ B) (hK : 0 < K) (hD : 0 ≤ D)
    (hwidth : ∀ t ∈ tops, B^2*w ≤ (T t).width)
    (base h i : ℕ) (hhi : h ≤ i) (gap : ℝ) (hgap0 : 0 ≤ gap) (hgap : gap ≤ g.width h)
    (s sR : ℝ) (hs : g.index h s = g.index h sR)
    (child : ℝ) (hchild : 0 < child) (hblock : g.width h ≤ B*child)
    (parentSet childSet : Finset ι) (hsub : childSet ⊆ parentSet) (hne : childSet.Nonempty)
    (hparent : parentSet ⊆ g.boundaryTops tops (fun t => (T t).slope)
      (fun t => w/(T t).length) (g.rootWidth/B^2) base i gap s)
    (b : ℝ) (hb : |b| ≤ w/(child*Real.sqrt (g.branching:ℝ))) (z : ℝ × ℝ)
    (hsmall : Real.exp ((5*D/K)/Real.sqrt (g.branching:ℝ))*
…

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