OAI/NumberTheory/Ostmann/Arithmetic/MovingDirectRecursion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingSampledWeight_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_direct_node {σ : Type*} [Fintype σ]
       (value : σ → ℕ) (μ : ℕ → σ → ℝ) (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