QuadraticInverse.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

An effective inverse conclusion for a large quadratic sum

All assumptions below are explicit numerical scale inequalities. The rational approximation and exponential-sum bound are proved, not supplied as inputs.

theorem OAI.Ostmann.weyl_numeric_contradiction line 15

theorem OAI.Ostmann.quadratic_inverse_approximation line 48

Source documentation

A large sum forces a denominator O(1/ρ), with approximation precision 1/(Q+1). The stated scale conditions are precisely those used to choose Q.

theorem quadratic_inverse_approximation (α β ρ B : ℝ) (N Q : ℕ)
    (hN : 0 < N) (hQ : 0 < Q) (hρ : 0 < ρ) (hB : 1 ≤ B)
    (hlog : 1 + Real.log (Q : ℝ) ≤ B)
    (hsmallN : 512 * B ≤ ρ * N)
    (hsmallQ : 512 * (Q : ℝ) * B ≤ ρ * (N : ℝ) ^ 2)
    (hlarge : ρ * (N : ℝ) ^ 2 ≤
      ‖∑ j ∈ Finset.range N, realQuadraticPhase α β j‖ ^ 2) :
    ∃ q : ℕ, 0 < q ∧ (q : ℝ) ≤ 1024 / ρ ∧
      |(q : ℝ) * α - (round ((q : ℝ) * α) : ℤ)| ≤ 1 / ((Q : ℝ) + 1) := by
…