OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateIntegerNode.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplateMapped_product line 11
2. theorem OAI.Ostmann.movingTemplateCompensationEquiv_product line 20
3. theorem OAI.Ostmann.movingTemplateCoefficient_integer_node line 29

   Source documentation

   This is the full next coefficient under the original independent compensation law, with its exact integer pivot and complete child coefficients.

   theorem movingTemplateCoefficient_integer_node {σ : Type} [Fintype σ]
       (value : σ → ℕ) (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))
       (left right : MovingRegularSlot n 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