OAI/NumberTheory/Ostmann/Quadratic/QuadraticCompactCutoff.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.quadraticCompactCutoff line 12
2. theorem OAI.Ostmann.quadraticCompactCutoff_spec line 15
3. theorem OAI.Ostmann.quadraticDensityTerm_mem_cutoff line 27
4. def OAI.Ostmann.positiveQuadraticSum line 47
5. theorem OAI.Ostmann.positiveQuadraticSum_eq_cutoff line 54

   Source documentation

   Compact support makes the positive quadratic series exactly finite, with one common cutoff for every index in the dyadic segment.

   theorem positiveQuadraticSum_eq_cutoff {q : ℕ} [NeZero q]
       (g : ZMod q → ℂ) (a : ZMod q) (θ : ℝ) (Φ : 𝓢(ℝ, ℂ))
       (R v C : ℝ) (N s : ℕ) (hR : 0 < R) (hv : 0 < v) (hN : 0 < N)
       (hs : N ≤ s) (hΦ : ∀ x : ℝ, C < x → Φ x = 0) :
       positiveQuadraticSum g a θ Φ R v s =
         quadraticDensitySum g (quadraticCompactCutoff q R v C N) a θ Φ R v s := by
   …

   Mentions: OAI.Ostmann.positiveQuadraticSum, OAI.Ostmann.quadraticDensitySum, OAI.Ostmann.quadraticCompactCutoff