PrimeGroupTailAllFrequency.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

All nonzero frequencies through N^(19/20), including cubes, at arbitrary translated heights.

theorem OAI.CubicFirstMoment.primeGroupTail_all_frequency_height_power line 14

Source documentation

Every nonzero frequency in the small-B cutoff has a power-saving height average, with arbitrary coefficients and no restriction on u.

theorem primeGroupTail_all_frequency_height_power
    {C : ℝ} (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C)
    (hHuxley : HuxleyAdditiveLargeSieve) :
    ∃ K : ℝ, 0 < K ∧ ∀ (S H : Finset Eisenstein) (β : Eisenstein → ℂ)
      (Z : ℕ) (B T u : ℝ) (ℓ : ℤ), 1 ≤ (Z:ℝ) → 1 ≤ B →
      (Z:ℝ)^(1/50:ℝ) ≤ T →
      (∀ b ∈ S, primary b ∧ Squarefree b ∧ norm b ≤ (Z:ℝ)) →
      8*B ≤ (Z:ℝ)^(19/20:ℝ) →
      (∀ h ∈ H, h ≠ 0 ∧ norm h ≤ B) →
      dyadicHeightMean (fun t => ∑ h ∈ H,
        ‖∑ b ∈ S, β b*cubicSymbol b h*theta ℓ b*mellinPhase (t+u) (norm b)‖^2) T ≤
      K*(Z:ℝ)^(1-1/20000:ℝ)*B^(1/3:ℝ)*∑ b ∈ S, ‖β b‖^2 := by
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.dyadicHeightMean, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.theta, OAI.CubicFirstMoment.mellinPhase