MetaplecticLocalEuler.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Finite versions of the absolute local Euler sum in the Voronoi formula, including the actual squarefree and supported ideal exponents.

def OAI.CubicFirstMoment.metaplecticPrimeWeight line 13
lemma OAI.CubicFirstMoment.metaplecticPrimeWeight_nonneg line 18
lemma OAI.CubicFirstMoment.metaplecticPrimeWeight_sum line 23
lemma OAI.CubicFirstMoment.metaplecticPrimeWeight_eq line 30
Source documentation
The local summand is exactly the common-prime factor, times the square-root coefficient growth, times the inverse norm power.
```
lemma metaplecticPrimeWeight_eq {p : ℝ} (hp : 0 < p) (σ : ℝ) (e : Fin 2) (k : ℕ) :
    metaplecticPrimeWeight p σ e k =
      (if e.val+k = 0 then 1 else p)*p^((k:ℝ)/2)*
        p^(-((e.val:ℝ)+3*k)*(1+σ)) := by
…
```
Mentions: OAI.CubicFirstMoment.metaplecticPrimeWeight
lemma OAI.CubicFirstMoment.metaplecticPrimeWeight_box line 58
lemma OAI.CubicFirstMoment.metaplectic_local_code_bound line 69
def OAI.CubicFirstMoment.metaplecticIdealLocalWeight line 93
Source documentation
The absolute supported-prime factor in terms of genuine ideal exponents. The first ideal is squarefree; the second carries the cubes.
```
def metaplecticIdealLocalWeight (S : Finset EisensteinIdealPrime)
    (σ : ℝ) (μ ν : EisensteinIdealExponent) : ℝ :=
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent
theorem OAI.CubicFirstMoment.metaplectic_ideal_local_sum line 102
Source documentation
Arbitrary finite sets of supported pairs are bounded by the literal Euler product; no norm cutoff or bound on prime-power exponents is used.
```
theorem metaplectic_ideal_local_sum {σ : ℝ} (hσ : 0 < σ)
    (S : Finset EisensteinIdealPrime)
    (T : Finset (EisensteinIdealExponent × EisensteinIdealExponent))
    (hT : ∀ a ∈ T, a.1.support ⊆ S ∧ a.2.support ⊆ S ∧ ∀ p, a.1 p ≤ 1) :
    (∑ a ∈ T, metaplecticIdealLocalWeight S σ a.1 a.2) ≤
      ∏ p ∈ S, metaplecticLocalEuler (normNat (idealPrimeRepresentative p)) σ := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.metaplecticIdealLocalWeight, OAI.CubicFirstMoment.metaplecticLocalEuler, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.idealPrimeRepresentative
theorem OAI.CubicFirstMoment.metaplectic_ideal_euler_small_power line 147
Source documentation
The local product has subpower growth in any ambient ideal.
```
theorem metaplectic_ideal_euler_small_power {ε σ : ℝ} (hε : 0 < ε) (hσ : 0 < σ) :
    ∃ C : ℝ, 0 < C ∧ ∀ ρ : EisensteinIdealExponent,
      (∏ p ∈ ρ.support, metaplecticLocalEuler (normNat (idealPrimeRepresentative p)) σ) ≤
        C*idealExponentNorm ρ^ε := by
…
```
Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.metaplecticLocalEuler, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.idealPrimeRepresentative, OAI.CubicFirstMoment.idealExponentNorm

theorem OAI.CubicFirstMoment.metaplectic_ideal_local_small_power line 182

Source documentation

The precise supported-prime sum needed for absolute convergence of Voronoi is uniformly bounded by an arbitrary ambient norm power.

theorem metaplectic_ideal_local_small_power {ε σ : ℝ} (hε : 0 < ε) (hσ : 0 < σ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (ρ : EisensteinIdealExponent)
      (T : Finset (EisensteinIdealExponent × EisensteinIdealExponent)),
      (∀ a ∈ T, a.1.support ⊆ ρ.support ∧ a.2.support ⊆ ρ.support ∧ ∀ p, a.1 p ≤ 1) →
      (∑ a ∈ T, metaplecticIdealLocalWeight ρ.support σ a.1 a.2) ≤
        C*idealExponentNorm ρ^ε := by
…

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