PrimaryNormMultiplicity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Rational norm fibers of arbitrary primary elements. An element of norm n divides the rational integer n in the Eisenstein ring. Thus the proved ideal divisor bound supplies the small multiplicity loss required by the ordinary Montgomery--Vaughan input, without any prime-factor restriction.

lemma OAI.CubicFirstMoment.primary_dvd_of_normNat_eq line 16
lemma OAI.CubicFirstMoment.norm_natCast_eisenstein line 21

theorem OAI.CubicFirstMoment.primary_norm_fiber_small_power line 26

Source documentation

Uniform small-power bound for positive rational norm fibers.

theorem primary_norm_fiber_small_power {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (T : Finset Eisenstein),
      (∀ b ∈ T, primary b) → ∀ n : ℕ, 0 < n →
      ((T.filter (fun b => normNat b = n)).card:ℝ) ≤ C*(n:ℝ)^ε := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.normNat

lemma OAI.CubicFirstMoment.primary_norm_fiber_length_bound line 45

theorem OAI.CubicFirstMoment.primary_angular_meanSquare line 58

Source documentation

The actual primary angular polynomial satisfies the ordinary height mean with only an arbitrarily small norm-length loss.

theorem primary_angular_meanSquare {ε C : ℝ} (hε : 0 < ε)
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) :
    ∃ D : ℝ, 0 < D ∧ ∀ (T : Finset Eisenstein), (∀ b ∈ T, primary b) →
      ∀ (v : Eisenstein → ℂ) (Z : ℕ),
      (∀ b ∈ T, normNat b ∈ Finset.Icc 1 Z) → ∀ (ℓ : ℤ) (u a b : ℝ), a ≤ b →
      (∫ t in a..b, ‖∑ c ∈ T, v c*theta ℓ c*mellinPhase (t+u) (norm c)‖^2) ≤
        C*(b-a+Z)*(D*(Z:ℝ)^ε)*(∑ c ∈ T, ‖v c‖^2) := by
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.theta, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.norm