MetaplecticVoronoi.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

The literal level/angular Voronoi input of Dunn--Radziwill, arXiv:2109.07463v3, Proposition 5.3, equations (5.79)--(5.82), pp.33--34. The raw formula is kept separate from its proved Gauss/phase normalization. The index n below denotes the actual frequency n / lambda; zero is excluded. No estimate for a completed sum is assumed.

abbrev OAI.CubicFirstMoment.MetaplecticDualArgument line 18
def OAI.CubicFirstMoment.metaplecticFrequency line 20
lemma OAI.CubicFirstMoment.metaplecticFrequency_ne_zero line 23
def OAI.CubicFirstMoment.complexAngular line 27
lemma OAI.CubicFirstMoment.complexAngular_coe line 29
def OAI.CubicFirstMoment.metaplecticGammaQuotient line 32
def OAI.CubicFirstMoment.metaplecticTransform line 37
Source documentation
Equation (5.81), parameterized on the vertical line Re s = -sigma.
```
def metaplecticTransform (ℓ : ℤ) (W : ℝ → ℂ) (σ v : ℝ) : ℂ :=
…
```
def OAI.CubicFirstMoment.metaplecticLocalCoefficient line 44
Source documentation
Equation (5.68), written as its exact squarefree Euler product.
```
def metaplecticLocalCoefficient (r : Eisenstein) (n : MetaplecticDualArgument) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument
def OAI.CubicFirstMoment.metaplecticCommonNorm line 48
lemma OAI.CubicFirstMoment.norm_metaplecticLocalCoefficient_le line 51
def OAI.CubicFirstMoment.MetaplecticCoefficientBounds line 72
Source documentation
Support read from (5.79), avoiding the repeated ramified exponent in the printed (5.67). The coefficient bound follows from (5.7), (5.13), (5.14). The two supported factors may have arbitrarily large exponents.
```
def MetaplecticCoefficientBounds
    (a : Eisenstein → MetaplecticDualArgument → ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument
def OAI.CubicFirstMoment.metaplecticDualTerm line 83
def OAI.CubicFirstMoment.metaplecticRawCompleted line 95
def OAI.CubicFirstMoment.metaplecticCompleted line 102
def OAI.CubicFirstMoment.metaplecticRawMain line 109
def OAI.CubicFirstMoment.metaplecticMain line 115
def OAI.CubicFirstMoment.metaplecticRawPrefactor line 121
def OAI.CubicFirstMoment.metaplecticPrefactor line 125
def OAI.CubicFirstMoment.MetaplecticVoronoiInput line 132
Source documentation
The only new analytic identity assumed here is DR Proposition 5.3. Its absolute convergence is part of the published proof of (5.80). The input retains the actual transform, frequency lattice, local Euler coefficients and global theta-coefficient support.
```
def MetaplecticVoronoiInput
    (a : Eisenstein → MetaplecticDualArgument → ℂ) : Prop :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument
lemma OAI.CubicFirstMoment.metaplecticCompleted_eq_raw line 142
lemma OAI.CubicFirstMoment.gauss_mul_conj_unnormalized line 153
lemma OAI.CubicFirstMoment.angular_conjugate_ratio line 163
lemma OAI.CubicFirstMoment.metaplecticMain_normalization line 177
lemma OAI.CubicFirstMoment.metaplecticPrefactor_normalization line 198
theorem OAI.CubicFirstMoment.metaplectic_angular_voronoi line 213
Source documentation
The manuscript's normalized angular Voronoi identity, derived from the published raw formula. The theta coefficients remain explicit.
```
theorem metaplectic_angular_voronoi
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (hV : MetaplecticVoronoiInput a)
    {r : Eisenstein} (hr : primary r) (hs : Squarefree r) (ℓ : ℤ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {X σ : ℝ} (hX : 0 < X) (hσ : 0 < σ)
    (hσ' : σ < 1/10000) :
    metaplecticCompleted r ℓ W X = metaplecticMain r ℓ W X+
      metaplecticPrefactor r ℓ*∑' nd, metaplecticDualTerm a r ℓ W σ X nd := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticVoronoiInput, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticCompleted, OAI.CubicFirstMoment.metaplecticMain, OAI.CubicFirstMoment.metaplecticPrefactor, OAI.CubicFirstMoment.metaplecticDualTerm
lemma OAI.CubicFirstMoment.norm_metaplecticPrefactor line 226
lemma OAI.CubicFirstMoment.norm_metaplecticGammaQuotient_critical line 235
Source documentation
On the critical line the two numerator Gamma factors are the conjugates of the denominator factors, so the angular quotient has norm one.
```
lemma norm_metaplecticGammaQuotient_critical (ℓ : ℤ) (t : ℝ) :
    ‖metaplecticGammaQuotient ℓ ((1/2:ℝ)+(t:ℂ)*Complex.I)‖ = 1 := by
…
```
Mentions: OAI.CubicFirstMoment.metaplecticGammaQuotient