OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateDiagonal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingTemplate_restored_diagonal_le line 14

   Source documentation

   Every support condition in the grouped diagonal estimate follows from the original coefficient and the prescribed prime/frequency ranges. Only the mass of an actual product/frequency fibre remains to be bounded.

   theorem movingTemplate_restored_diagonal_le {σ A : Type} [Fintype σ] [Fintype A]
       (value : σ → ℕ) (hvalue : ∀ a, (value a).Prime) (outside : List ℕ)
       (μ : ℕ → σ → ℝ) (childBound pivotBound V : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ)
       (u : TreeLeafIndex n × Fin 4 → σ) (p : ℕ)
       (X : A → ℕ) (hX : ∀ a, (X a).Prime)
       (y : A → MovingRegularSlot n r m → σ) (v : A → ℤ)
       (α : A → ℝ) (hα : ∀ a, 0 ≤ α a) (θ : ℕ × ℕ × ℤ → ℝ)
       (hv : ∀ a, (v a).natAbs ≤ V n)
       (hvg : ∀ a, V n < X a) (hvr : ∀ a i, V n < value (y a i))
       (hsep : ∀ a b i, X a ≠ value (y b i))
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot