MovingGuardedDirectRecursion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The fully guarded sampled recursion with the explicit giant quotient

theorem OAI.Ostmann.movingSampledWeight_guarded_direct_node line 13

Source documentation

The original sample law and the two independent child sample trees are retained. The inserted giant is exactly (v H⁻ - w H⁺)/(s U), matching the weighted integer off-diagonal, with every root support test still explicit.

theorem movingSampledWeight_guarded_direct_node {σ : Type*} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (n : ℕ) (t : FrequencyTree ℤ (n + 1))
    (small bulk : TreeLeafTuple (List σ) (n + 1)) (XL XR : ℕ) :
    let E := movingCompensatedExtra value (movingOriginalNode value childBound pivotBound φ G)
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingCompensatedExtra, OAI.Ostmann.movingOriginalNode

theorem OAI.Ostmann.movingSupportedSampledWeight_direct_node line 104

Source documentation

The same exact recurrence for the fully supported coefficient used by the arithmetic comparison.

theorem movingSupportedSampledWeight_direct_node {σ : Type*} [Fintype σ]
    (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ) (childBound pivotBound : ℕ → ℕ)
    (F : MovingSlotState σ → ℤ → ℂ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
    (n : ℕ) (t : FrequencyTree ℤ (n + 1))
    (small bulk : TreeLeafTuple (List σ) (n + 1)) (XL XR : ℕ) :
    let E := movingOriginalNode value childBound pivotBound φ G
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingOriginalNode