SourcePathCoefficientMotion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The dominant path coefficient from actual complementary top masses. Empty complementary sets contribute zero and retain the path-drop factor.

theorem OAI.LipschitzHilbert.AngularGrid.source_submass_relative_motion line 13

theorem OAI.LipschitzHilbert.AngularGrid.source_path_coefficient_motion line 45

Source documentation

The two complements are actual finite top sums. The parent drop alone controls the coefficient drop and its motion.

theorem source_path_coefficient_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 boundarySet childSet : Finset ι)
    (hchildBoundary : childSet ⊆ boundarySet) (hboundaryParent : boundarySet ⊆ 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)
…

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