SparseStoppedBilinear.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual sparse late-stop Gauss sums have a power saving. The two coefficient energies come from their literal stopping constructions; the smooth factor is handled by the proved weighted cubic sieve.

lemma OAI.CubicFirstMoment.energy_bounded_twist line 17

theorem OAI.CubicFirstMoment.ordinary_late_stopped_bilinear line 29

Source documentation

Fixed support dilations and arbitrary bounded independent twists are allowed. The small-prime boundary and the stopping thresholds are the actual geometric ones, not assumed sparsity of an abstract coefficient.

theorem ordinary_late_stopped_bilinear
    {ι γ : Type*} [Fintype ι] [DecidableEq ι]
    (hpnt : PrimaryPrimePNT) {C ξ M : ℝ} (hC : 0 < C)
    (hξ : 0 < ξ) (hξz : ξ ≤ 2/5) (hM : 1 ≤ M)
    {G : γ → ℝ → ℂ} (hG : UniformLogWeights G) :
    ∃ τ K : ℝ, 0 < τ ∧ 0 < K ∧ ∀ᶠ X : ℝ in atTop,
      ∀ (A B ρ V : ℝ), Real.exp 1 ≤ A → 1 ≤ B → A ≤ X → B ≤ X →
      A ≤ M*X^(2/3:ℝ) → B ≤ M*X^(2/3:ℝ) → A*B ≤ M*X →
      1 < ρ → ρ ≤ 2 → 0 < V →
      ∀ (j k h : ℕ), ρ*geometricBinLower ρ X h ≤ (Real.log X)^C →
      ∀ (S : ι → Finset Eisenstein) (W : ι → Eisenstein → ℂ)
        (R D E U P Q : Finset Eisenstein) (remaining : Eisenstein → Prop)
…

Mentions: OAI.CubicFirstMoment.PrimaryPrimePNT, OAI.CubicFirstMoment.UniformLogWeights, OAI.CubicFirstMoment.geometricBinLower, OAI.CubicFirstMoment.Eisenstein