PolynomialMeanValue.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Ordinary mean values after collecting Eisenstein norms

The input MontgomeryVaughanBound is the ordinary Dirichlet-polynomial mean-square theorem of Montgomery--Vaughan, Hilbert's inequality, J. London Math. Soc. (2) 8 (1974), Corollary 3, p. 75, equation (1.11), in the form explicitly recorded in the manuscript as eq:ordinary-mean-value.

The deductions below collect the actual Eisenstein norms, record their multiplicity cost, and preserve an arbitrary fixed angular weight and an arbitrary translated height. These are the ordinary mean-value steps in eq:dispersion-height-small and eq:angular-completed-height.

def OAI.CubicFirstMoment.integerNormPolynomial line 28
Source documentation
Ordinary Dirichlet polynomial, with positive integer frequencies.
```
def integerNormPolynomial (Z : ℕ) (v : ℕ → ℂ) (t : ℝ) : ℂ :=
…
```
def OAI.CubicFirstMoment.MontgomeryVaughanBound line 33
Source documentation
Precise published input: the constant is independent of the interval, length, coefficients, and any later translation of the height.
```
def MontgomeryVaughanBound (C : ℝ) : Prop :=
…
```
def OAI.CubicFirstMoment.normCollectedCoeff line 39
Source documentation
Collection by rational norm, with no change to the coefficients.
```
def normCollectedCoeff (s : Finset Eisenstein) (v : Eisenstein → ℂ) (n : ℕ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.eisensteinNormPolynomial line 43
Source documentation
Finite polynomial before collecting the equal rational norms.
```
def eisensteinNormPolynomial (s : Finset Eisenstein) (v : Eisenstein → ℂ) (t : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.mellinPhase_add line 46
lemma OAI.CubicFirstMoment.normPolynomial_collected line 54
lemma OAI.CubicFirstMoment.norm_sum_sq_le_card_mul line 67
lemma OAI.CubicFirstMoment.normCollectedCoeff_energy line 75

theorem OAI.CubicFirstMoment.eisensteinNormPolynomial_meanSquare line 91

Source documentation

The mean-square bound with the exact multiplicity loss from collecting Eisenstein norms.

theorem eisensteinNormPolynomial_meanSquare {C : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C)
    (s : Finset Eisenstein) (v : Eisenstein → ℂ) (Z : ℕ) (M : ℝ)
    (hs : ∀ b ∈ s, normNat b ∈ Finset.Icc 1 Z)
    (hM : ∀ n ∈ Finset.Icc 1 Z, ((s.filter (fun b => normNat b = n)).card : ℝ) ≤ M)
    {a b : ℝ} (hab : a ≤ b) :
    (∫ t in a..b, ‖eisensteinNormPolynomial s v t‖ ^ 2) ≤
      C * (b - a + Z) * M * ∑ c ∈ s, ‖v c‖ ^ 2 := by
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.eisensteinNormPolynomial

theorem OAI.CubicFirstMoment.fixedAngular_translated_meanSquare line 109

Source documentation

A fixed angular character and translated height are coefficient phases; they do not change the original coefficient energy.

theorem fixedAngular_translated_meanSquare {C : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C)
    (s : Finset Eisenstein) (v : Eisenstein → ℂ) (Z : ℕ) (M : ℝ)
    (hs : ∀ b ∈ s, normNat b ∈ Finset.Icc 1 Z)
    (hzero : ∀ b ∈ s, b ≠ 0)
    (hM : ∀ n ∈ Finset.Icc 1 Z, ((s.filter (fun b => normNat b = n)).card : ℝ) ≤ M)
    (ℓ : ℤ) (u : ℝ) {a b : ℝ} (hab : a ≤ b) :
    (∫ t in a..b, ‖∑ c ∈ s, v c * theta ℓ c * mellinPhase (t + u) (norm c)‖ ^ 2) ≤
      C * (b - a + Z) * M * ∑ c ∈ s, ‖v c‖ ^ 2 := by
…

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

theorem OAI.CubicFirstMoment.fixedAngular_translated_dyadicMeanSquare line 137

Source documentation

The normalized two-sided height mean used for the small-conductor noncube contribution. Both positive and negative height intervals occur.

theorem fixedAngular_translated_dyadicMeanSquare {C : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C)
    (s : Finset Eisenstein) (v : Eisenstein → ℂ) (Z : ℕ) (M : ℝ)
    (hs : ∀ b ∈ s, normNat b ∈ Finset.Icc 1 Z)
    (hzero : ∀ b ∈ s, b ≠ 0)
    (hM : ∀ n ∈ Finset.Icc 1 Z, ((s.filter (fun b => normNat b = n)).card : ℝ) ≤ M)
    (ℓ : ℤ) (u : ℝ) {T : ℝ} (hT : 0 < T) :
    ((∫ t in T..2 * T, ‖∑ c ∈ s, v c * theta ℓ c * mellinPhase (t + u) (norm c)‖ ^ 2) +
     (∫ t in -2 * T..-T, ‖∑ c ∈ s, v c * theta ℓ c * mellinPhase (t + u) (norm c)‖ ^ 2)) / T ≤
      2 * C * (1 + (Z : ℝ) / T) * M * ∑ c ∈ s, ‖v c‖ ^ 2 := by
…

lemma OAI.CubicFirstMoment.continuous_angularNormPolynomial line 156
lemma OAI.CubicFirstMoment.interval_integral_sq_le line 167

theorem OAI.CubicFirstMoment.fixedAngular_translated_meanAbsolute_sq line 200

Source documentation

Mean absolute size on a height interval, derived from the mean square. This form retains the exact coefficient energy instead of hiding it in a big-O constant.

theorem fixedAngular_translated_meanAbsolute_sq {C : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C)
    (s : Finset Eisenstein) (v : Eisenstein → ℂ) (Z : ℕ) (M : ℝ)
    (hs : ∀ b ∈ s, normNat b ∈ Finset.Icc 1 Z)
    (hzero : ∀ b ∈ s, b ≠ 0)
    (hM : ∀ n ∈ Finset.Icc 1 Z, ((s.filter (fun b => normNat b = n)).card : ℝ) ≤ M)
    (ℓ : ℤ) (u : ℝ) {T : ℝ} (hT : 0 < T) :
    ((∫ t in T..2 * T, ‖∑ c ∈ s, v c * theta ℓ c * mellinPhase (t + u) (norm c)‖) / T) ^ 2 ≤
      C * (1 + (Z : ℝ) / T) * M * ∑ c ∈ s, ‖v c‖ ^ 2 := by
…

theorem OAI.CubicFirstMoment.fixedAngular_translated_short_meanAbsolute line 224

Source documentation

The short-polynomial branch of the completed angular height estimate: length at most sqrt R * T² and coefficient energy at most V give mean absolute size at most sqrt (2 C M V sqrt R T). The square-root form is O(sqrt V * R^(1/4) * sqrt T) after the divisor loss is included in M.

theorem fixedAngular_translated_short_meanAbsolute {C : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C)
    (s : Finset Eisenstein) (v : Eisenstein → ℂ) (Z : ℕ) (M : ℝ)
    (hs : ∀ b ∈ s, normNat b ∈ Finset.Icc 1 Z)
    (hzero : ∀ b ∈ s, b ≠ 0)
    (hM : ∀ n ∈ Finset.Icc 1 Z, ((s.filter (fun b => normNat b = n)).card : ℝ) ≤ M)
    (hM₀ : 0 ≤ M) (ℓ : ℤ) (u : ℝ) {T R V : ℝ}
    (hT : 1 ≤ T) (hR : 1 ≤ R) (hV : 0 ≤ V)
    (henergy : (∑ c ∈ s, ‖v c‖ ^ 2) ≤ V)
    (hlength : (Z : ℝ) ≤ Real.sqrt R * T ^ 2) :
    (∫ t in T..2 * T, ‖∑ c ∈ s, v c * theta ℓ c * mellinPhase (t + u) (norm c)‖) / T ≤
      Real.sqrt (2 * C * M * V * Real.sqrt R * T) := by
…