ShortMoebiusPolynomials.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

The short ideal convolution identity evaluated on actual primary character polynomials. All sums below are finite divisor sums.

def OAI.CubicFirstMoment.idealPrimaryGenerator line 15
Source documentation
Canonical primary generator on the ideals prime to three. We use it only for exponent vectors below an actual primary principal ideal.
```
def idealPrimaryGenerator (ν : EisensteinIdealExponent) : Eisenstein :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.idealExponentGenerator_dvd_of_le line 18
lemma OAI.CubicFirstMoment.idealPrimaryGenerator_primary line 23
lemma OAI.CubicFirstMoment.idealPrimaryGenerator_at_element line 30
lemma OAI.CubicFirstMoment.idealPrimaryGenerator_norm line 35
lemma OAI.CubicFirstMoment.idealPrimaryGenerator_add line 42
def OAI.CubicFirstMoment.idealCharacterCoeff line 55
Source documentation
Real ideal coefficients evaluated against a character of primary Eisenstein elements.
```
def idealCharacterCoeff (A : EisensteinArithmeticFunction) (χ : Eisenstein → ℂ)
    (ν : EisensteinIdealExponent) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.idealCharacterCoeff_mul line 59
lemma OAI.CubicFirstMoment.idealCharacterCoeff_add line 79
lemma OAI.CubicFirstMoment.idealCharacterCoeff_sub line 84

theorem OAI.CubicFirstMoment.shortMoebius_character_identity line 91

Source documentation

The actual von Mangoldt character coefficient splits into a two-factor and a four-factor ideal convolution throughout the sharp norm range.

theorem shortMoebius_character_identity {F : ℝ} (hF : 0 ≤ F)
    {a : Eisenstein} (ha : primary a) (hNa : norm a ≤ F)
    (χ : Eisenstein → ℂ)
    (hχ : ∀ x y, primary x → primary y → χ (x*y) = χ x*χ y) :
    ((MvPowerSeries.coeff (idealExponentOf a) idealVonMangoldt : ℝ) : ℂ)*χ a =
      2 * (∑ p ∈ Finset.HasAntidiagonal.antidiagonal (idealExponentOf a),
        idealCharacterCoeff (shortIdealMoebius F) χ p.1 * idealCharacterCoeff idealLogNorm χ p.2) -
      (∑ p ∈ Finset.HasAntidiagonal.antidiagonal (idealExponentOf a),
        idealCharacterCoeff (shortIdealMoebius F*shortIdealMoebius F*idealZeta) χ p.1 *
          idealCharacterCoeff idealLogNorm χ p.2) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.idealCharacterCoeff, OAI.CubicFirstMoment.shortIdealMoebius, OAI.CubicFirstMoment.idealLogNorm, OAI.CubicFirstMoment.idealZeta

lemma OAI.CubicFirstMoment.idealCharacterCoeff_four line 121

Source documentation

Four actual ideal factors, with no convolution coefficient left hidden. The antidiagonal constraints encode their exact product, before Mellin separation of a norm weight.

lemma idealCharacterCoeff_four {a : Eisenstein} (ha : primary a)
    (A B C D : EisensteinArithmeticFunction) (χ : Eisenstein → ℂ)
    (hχ : ∀ x y, primary x → primary y → χ (x*y) = χ x*χ y)
    {ν : EisensteinIdealExponent} (hν : ν ≤ idealExponentOf a) :
    idealCharacterCoeff (A*B*C*D) χ ν =
      ∑ p ∈ Finset.HasAntidiagonal.antidiagonal ν,
        (∑ q ∈ Finset.HasAntidiagonal.antidiagonal p.1,
          (∑ r ∈ Finset.HasAntidiagonal.antidiagonal q.1,
            idealCharacterCoeff A χ r.1*idealCharacterCoeff B χ r.2)*
          idealCharacterCoeff C χ q.2)*idealCharacterCoeff D χ p.2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.idealCharacterCoeff

lemma OAI.CubicFirstMoment.idealCharacterCoeff_zeta line 146
lemma OAI.CubicFirstMoment.idealCharacterCoeff_log line 150
lemma OAI.CubicFirstMoment.shortIdeal_characterCoeff_support line 157
Source documentation
Every nonzero short Möbius factor has the required half-length and squarefree ideal support. These are derived support conditions.
```
lemma shortIdeal_characterCoeff_support {F : ℝ} {χ : Eisenstein → ℂ}
    {ν : EisensteinIdealExponent}
    (h : idealCharacterCoeff (shortIdealMoebius F) χ ν ≠ 0) :
    idealExponentNorm ν ≤ Real.sqrt F ∧ ∀ p, ν p ≤ 1 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealCharacterCoeff, OAI.CubicFirstMoment.shortIdealMoebius, OAI.CubicFirstMoment.idealExponentNorm
lemma OAI.CubicFirstMoment.shortIdeal_characterCoeff_norm_le_one line 170
lemma OAI.CubicFirstMoment.logIdeal_characterCoeff_norm_le line 179

theorem OAI.CubicFirstMoment.shortMoebius_mixedCubic_identity line 188

Source documentation

Evaluation at the actual mixed cubic character used in the exceptional moments; its multiplicativity is already proved arithmetically.

theorem shortMoebius_mixedCubic_identity {F : ℝ} (hF : 0 ≤ F)
    {a q₁ q₂ : Eisenstein} (ha : primary a) (hNa : norm a ≤ F)
    (h₁ : primary q₁) (h₂ : primary q₂) :
    ((MvPowerSeries.coeff (idealExponentOf a) idealVonMangoldt : ℝ) : ℂ)*mixedCubic q₁ q₂ a =
      2 * (∑ p ∈ Finset.HasAntidiagonal.antidiagonal (idealExponentOf a),
        idealCharacterCoeff (shortIdealMoebius F) (mixedCubic q₁ q₂) p.1 *
        idealCharacterCoeff idealLogNorm (mixedCubic q₁ q₂) p.2) -
      (∑ p ∈ Finset.HasAntidiagonal.antidiagonal (idealExponentOf a),
        (∑ q ∈ Finset.HasAntidiagonal.antidiagonal p.1,
          (∑ r ∈ Finset.HasAntidiagonal.antidiagonal q.1,
            idealCharacterCoeff (shortIdealMoebius F) (mixedCubic q₁ q₂) r.1*
            idealCharacterCoeff (shortIdealMoebius F) (mixedCubic q₁ q₂) r.2)*
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.mixedCubic, OAI.CubicFirstMoment.idealCharacterCoeff, OAI.CubicFirstMoment.shortIdealMoebius, OAI.CubicFirstMoment.idealLogNorm

def OAI.CubicFirstMoment.shortTypeITwo line 213
Source documentation
The two-factor Type I term furnished by the short inverse.
```
def shortTypeITwo (F : ℝ) (χ : Eisenstein → ℂ) (ν : EisensteinIdealExponent) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent
def OAI.CubicFirstMoment.shortTypeIFour line 218
Source documentation
The four-factor Type I term, keeping both short Möbius factors explicit.
```
def shortTypeIFour (F : ℝ) (χ : Eisenstein → ℂ) (ν : EisensteinIdealExponent) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.shortMoebius_character_identity_expanded line 226
theorem OAI.CubicFirstMoment.shortMoebius_weighted_finite_sum line 243
Source documentation
Exact finite weighted Type I decomposition on actual primary elements. No separation of the product norm, dyadic partition, or analytic bound is assumed here; those operations apply to this proved identity.
```
theorem shortMoebius_weighted_finite_sum {F : ℝ} (hF : 0 ≤ F)
    (S : Finset Eisenstein) (hS : ∀ a ∈ S, primary a ∧ norm a ≤ F)
    (W : ℝ → ℂ) (χ : Eisenstein → ℂ)
    (hχ : ∀ x y, primary x → primary y → χ (x*y) = χ x*χ y) :
    (∑ a ∈ S, W (norm a)*((MvPowerSeries.coeff (idealExponentOf a) idealVonMangoldt : ℝ) : ℂ)*χ a) =
      2*(∑ a ∈ S, W (norm a)*shortTypeITwo F χ (idealExponentOf a)) -
        ∑ a ∈ S, W (norm a)*shortTypeIFour F χ (idealExponentOf a) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.shortTypeITwo, OAI.CubicFirstMoment.shortTypeIFour