StoppedScalarExpansion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar algebra for a stopped path. The terminal coefficient is retained, so a small positive terminal mass is never replaced by zero.

def OAI.LipschitzHilbert.stoppedScalarExpansion line 13

theorem OAI.LipschitzHilbert.stoppedScalarExpansion_eq line 19

Source documentation

Unroll up to the first inactive index, keeping its exact terminal value.

theorem stoppedScalarExpansion_eq (active : ℕ → Prop) (beta terminal : ℕ → ℝ)
    (count stop j : ℕ) (hstop : stop ≤ count)
    (ha : ∀ i < stop, active (j+i)) (hz : ¬active (j+stop)) :
    stoppedScalarExpansion active beta terminal count j =
      terminal (j+stop)*∏ i ∈ Finset.range stop, beta (j+i) := by
…

Mentions: OAI.LipschitzHilbert.stoppedScalarExpansion

theorem OAI.LipschitzHilbert.normalized_path_parent_bound line 54

Source documentation

A normalized path reaches its final parent with probability at most one. This is the scalar form of the subunit child transition bound.

theorem normalized_path_parent_bound (V D : ℕ → ℝ) (N : ℕ)
    (hV : ∀ j ≤ N, 0 < V j) (hD : ∀ j ≤ N, 0 < D j)
    (hchild : ∀ j < N, V (j+1) ≤ D j) :
    (∏ j ∈ Finset.range (N+1), V j/D j) ≤ V 0/D N := by
…

theorem OAI.LipschitzHilbert.normalized_terminal_weight_bound line 74

Source documentation

An arbitrary terminal coefficient with a weight bound gives the required per-top probability bound, with no depth factor.

theorem normalized_terminal_weight_bound (V D : ℕ → ℝ) (N : ℕ)
    (e C w : ℝ) (hV : ∀ j ≤ N, 0 < V j) (hD : ∀ j ≤ N, 0 < D j)
    (hchild : ∀ j < N, V (j+1) ≤ D j) (he : 0 ≤ e) (hCw : e ≤ C*w)
    (hfinal : 1 ≤ D N) :
    e*(∏ j ∈ Finset.range (N+1), V j/D j)/V 0 ≤ C*w := by
…