OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeOffDiagonalCoefficient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPrimeOffDiagonalCoefficient line 10
2. theorem OAI.Ostmann.movingFrequencyCoefficient_eq_offDiagonal line 35

   Source documentation

   This identifies the full next coefficient, rather than a history-wise surrogate. Only compensation samples with nonzero original prior need the range bounds.

   theorem movingFrequencyCoefficient_eq_offDiagonal {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (hV : Monotone V)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (s : ℤ)
       (hs : s ≠ 0) (hsV : s.natAbs ≤ V (n + 1))
       (small bulk : TreeLeafTuple (List σ) (n + 1)) (XL XR : ℕ)
       (hXL : XL.Prime) (hXR : XR.Prime)
       (hVL : V (n + 1) < XL) (hVR : V (n + 1) < XR)
       (I : Finset ℕ) (hI : ∀ p ∈ I, 0 < p)
       (hφ : ∀ p : ℕ, 0 < p → φ (Real.log p - G (n + 1)) ≠ 0 → p ∈ I)
       (hchild : V n ≤ childBound (n + 1)) :
   …

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