SparseGeometricStop.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The sparse-support hypotheses follow from the actual descending geometric bins and the ordinary X^.36 then X^.38 stopping thresholds.

lemma OAI.CubicFirstMoment.geometric_late_prime_bound line 14
lemma OAI.CubicFirstMoment.ordinary_late_threshold_ratio line 25
theorem OAI.CubicFirstMoment.ordinary_late_stopped_support line 30

theorem OAI.CubicFirstMoment.ordinary_late_stopped_energy line 59

Source documentation

The literal ordinary late-stop coefficient has power-saving energy. Only the concrete location of the roughness boundary is required; the large divisor and its sparse multiple support follow from the stopping condition.

theorem ordinary_late_stopped_energy {ι : Type*} [Fintype ι] [DecidableEq ι]
    (hpnt : PrimaryPrimePNT) {C ξ : ℝ} (hC : 0 < C)
    (hξ : 0 < ξ) (hξz : ξ ≤ 2/5) :
    ∃ δ K : ℝ, 0 < δ ∧ 0 < K ∧ ∀ᶠ X : ℝ in atTop,
      ∀ (B ρ : ℝ), 0 ≤ B → B ≤ X → 1 < ρ → ρ ≤ 2 →
      ∀ (j k h : ℕ), ρ*geometricBinLower ρ X h ≤ (Real.log X)^C →
      ∀ (S : ι → Finset Eisenstein) (W : ι → Eisenstein → ℂ)
        (R D U : Finset Eisenstein),
      (∀ i, ∀ p ∈ S i, primaryPrime p) → (∀ i, ∀ p ∈ S i, ‖W i p‖ ≤ 1) →
      (∀ r ∈ R, primary r) → (∀ d ∈ D, primary d ∧ norm d ≤ X) →
      (∀ b ∈ U, primary b ∧ Squarefree b ∧ norm b ≤ B) →
      (∑ b ∈ U, ‖stoppedBeta R D
…

Mentions: OAI.CubicFirstMoment.PrimaryPrimePNT, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.stoppedBeta