OAI/NumberTheory/CubicMoment/Estimates/EnlargedNoncubeGap.lean
2 declarations, 0 contain sorry, 0 declared as axioms
The nonexceptional sieve gap persists under the small enlargement of
P Q² ≤ B required by the dispersion localization.
- theorem
OAI.CubicFirstMoment.enlarged_noncube_exponent_gapline 11 - theorem
OAI.CubicFirstMoment.enlarged_noncube_ratio_savingline 62Source documentation
The same enlargement allows all sieve epsilon losses to be absorbed.
theorem enlarged_noncube_ratio_saving {κ δ : ℝ} (hκ : 0 < κ) (hδ : 0 < δ) : ∃ η γ : ℝ, 0 < η ∧ η ≤ 1 ∧ 0 < γ ∧ ∀ (B p q e : ℝ), 1 ≤ B → 0 ≤ p → 0 ≤ q → p+2*q ≤ 1+η → κ ≤ p+2*q → δ ≤ |p-1|+|q| → δ ≤ |p-1/3|+|q-1/3| → e ≤ γ/2 → B^e * min (pSieveRatio B (B^p) (B^q)) (min (qSieveRatio B (B^p) (B^q)) (ordinarySieveRatio B (B^p) (B^q))) ≤ 3*B^(-γ/2) := by …Mentions: OAI.CubicFirstMoment.pSieveRatio, OAI.CubicFirstMoment.qSieveRatio, OAI.CubicFirstMoment.ordinarySieveRatio