OAI/Analysis/LipschitzHilbert/Trees/SourceTreeConservation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact finite conservation for the actual angular partitions. Stopping at a small-mass cell retains its normalized vertex amount; ineligible tops retain their original weight.

  1. theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_sum_continuing line 15
  2. theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_weighted_sum line 36
  3. def OAI.LipschitzHilbert.AngularGrid.sourceTreeAmount line 62
  4. def OAI.LipschitzHilbert.AngularGrid.sourceTreeDenominator line 65
  5. def OAI.LipschitzHilbert.AngularGrid.sourceTreeExit line 71
  6. def OAI.LipschitzHilbert.AngularGrid.sourceTreeTail line 78
  7. theorem OAI.LipschitzHilbert.AngularGrid.sourceTreeTail_ineligible line 92
  8. theorem OAI.LipschitzHilbert.AngularGrid.sourceTreeExit_sum line 97
  9. theorem OAI.LipschitzHilbert.AngularGrid.sourceTreeTail_sum line 120

    Source documentation

    A finite stopped expansion exactly recovers the original node amount. No transition or path-probability identity is assumed.

    theorem sourceTreeTail_sum (hp : ∀ t ∈ tops, 0 ≤ precision t)
    (hw : ∀ t x, 0 < weight t x) (hlevel : Monotone level) (M : ℝ)
    (n j : ℕ) (cell : ℤ)
    (hne : (g.cellTops tops slope precision cutoff (level j) cell).Nonempty) :
    (∑ t ∈ g.cellTops tops slope precision cutoff (level j) cell,
      weight t x*g.sourceTreeTail tops slope precision cutoff weight level A α p x M n j t) =
      g.sourceTreeAmount tops slope precision cutoff weight level A α p x j cell := by
…