SourceBlockConservation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact conservation on one source block, including the top weights that stop before its upper endpoint. This is the row decomposition of the original node denominator used by the finite path flow.

theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_continuing_fiber line 16
theorem OAI.LipschitzHilbert.AngularGrid.sum_sourceBlock_child_mass line 41

theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_mass_conservation line 68

Source documentation

The stopping mass is an actual sum of original top weights.

theorem sourceBlock_mass_conservation (g : AngularGrid) (tops : Finset τ)
    (slope precision : τ → ℝ) (cutoff : ℝ) (weight : τ → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (lower upper : ℕ) (hle : lower ≤ upper)
    (parent : ℤ) (x : X) :
    g.mass tops slope precision cutoff weight lower parent x =
    (∑ t ∈ (g.cellTops tops slope precision cutoff lower parent).filter
      (fun t => ¬g.eligible cutoff (precision t) upper), weight t x)+
    ∑ c : g.sourceBlockCells tops slope precision cutoff lower upper parent,
      g.mass tops slope precision cutoff weight upper c.val x := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_denominator_conservation line 84

Source documentation

Exact source denominator as continuing child amounts plus stopped top weights; no mass is lost by grouping several angular levels.

theorem sourceBlock_denominator_conservation {κ : Type} [Fintype κ]
    (g : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ) (cutoff : ℝ)
    (weight : τ → X → ℝ) (hp : ∀ t ∈ tops, 0 ≤ precision t)
    (lower upper : ℕ) (hle : lower ≤ upper) (parent : ℤ) (x : X)
    (A : g.sourceBlockCells tops slope precision cutoff lower upper parent → EuclideanSpace ℂ κ)
    (α p : ℝ) :
    sourceNodeDenominator (g.mass tops slope precision cutoff weight lower parent x)
      (fun c => g.mass tops slope precision cutoff weight upper c.val x) A α p =
    (∑ t ∈ (g.cellTops tops slope precision cutoff lower parent).filter
      (fun t => ¬g.eligible cutoff (precision t) upper), weight t x)+
    ∑ c, vertexAmount (g.mass tops slope precision cutoff weight upper c.val x) (A c) α p := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.sourceNodeDenominator, OAI.LipschitzHilbert.vertexAmount