OAI/Analysis/LipschitzHilbert/Trees/SourceTreeExpansion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite angular-tree conservation law is exactly the stopped product used in the analytic path estimate.

  1. def OAI.LipschitzHilbert.AngularGrid.sourceTreePathMass line 21
  2. def OAI.LipschitzHilbert.AngularGrid.sourceTreePathRatio line 26
  3. theorem OAI.LipschitzHilbert.AngularGrid.sourceTreeTail_eq_scalar line 34
  4. theorem OAI.LipschitzHilbert.AngularGrid.sourceTreeTail_eq_stopped line 47
  5. theorem OAI.LipschitzHilbert.AngularGrid.sourceTree_terminal_expansion line 78

    Source documentation

    Exact terminal product expansion of the original node amount.

    theorem sourceTree_terminal_expansion (hp : ∀ t ∈ tops, 0 ≤ precision t)
    (hw : ∀ t x, 0 < weight t x) (hlevel : Monotone level)
    (M : ℝ) (hM : 0 ≤ M) (count : ℕ) (cell : ℤ)
    (hne : (g.cellTops tops slope precision cutoff (level 0) cell).Nonempty)
    (hterminal : ∀ t ∈ g.cellTops tops slope precision cutoff (level 0) cell,
      ¬g.eligible cutoff (precision t) (level count)) :
    (∑ t ∈ g.cellTops tops slope precision cutoff (level 0) cell,
      let stop := firstMassStop (g.sourceTreePathMass tops slope precision cutoff weight level x t) count M
…

    Mentions: OAI.LipschitzHilbert.firstMassStop