EffectiveQuadraticInverse.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing the actual approximation cutoff for the inverse quadratic step

theorem OAI.Ostmann.effective_quadratic_inverse line 13

Source documentation

A quadratic sum of relative squared size ρ has a small denominator, with the expected N⁻² precision up to a logarithmic factor.

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