QuadraticProgressionExtraction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

From the original positive sum to its long weighted progression

theorem OAI.Ostmann.quadratic_cutoff_scale line 12
theorem OAI.Ostmann.quadratic_normalizer_progression_scale line 23

theorem OAI.Ostmann.positiveQuadraticSum_large_progression line 31

Source documentation

The estimate is extracted from the actual compactly supported positive series. Its hypothesis is the explicit large-sum event in the manuscript.

theorem positiveQuadraticSum_large_progression {q : ℕ} [NeZero q]
    (g : ZMod q → ℂ) (hg : ∀ x, ¬IsUnit x → g x = 0)
    (henergy : (∑ x : ZMod q, ‖g x‖ ^ 2) ≤ q)
    (a : ZMod q) (h₀ s v : ℕ) (θ R B A : ℝ) (Φ : 𝓢(ℝ, ℂ))
    (hs : 0 < s) (hv : 0 < v) (hR : 0 < R) (hB : 3 ≤ B)
    (hY : 1 ≤ Real.sqrt (R / ((s : ℝ) * v * q))) (hA : 0 ≤ A)
    (hΦ : ∀ x : ℝ, B ^ 2 < x → Φ x = 0)
    (hlarge : (Real.sqrt ((2 : ℝ) ^ (q.primeFactors.card + 1)) * q) * A <
      Real.sqrt (R * q / ((s : ℝ) * v)) *
        ‖positiveQuadraticSum g a ((h₀ : ℝ) + θ) Φ R v s‖) :
    ∃ r : ℕ, 0 < r ∧ r ≤ q ∧
      let N := (⌊B * q * Real.sqrt (R / ((s : ℝ) * v * q))⌋₊ + q - r) / q
…

Mentions: OAI.Ostmann.positiveQuadraticSum