SourceTreeProbability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Every child transition in the actual angular tree has mass at most one. The terminal path weights therefore have the required uniform cap.

theorem OAI.LipschitzHilbert.AngularGrid.sourceTreePathRatio_nonneg line 20
theorem OAI.LipschitzHilbert.AngularGrid.sourceTreeExit_nonneg line 30
theorem OAI.LipschitzHilbert.AngularGrid.sourceTreeDenominator_ge_child_amount line 40

theorem OAI.LipschitzHilbert.AngularGrid.sourceTree_terminal_probability_le line 67

Source documentation

The product-to-root quotient has a uniform cap for every individual terminal top; all preceding transitions use the actual child denominator.

theorem sourceTree_terminal_probability_le
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t x, 0 < weight t x)
    (hlevel : Monotone level) (M : ℝ) (hM : 1 ≤ M)
    (count : ℕ) (top : τ) (htop : top ∈ tops)
    (hterminal : ¬g.eligible cutoff (precision top) (level count))
    (hroot : M < g.sourceTreePathMass tops slope precision cutoff weight level x top 0)
    (C : ℝ)
    (hexit : g.sourceTreeExit tops slope precision cutoff weight level A α p x
      (firstMassStop (g.sourceTreePathMass tops slope precision cutoff weight level x top) count M)
      top ≤ C) :
    weight top x*g.sourceTreeTail tops slope precision cutoff weight level A α p x M count 0 top/
      g.sourceTreeAmount tops slope precision cutoff weight level A α p x 0
…

Mentions: OAI.LipschitzHilbert.firstMassStop