PrimeToThreeIdeals.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual ramified Euler restriction in primary-element polynomials. Prime-to-three ideals are identified arithmetically, then the complete ideal-sum exclusion formula restores their missing local factors.

lemma OAI.CubicFirstMoment.idealPrime_dvd_iff line 14
lemma OAI.CubicFirstMoment.isCoprime_iff_idealExponent_disjoint line 34
Source documentation
Coprimality is exactly disjoint prime-ideal support, with no omitted ramified prime or assumption of squarefreeness.
```
lemma isCoprime_iff_idealExponent_disjoint {a b : Eisenstein} (ha : a ≠ 0) (hb : b ≠ 0) :
    IsCoprime a b ↔ ∀ p : EisensteinIdealPrime, idealExponentOf a p = 0 ∨ idealExponentOf b p = 0 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.idealExponentOf
def OAI.CubicFirstMoment.ramifiedIdealPrimes line 60
Source documentation
All prime ideals dividing the rational integer three.
```
def ramifiedIdealPrimes : Finset EisensteinIdealPrime :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime
lemma OAI.CubicFirstMoment.idealGenerator_coprime_three_iff line 63
theorem OAI.CubicFirstMoment.idealPrimaryGenerator_primary_iff line 78
Source documentation
Primary normalization succeeds exactly on the ideals prime to three.
```
theorem idealPrimaryGenerator_primary_iff (ν : EisensteinIdealExponent) :
    primary (idealPrimaryGenerator ν) ↔ ∀ p ∈ ramifiedIdealPrimes, ν p = 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealPrimaryGenerator, OAI.CubicFirstMoment.ramifiedIdealPrimes
lemma OAI.CubicFirstMoment.primaryIdealBall_eq_full_filter line 88
theorem OAI.CubicFirstMoment.primaryIdealPolynomial_eq_ramified_filter line 97
Source documentation
The primary polynomial is the complete ideal polynomial with its actual ramified Euler factors deleted.
```
theorem primaryIdealPolynomial_eq_ramified_filter (Y : ℝ) (A : EisensteinArithmeticFunction)
    (χ : Eisenstein → ℂ) :
    primaryIdealPolynomial Y A χ = ∑ ν ∈ fullIdealBall Y,
      if ∀ p ∈ ramifiedIdealPrimes, ν p = 0 then idealCharacterCoeff A χ ν else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.fullIdealBall, OAI.CubicFirstMoment.ramifiedIdealPrimes, OAI.CubicFirstMoment.idealCharacterCoeff

theorem OAI.CubicFirstMoment.primary_ideal_smooth_euler line 105

Source documentation

Exact restoration of the missing ramified Euler factors for a complete smooth Hecke-ideal character sum.

theorem primary_ideal_smooth_euler (χ : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν κ, χ (ν+κ) = χ ν*χ κ) (W : ℝ → ℂ) (hW : HasCompactSupport W)
    {Z : ℝ} (hZ : 0 < Z) :
    (∑' ν, if primary (idealPrimaryGenerator ν) then χ ν*W (idealExponentNorm ν/Z) else 0) =
      ∑ T ∈ ramifiedIdealPrimes.powerset, (-1:ℂ)^T.card*χ (primeSetExponent T)*
        ∑' κ, χ κ*W (idealExponentNorm κ/(Z/idealExponentNorm (primeSetExponent T))) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealPrimaryGenerator, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.primeSetExponent

lemma OAI.CubicFirstMoment.primaryIdealBall_sum_eq_elements line 114
lemma OAI.CubicFirstMoment.primary_ideal_smooth_tsum_eq_ball line 122
lemma OAI.CubicFirstMoment.primary_element_smooth_tsum_eq_ball line 132
theorem OAI.CubicFirstMoment.primary_element_ideal_smooth_eq line 152
Source documentation
The original primary-element smooth polynomial is exactly the smooth ideal sum with the actual primes above three excluded.
```
theorem primary_element_ideal_smooth_eq (χ : EisensteinIdealExponent → ℂ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) {Z : ℝ} (hZ : 0 < Z) :
    (∑' a : Eisenstein, if primary a then χ (idealExponentOf a)*W (norm a/Z) else 0) =
      ∑' ν, if primary (idealPrimaryGenerator ν) then χ ν*W (idealExponentNorm ν/Z) else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealPrimaryGenerator, OAI.CubicFirstMoment.idealExponentNorm

theorem OAI.CubicFirstMoment.primary_element_smooth_euler line 165

Source documentation

The actual primary-element sum with all omitted ramified factors restored as complete ideal sums at the exact rescaled lengths.

theorem primary_element_smooth_euler (χ : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν κ, χ (ν+κ) = χ ν*χ κ) (W : ℝ → ℂ) (hW : HasCompactSupport W)
    {Z : ℝ} (hZ : 0 < Z) :
    (∑' a : Eisenstein, if primary a then χ (idealExponentOf a)*W (norm a/Z) else 0) =
      ∑ T ∈ ramifiedIdealPrimes.powerset, (-1:ℂ)^T.card*χ (primeSetExponent T)*
        ∑' κ, χ κ*W (idealExponentNorm κ/(Z/idealExponentNorm (primeSetExponent T))) :=
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeSetExponent, OAI.CubicFirstMoment.idealExponentNorm