WeightedQuadraticInverse.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The inverse phase conclusion for the actual weighted quadratic sum

theorem OAI.Ostmann.weighted_quadratic_inverse line 14

Source documentation

Finite variation removes the smooth weight. The resulting explicit losses are harmless exponential factors when δ=exp(-K), as in the manuscript.

theorem weighted_quadratic_inverse (w : ℕ → ℂ) (α β δ : ℝ) (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 * realQuadraticPhase α β 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.realQuadraticPhase