IdealEulerExclusion.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Finite Euler exclusions on the complete ideal lattice. The full norm ball includes the ramified prime; excluding it is an explicit choice of prime set, and every rescaling factor is retained.

def OAI.CubicFirstMoment.fullIdealBall line 15
Source documentation
All nonzero ideals of norm at most Y, including ideals above three.
```
def fullIdealBall (Y : ℝ) : Finset EisensteinIdealExponent :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.mem_fullIdealBall line 18
def OAI.CubicFirstMoment.primeSetExponent line 31
Source documentation
The squarefree product of a finite set of prime ideals.
```
def primeSetExponent (S : Finset EisensteinIdealPrime) : EisensteinIdealExponent :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent
lemma OAI.CubicFirstMoment.primeSetExponent_apply line 34
lemma OAI.CubicFirstMoment.primeSetExponent_le_iff line 38
lemma OAI.CubicFirstMoment.ideal_prime_exclusion_indicator line 51
Source documentation
Exact finite inclusion--exclusion for the prime-to-S condition.
```
lemma ideal_prime_exclusion_indicator (S : Finset EisensteinIdealPrime)
    (ν : EisensteinIdealExponent) :
    (if ∀ p ∈ S, ν p = 0 then (1:ℂ) else 0) =
      ∑ T ∈ S.powerset, if primeSetExponent T ≤ ν then (-1:ℂ)^T.card else 0 := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.primeSetExponent
lemma OAI.CubicFirstMoment.idealNorm_shift_mem_iff line 74
lemma OAI.CubicFirstMoment.idealNorm_tsub_mem line 80

lemma OAI.CubicFirstMoment.fullIdealBall_shift_sum line 88

Source documentation

An exact rescaled complete ideal sum for one divisor. Character multiplicativity is explicit, and no Euler factor is silently deleted.

lemma fullIdealBall_shift_sum (δ : EisensteinIdealExponent) (Y : ℝ)
    (χ : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν κ, χ (ν+κ) = χ ν*χ κ) (W : ℝ → ℂ)
    {Z : ℝ} (hZ : 0 < Z) :
    (∑ ν ∈ fullIdealBall Y, if δ ≤ ν then χ ν*W (idealExponentNorm ν/Z) else 0) =
      χ δ * ∑ κ ∈ fullIdealBall (Y/idealExponentNorm δ),
        χ κ*W (idealExponentNorm κ/(Z/idealExponentNorm δ)) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.fullIdealBall, OAI.CubicFirstMoment.idealExponentNorm

theorem OAI.CubicFirstMoment.fullIdealBall_euler_exclusion line 122

Source documentation

Removing any finite set of local Euler factors is a finite sum of complete ideal sums at the exact rescaled lengths. The finite set may include the ramified prime; its norm and character factor are retained.

theorem fullIdealBall_euler_exclusion (S : Finset EisensteinIdealPrime)
    (Y : ℝ) (χ : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν κ, χ (ν+κ) = χ ν*χ κ) (W : ℝ → ℂ)
    {Z : ℝ} (hZ : 0 < Z) :
    (∑ ν ∈ fullIdealBall Y, if ∀ p ∈ S, ν p = 0 then χ ν*W (idealExponentNorm ν/Z) else 0) =
      ∑ T ∈ S.powerset, (-1:ℂ)^T.card*χ (primeSetExponent T)*
        ∑ κ ∈ fullIdealBall (Y/idealExponentNorm (primeSetExponent T)),
          χ κ*W (idealExponentNorm κ/(Z/idealExponentNorm (primeSetExponent T))) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.fullIdealBall, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.primeSetExponent

lemma OAI.CubicFirstMoment.compactSupport_upper_cutoff line 156
lemma OAI.CubicFirstMoment.ideal_smooth_tsum_eq_ball line 169
Source documentation
Compact norm support makes the complete ideal sum literally finite; no analytic convergence hypothesis is required for this reduction.
```
lemma ideal_smooth_tsum_eq_ball (χ : EisensteinIdealExponent → ℂ) (W : ℝ → ℂ)
    {B Z : ℝ} (hZ : 0 < Z) (hW : ∀ x : ℝ, B < x → W x = 0) :
    (∑' ν, χ ν*W (idealExponentNorm ν/Z)) =
      ∑ ν ∈ fullIdealBall (B*Z), χ ν*W (idealExponentNorm ν/Z) := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.fullIdealBall

theorem OAI.CubicFirstMoment.smooth_ideal_euler_exclusion line 181

Source documentation

The actual complete smooth ideal sum, with finite Euler exclusions. In particular, selecting the ramified prime in S restores or removes its local factor through this formula with its exact norm and character value.

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

Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.primeSetExponent

lemma OAI.CubicFirstMoment.idealExponentNorm_zero line 203

theorem OAI.CubicFirstMoment.smooth_ideal_single_prime_exclusion line 208

Source documentation

The single local factor, applicable in particular to the prime above three: the omitted factor is restored at exactly Z/N(p).

theorem smooth_ideal_single_prime_exclusion (p : EisensteinIdealPrime)
    (χ : EisensteinIdealExponent → ℂ) (hχ0 : χ 0 = 1)
    (hχ : ∀ ν κ, χ (ν+κ) = χ ν*χ κ) (W : ℝ → ℂ) (hW : HasCompactSupport W)
    {Z : ℝ} (hZ : 0 < Z) :
    (∑' ν, if ν p = 0 then χ ν*W (idealExponentNorm ν/Z) else 0) =
      (∑' ν, χ ν*W (idealExponentNorm ν/Z)) -
      χ (Finsupp.single p 1)*
        ∑' ν, χ ν*W (idealExponentNorm ν/(Z/(normNat (idealPrimeRepresentative p):ℝ))) := by
…

Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.idealPrimeRepresentative