PrimeModelHeight.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The undecomposed prime model at large heights. The norm fibre has size at most two, so Montgomery--Vaughan gives its genuine mean square without a divisor loss or an assumed model cancellation estimate.

lemma OAI.CubicFirstMoment.prime_model_coefficient_energy line 15
theorem OAI.CubicFirstMoment.prime_model_height_mean_square line 51
lemma OAI.CubicFirstMoment.continuous_prime_model_height line 102
theorem OAI.CubicFirstMoment.prime_model_height_mean_absolute line 111

theorem OAI.CubicFirstMoment.prime_model_height_power_saving line 124

Source documentation

Large-height decay for the actual prime model. Only ordinary polynomial mean value and the prime norm multiplicity are used.

theorem prime_model_height_power_saving {C : ℝ} (hMV : MontgomeryVaughanBound C)
    (hC : 0 ≤ C) (P : Finset Eisenstein) (c : Eisenstein → ℂ)
    {X T M δ : ℝ} (hX : 1 ≤ X) (hTX : T ≤ X) (hTδ : X^δ ≤ T) (hM : 0 ≤ M)
    (hP : ∀ p ∈ P, primaryPrime p ∧ norm p ≤ 4*X)
    (hc : ∀ p ∈ P, ‖c p‖ ≤ M) (ℓ : ℤ) (u : ℝ) :
    dyadicHeightMean (fun t =>
      ‖dispersionModel P (fun p => c p*theta ℓ p) (t+u)‖) T ≤
      2*Real.sqrt (720*C)*M*X^(5/6-δ/2) := by
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.dyadicHeightMean, OAI.CubicFirstMoment.dispersionModel, OAI.CubicFirstMoment.theta