OAI/NumberTheory/Ostmann/Arithmetic/MovingAveragedIntegerNode.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTemplateSidePrior line 10
2. def OAI.Ostmann.movingTemplateIntegerFourierTerm line 15
3. theorem OAI.Ostmann.movingTemplateCoefficient_averaged_integer_node line 41

   Source documentation

   The next regular template is the independent pair of the two surviving templates. Compensation remains outside both priors and is sampled once.

   theorem movingTemplateCoefficient_averaged_integer_node {σ : Type} [Fintype σ]
       (value : σ → ℕ) (hvalue : ∀ a, (value a).Prime) (outside : List ℕ)
       (μ : ℕ → σ → ℝ) (childBound pivotBound V : ℕ → ℕ) (hV : Monotone V)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ) (s : ℤ)
       (hsV : s.natAbs ≤ V (n + 1))
       (ν : MovingRegularSlot (n + 1) r m → σ → ℝ)
       (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.MovingRegularSlot