MetaplecticCompletionCoefficient.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The completed formal coefficients are exactly the actual primary Gauss cube-divisor coefficients, including the positive angular index and the height multiplier.

lemma OAI.CubicFirstMoment.theta_cube_index line 13
lemma OAI.CubicFirstMoment.mellinPhase_cube_norm line 18
lemma OAI.CubicFirstMoment.metaplecticCompletionWeight_phase line 26
lemma OAI.CubicFirstMoment.metaplectic_completion_factor line 37
theorem OAI.CubicFirstMoment.metaplectic_completed_primary_coefficient line 54
Source documentation
Completing the actual Gauss ideal series gives exactly the literal primary cube fiber used by the Voronoi formula.
```
theorem metaplectic_completed_primary_coefficient
    (r : Eisenstein) (ℓ : ℤ) (t : ℝ)
    {b : Eisenstein} (hb : primary b) {F : ℝ} (hbF : norm b ≤ F) :
    MvPowerSeries.coeff (idealExponentOf b)
      (cubeCompletionSeries (metaplecticPrimeCompletionWeights r ℓ t)*
        metaplecticGaussIdealSeries r ℓ t) =
      ∑ n ∈ primaryCubeFiber F b,
        metaplecticPrimalCoefficient r ℓ (fun _ => 1) 1 (n 0,n 1)*
          mellinPhase t (norm (metaplecticCubeProduct (n 0,n 1))) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.cubeCompletionSeries, OAI.CubicFirstMoment.metaplecticPrimeCompletionWeights, OAI.CubicFirstMoment.metaplecticGaussIdealSeries, OAI.CubicFirstMoment.primaryCubeFiber, OAI.CubicFirstMoment.metaplecticPrimalCoefficient, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.metaplecticCubeProduct