OAI/NumberTheory/Ostmann/Quadratic/QuadraticIntervalInverse.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.integerQuadraticPhase line 11
2. theorem OAI.Ostmann.integerQuadraticPhase_translate line 14
3. theorem OAI.Ostmann.weighted_quadratic_translate_norm line 24
4. theorem OAI.Ostmann.weighted_integer_quadratic_inverse line 40

   Source documentation

   The original interval location affects only the linear coefficient, which is arbitrary in the proved inverse theorem.

   theorem weighted_integer_quadratic_inverse (w : ℕ → ℂ) (α β δ : ℝ) (z : ℤ) (N : ℕ)
       (hN : 0 < N) (hδ : 0 < δ) (hδ1 : δ ≤ 1)
       (hscale : 512 * (1 + 2 * Real.log (N : ℝ)) ≤ δ ^ 3 * N)
       (hlarge : discreteVariation w N * (δ * N) <
         ‖∑ j ∈ Finset.range N, w j * integerQuadraticPhase α β (z + j)‖) :
       ∃ q : ℕ, 0 < q ∧ (q : ℝ) ≤ 1024 / δ ^ 2 ∧
         |(q : ℝ) * α - (round ((q : ℝ) * α) : ℤ)| ≤
           1024 * (1 + 2 * Real.log (N : ℝ)) / (δ ^ 4 * (N : ℝ) ^ 2) := by
   …

   Mentions: OAI.Ostmann.discreteVariation, OAI.Ostmann.integerQuadraticPhase