StructuredMeanValue.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Mean values of the squarefree prime-convolution discrepancy

The ordinary Montgomery--Vaughan input is specialized to the actual coefficients obtained from independent prime factors. The full polynomial factors exactly; removing repeated primes costs the energy already proved in RepeatedPrimeSupport. The maximum multiplicity of an integer norm is kept explicit, so no divisor estimate is hidden in this deduction.

lemma OAI.CubicFirstMoment.theta_finset_prod line 24
lemma OAI.CubicFirstMoment.normTwist_finset_prod line 31
def OAI.CubicFirstMoment.angularCoefficientPolynomial line 43
Source documentation
Fixed-angle polynomial with arbitrary finite Eisenstein support.
```
def angularCoefficientPolynomial (B : Finset Eisenstein) (β : Eisenstein → ℂ)
    (ℓ : ℤ) (u t : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.fullPrimeProductPolynomial line 51
Source documentation
The product before imposing squarefreeness. The prime supports and weights are independent, exactly as required by the structured coefficients.
```
def fullPrimeProductPolynomial (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) (ℓ : ℤ) (u t : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.squarefreePrimePolynomial line 55
def OAI.CubicFirstMoment.errorPrimePolynomial line 60
theorem OAI.CubicFirstMoment.orderedConvolution_angular_polynomial line 67
Source documentation
Collection by products preserves the independent prime factorization, including the fixed angular character and the translated Mellin height.
```
theorem orderedConvolution_angular_polynomial (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ)
    (hS : ∀ i, ∀ p ∈ S i, primaryPrime p) (ℓ : ℤ) (u t : ℝ) :
    angularCoefficientPolynomial (orderedConvolutionSupport S)
      (orderedConvolution S w) ℓ u t = fullPrimeProductPolynomial S w ℓ u t := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.angularCoefficientPolynomial, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.fullPrimeProductPolynomial
theorem OAI.CubicFirstMoment.fullPrimeProduct_sub_squarefree line 91
Source documentation
The difference between the factored polynomial and its squarefree part has exactly the repeated-prime discrepancy coefficients.
```
theorem fullPrimeProduct_sub_squarefree (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ)
    (hS : ∀ i, ∀ p ∈ S i, primaryPrime p) (ℓ : ℤ) (u t : ℝ) :
    fullPrimeProductPolynomial S w ℓ u t - squarefreePrimePolynomial S w ℓ u t =
      errorPrimePolynomial S w ℓ u t := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.fullPrimeProductPolynomial, OAI.CubicFirstMoment.squarefreePrimePolynomial, OAI.CubicFirstMoment.errorPrimePolynomial
def OAI.CubicFirstMoment.normFiberMultiplicity line 103
Source documentation
The actual largest multiplicity when distinct Eisenstein integers have the same positive rational norm.
```
def normFiberMultiplicity (B : Finset Eisenstein) (Z : ℕ) : ℕ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.normFiber_card_le line 106
lemma OAI.CubicFirstMoment.normFiberMultiplicity_primeProducts_le line 112
lemma OAI.CubicFirstMoment.orderedConvolutionSupport_ne_zero line 120
lemma OAI.CubicFirstMoment.orderedConvolutionSupport_normNat line 129

theorem OAI.CubicFirstMoment.primeConvolutionError_dyadicMeanSquare line 147

Source documentation

The repeated-prime error inherits an actual power saving in its dyadic mean square. The only analytic input here is the ordinary published Montgomery--Vaughan inequality; the coefficient energy is proved.

theorem primeConvolutionError_dyadicMeanSquare {C : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) :
    ∃ K : ℝ, 0 < K ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ) (Y c : ℝ) (Z : ℕ),
      0 < Y → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ p ∈ S i, primaryPrime p ∧ Y ^ c < norm p) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i) → Y ≤ (Z : ℝ) →
      ∀ (ℓ : ℤ) (u T : ℝ), 0 < T →
      ((∫ t in T..2 * T, ‖errorPrimePolynomial S w ℓ u t‖ ^ 2) +
       (∫ t in -2 * T..-T, ‖errorPrimePolynomial S w ℓ u t‖ ^ 2)) / T ≤
        2 * C * (1 + (Z : ℝ) / T) *
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.errorPrimePolynomial

lemma OAI.CubicFirstMoment.coefficient_twist_energy_le line 177
Source documentation
A character bounded by one does not increase coefficient energy, including at primes dividing its conductor, where it may vanish.
```
lemma coefficient_twist_energy_le (B : Finset Eisenstein)
    (β χ : Eisenstein → ℂ) (hχ : ∀ b ∈ B, ‖χ b‖ ≤ 1) :
    (∑ b ∈ B, ‖β b * χ b‖ ^ 2) ≤ ∑ b ∈ B, ‖β b‖ ^ 2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.twistedErrorPrimePolynomial line 187

theorem OAI.CubicFirstMoment.primeConvolutionError_twisted_height_bounds line 195

Source documentation

Both height norms required in the exceptional-moment argument retain the repeated-prime power saving after a conductor character is inserted. All constants are uniform in the character, angular mode, and translation.

theorem primeConvolutionError_twisted_height_bounds {C : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) :
    ∃ K : ℝ, 0 < K ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ) (Y c : ℝ) (Z : ℕ),
      0 < Y → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ p ∈ S i, primaryPrime p ∧ Y ^ c < norm p) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i) → Y ≤ (Z : ℝ) →
      ∀ χ : Eisenstein → ℂ,
      (∀ b ∈ orderedConvolutionSupport S, ‖χ b‖ ≤ 1) →
      ∀ (ℓ : ℤ) (u T : ℝ), 0 < T →
      (((∫ t in T..2 * T, ‖twistedErrorPrimePolynomial S w χ ℓ u t‖ ^ 2) +
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.twistedErrorPrimePolynomial

lemma OAI.CubicFirstMoment.norm_mixedCubic_le_one line 236
theorem OAI.CubicFirstMoment.orderedConvolution_mixedCubic_weight line 246
Source documentation
A mixed cubic character may be moved between the independent prime weights and the collected convolution coefficient, even at its conductor.
```
theorem orderedConvolution_mixedCubic_weight (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) {q₁ q₂ : Eisenstein}
    (h₁ : primary q₁) (h₂ : primary q₂) (b : Eisenstein) :
    orderedConvolution S (fun i p => w i p * mixedCubic q₁ q₂ p) b =
      orderedConvolution S w b * mixedCubic q₁ q₂ b := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.orderedConvolution, OAI.CubicFirstMoment.mixedCubic
def OAI.CubicFirstMoment.mixedSquarefreePrimePolynomial line 260
Source documentation
This is the actual squarefree mixed-character polynomial appearing after the independent prime factors have been expanded.
```
def mixedSquarefreePrimePolynomial (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) (q₁ q₂ : Eisenstein) (ℓ : ℤ) (u t : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
theorem OAI.CubicFirstMoment.fullPrimeProduct_sub_mixedSquarefree line 265
theorem OAI.CubicFirstMoment.mixedCubic_error_energy_le line 279
Source documentation
The mixed-character twist needed by the exceptional moments satisfies the coefficient-energy requirement without any coprimality restriction.
```
theorem mixedCubic_error_energy_le (S : ι → Finset Eisenstein)
    (w : ι → Eisenstein → ℂ) {q₁ q₂ : Eisenstein}
    (h₁ : primary q₁) (h₂ : primary q₂) :
    (∑ b ∈ orderedConvolutionSupport S,
      ‖squarefreeConvolutionError S w b * mixedCubic q₁ q₂ b‖ ^ 2) ≤
        ∑ b ∈ orderedConvolutionSupport S, ‖squarefreeConvolutionError S w b‖ ^ 2 :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.squarefreeConvolutionError, OAI.CubicFirstMoment.mixedCubic

theorem OAI.CubicFirstMoment.primeConvolutionError_fixedLength_height_bounds line 290

Source documentation

The final fixed-length specialization has no arithmetic multiplicity hypothesis: its entire loss depends only on the number of prime factors. In particular it applies to mixedCubic q₁ q₂ by norm_mixedCubic_le_one.

theorem primeConvolutionError_fixedLength_height_bounds {C : ℝ}
    (hMV : MontgomeryVaughanBound C) (hC : 0 ≤ C) :
    ∃ K : ℝ, 0 < K ∧ ∀ (S : ι → Finset Eisenstein)
      (w : ι → Eisenstein → ℂ) (M : ι → ℝ) (Y c : ℝ) (Z : ℕ),
      0 < Y → (∀ i, 0 ≤ M i) →
      (∀ i, ∀ p ∈ S i, primaryPrime p ∧ Y ^ c < norm p) →
      (∀ f ∈ Fintype.piFinset S, norm (∏ i, f i) ≤ Y) →
      (∀ i, ∀ p ∈ S i, ‖w i p‖ ≤ M i) → Y ≤ (Z : ℝ) →
      ∀ χ : Eisenstein → ℂ,
      (∀ b ∈ orderedConvolutionSupport S, ‖χ b‖ ≤ 1) →
      ∀ (ℓ : ℤ) (u T : ℝ), 0 < T →
      (((∫ t in T..2 * T, ‖twistedErrorPrimePolynomial S w χ ℓ u t‖ ^ 2) +
…