DispersionAlgebra.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Exact corrected-dispersion identities

The polynomials below are those in eq:dispersion-polynomials of the manuscript. The factorization is valid even with a common prime factor: the already proved Gauss-sum multiplication law then makes the summand zero. The norm estimates here do not assume the new dispersion bounds.

def OAI.CubicFirstMoment.normTwist line 21
Source documentation
The norm twist at real Mellin height u.
```
def normTwist (u : ℝ) (a : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
theorem OAI.CubicFirstMoment.norm_normTwist line 24
theorem OAI.CubicFirstMoment.normTwist_mul line 27
def OAI.CubicFirstMoment.dispersionPolynomial line 37
Source documentation
The polynomial F_u(a) in the corrected-dispersion argument.
```
def dispersionPolynomial (B : Finset Eisenstein) (β : Eisenstein → ℂ)
    (u : ℝ) (a : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
def OAI.CubicFirstMoment.dispersionModel line 42
Source documentation
The model polynomial S(u).
```
def dispersionModel (B : Finset Eisenstein) (β : Eisenstein → ℂ) (u : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
theorem OAI.CubicFirstMoment.gauss_mul_star_squarefree line 47
Source documentation
The squarefree weight equals the squared absolute value of the normalized Gauss sum, for primary elements.
```
theorem gauss_mul_star_squarefree {a : Eisenstein} (ha : primary a) :
    gauss a * star (gauss a) = if Squarefree a then (1 : ℂ) else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.gauss
theorem OAI.CubicFirstMoment.norm_gauss_le_one line 54

theorem OAI.CubicFirstMoment.bilinear_gauss_eq_rows line 59

Source documentation

Exact factorization of the bilinear Gauss sum into the dispersion rows.

theorem bilinear_gauss_eq_rows (A B : Finset Eisenstein)
    (α β : Eisenstein → ℂ) (u : ℝ)
    (hA : ∀ a ∈ A, primary a) (hB : ∀ b ∈ B, primary b) :
    (∑ a ∈ A, ∑ b ∈ B, α a * β b * gauss (a * b) * normTwist u (a * b)) =
      ∑ a ∈ A, α a * normTwist u a * gauss a * dispersionPolynomial B β u a := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.dispersionPolynomial

def OAI.CubicFirstMoment.correctedDispersionPolynomial line 74
Source documentation
The corrected row polynomial.
```
def correctedDispersionPolynomial (B : Finset Eisenstein) (β : Eisenstein → ℂ)
    (u : ℝ) (a : Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein

theorem OAI.CubicFirstMoment.corrected_bilinear_identity line 83

Source documentation

The correction subtracts the factored model exactly, with the true squarefree weight on the outer variable. Removing common prime factors from the model is a separate arithmetic step.

theorem corrected_bilinear_identity (A B : Finset Eisenstein)
    (α β : Eisenstein → ℂ) (u : ℝ)
    (hA : ∀ a ∈ A, primary a) (hB : ∀ b ∈ B, primary b) :
    (∑ a ∈ A, ∑ b ∈ B, α a * β b * gauss (a * b) * normTwist u (a * b)) -
      (cStar : ℂ) * dispersionModel B β u *
        (∑ a ∈ A, α a * normTwist u a *
          (if Squarefree a then (1 : ℂ) else 0) * ((norm a ^ (-1 / 6 : ℝ) : ℝ) : ℂ)) =
      ∑ a ∈ A, α a * normTwist u a * gauss a *
        correctedDispersionPolynomial B β u a := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.cStar, OAI.CubicFirstMoment.dispersionModel, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.correctedDispersionPolynomial

theorem OAI.CubicFirstMoment.complex_bilinear_rows_sq line 101

Source documentation

Finite Cauchy--Schwarz for the actual complex row sum.

theorem complex_bilinear_rows_sq {ι : Type*} (A : Finset ι) (α F : ι → ℂ) :
    ‖∑ a ∈ A, α a * F a‖ ^ 2 ≤
      (∑ a ∈ A, ‖α a‖ ^ 2) * ∑ a ∈ A, ‖F a‖ ^ 2 := by
…

theorem OAI.CubicFirstMoment.corrected_bilinear_bound_sq line 112
Source documentation
The outer Gauss sum and norm twist cost no more than the coefficient energy. Thus the corrected variance gives the desired bilinear saving.
```
theorem corrected_bilinear_bound_sq (A B : Finset Eisenstein)
    (α β : Eisenstein → ℂ) (u : ℝ) (hA : ∀ a ∈ A, primary a) :
    ‖∑ a ∈ A, α a * normTwist u a * gauss a *
        correctedDispersionPolynomial B β u a‖ ^ 2 ≤
      (∑ a ∈ A, ‖α a‖ ^ 2) *
        ∑ a ∈ A, ‖correctedDispersionPolynomial B β u a‖ ^ 2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.normTwist, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.correctedDispersionPolynomial