QuadraticSmallGcdPowerSaving.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform arbitrary power saving at every retained small gcd

theorem OAI.Ostmann.quadratic_small_gcd_error_arbitrary_power line 11

theorem OAI.Ostmann.quadratic_rough_gcd_descent_epsilon line 36

Source documentation

The large-gcd loss in the descent is only an arbitrary small power.

theorem quadratic_rough_gcd_descent_epsilon (ε : ℝ) (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ M N K D₀ : ℕ, 0 < D₀ → ∀ T : ℝ, 0 ≤ T →
      QuadraticRoughBound M (N / D₀) K T → ∀ v : ℕ → ℂ,
      quadraticRoughEnergy M N K v ≤
        (∑ D ∈ (Finset.Icc 1 N).filter (fun D => D ≤ D₀),
          ‖quadraticRoughGcdMoment M N K D v‖) +
        C * (N : ℝ) ^ ε * T * quadraticSieveEnergy N v := by
…

Mentions: OAI.Ostmann.QuadraticRoughBound, OAI.Ostmann.quadraticRoughEnergy, OAI.Ostmann.quadraticRoughGcdMoment, OAI.Ostmann.quadraticSieveEnergy