OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeCoefficientNode.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingFrequencyCoefficient_zero line 11
2. theorem OAI.Ostmann.movingFrequencyCoefficient_prime_node line 34

   Source documentation

   At actual prime giants, the original coefficient is the product recursion in the two complete child coefficients. The shared compensation prior occurs once, and every child retains its own descendant frequency and prime samples.

   theorem movingFrequencyCoefficient_prime_node {σ : 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) :
       movingFrequencyCoefficient value outside μ childBound pivotBound V F φ G
         (n + 1) s small bulk XL XR =
         ∑ a : TreeLeafTuple (Fin 4 → σ) n, (movingCompensationPrior (μ n) n a : ℂ) *
   …

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