PositiveQuadraticWitness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A witness gives the denominator and accuracy at the manuscript scales

theorem OAI.Ostmann.quadratic_progression_scale_range line 12

theorem OAI.Ostmann.eventual_positiveQuadraticSum_phase_witness line 44

Source documentation

The original weighted series, with the original residue argument and the original scale R, yields a rational approximation. All numerical inequalities needed by the inverse theorem have been discharged.

theorem eventual_positiveQuadraticSum_phase_witness (B : ℝ) (Φ : 𝓢(ℝ, ℂ))
    (hB : 3 ≤ B) (hΦ : ∀ x : ℝ, B ^ 2 < x → Φ x = 0) :
    ∀ᶠ T : ℝ in atTop, ∀ (q s v : ℕ) [NeZero q] (g : ZMod q → ℂ)
      (a : ZMod q) (h₀ : ℕ) (θ R K : ℝ),
      (∀ x, ¬IsUnit x → g x = 0) → (∑ x : ZMod q, ‖g x‖ ^ 2) ≤ q →
      0 < s → 0 < v → 0 ≤ K → K ≤ T ^ (9999999 / 10000000 : ℝ) →
      ((s * v * q : ℕ) : ℝ) ≤ Real.exp (3 * T / 25) →
      Real.exp (10 * T) ≤ R → R ≤ Real.exp (14 * T) →
      Real.sqrt ((2 : ℝ) ^ q.primeFactors.card) * Real.exp (-K) <
        ‖positiveQuadraticSum g a ((h₀ : ℝ) + θ) Φ R v s‖ →
      ∃ c ∈ Finset.Icc 1 ⌈Real.exp (13 * T / 100)⌉₊, ∃ b : ℤ,
        |(c : ℝ) * θ - b| ≤ Real.exp (13 * T / 100) / R := by
…

Mentions: OAI.Ostmann.positiveQuadraticSum