MovingBulkRecursiveWeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Factoring terminal bulk weights from the original recursion

theorem OAI.Ostmann.movingSlotWeight_bulk_log line 14

Source documentation

The logarithmic bulk cutoffs are independent of every reconstructed pivot and survive the right-branch conjugations unchanged.

theorem movingSlotWeight_bulk_log {σ : Type*} (value : σ → ℕ) (tier : σ → ℕ)
    (k : ℕ) (outside : List ℕ) (cb cd : ℝ)
    (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
    (cutoff : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
    {n : ℕ} (T : MovingSlotData σ n) (XL XR : ℕ) (t : FrequencyTree ℤ n) :
    recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
        (fun x s => (movingBulkLeafLogWeight value tier k outside cb cd x.data : ℂ) * F x s)
        cutoff n ⟨n, T, XL, XR⟩ t =
      (movingBulkTreeLogWeight value tier k outside cb cd T : ℂ) *
        recursiveTransferWeight (movingSlotSystem value childBound pivotBound)
          F cutoff n ⟨n, T, XL, XR⟩ t := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingBulkLeafLogWeight, OAI.Ostmann.movingBulkTreeLogWeight

theorem OAI.Ostmann.movingCompensationPrior_levels line 40

Source documentation

The unchanged independent law already enforces the tier of every compensation prime, including repeated draws.

theorem movingCompensationPrior_levels {σ : Type*} (μ : σ → ℝ)
    (tier : σ → ℕ) (j : ℕ) (hμ : ∀ a, μ a ≠ 0 → tier a = j)
    (n : ℕ) (a : TreeLeafTuple (Fin 4 → σ) n)
    (ha : movingCompensationPrior μ n a ≠ 0) :
    ∀ i ∈ flattenMovingSlots n (movingCompensationSlots n a), tier i = j := by
…

Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.movingCompensationPrior, OAI.Ostmann.flattenMovingSlots, OAI.Ostmann.movingCompensationSlots

theorem OAI.Ostmann.movingSamplesPrior_levels line 56