MetaplecticPrimaryInverse.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The exact inverse completion at primary elements. The formal Euler inverse is reindexed onto the literal primary cube-divisor fibers, with its actual Möbius, angular and height weights.

def OAI.CubicFirstMoment.metaplecticPrimeCompletionWeights line 14
lemma OAI.CubicFirstMoment.weightedInverseCompletion_eq line 18
theorem OAI.CubicFirstMoment.metaplectic_primary_inverse_coefficient line 25
Source documentation
No cube-divisor is omitted: the finite bound follows from divisibility of the original primary element, not from an additional support hypothesis.
```
theorem metaplectic_primary_inverse_coefficient
    (r : Eisenstein) (ℓ : ℤ) (t : ℝ) (A : ComplexIdealSeries)
    {b : Eisenstein} (hb : primary b) {F : ℝ} (hbF : norm b ≤ F) :
    MvPowerSeries.coeff (idealExponentOf b) A =
      ∑ n ∈ primaryCubeFiber F b,
        ((idealMoebius (n 0):ℂ)*metaplecticCompletionWeight r ℓ t (n 0))*
          MvPowerSeries.coeff (idealExponentOf (n 1))
            (cubeCompletionSeries (metaplecticPrimeCompletionWeights r ℓ t)*A) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ComplexIdealSeries, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.primaryCubeFiber, OAI.CubicFirstMoment.idealMoebius, OAI.CubicFirstMoment.metaplecticCompletionWeight, OAI.CubicFirstMoment.cubeCompletionSeries, OAI.CubicFirstMoment.metaplecticPrimeCompletionWeights
theorem OAI.CubicFirstMoment.metaplectic_primary_weighted_inverse line 56
Source documentation
Any finite smooth norm weight may be applied after the actual primary inverse identity, without a rearrangement of an infinite series.
```
theorem metaplectic_primary_weighted_inverse
    (r : Eisenstein) (ℓ : ℤ) (t : ℝ) (A : ComplexIdealSeries)
    (F : ℝ) (W : ℝ → ℂ) :
    (∑ b ∈ primaryElementBall F, W (norm b)*MvPowerSeries.coeff (idealExponentOf b) A) =
      ∑ b ∈ primaryElementBall F, W (norm b)*
        ∑ n ∈ primaryCubeFiber F b,
          ((idealMoebius (n 0):ℂ)*metaplecticCompletionWeight r ℓ t (n 0))*
            MvPowerSeries.coeff (idealExponentOf (n 1))
              (cubeCompletionSeries (metaplecticPrimeCompletionWeights r ℓ t)*A) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ComplexIdealSeries, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.primaryCubeFiber, OAI.CubicFirstMoment.idealMoebius, OAI.CubicFirstMoment.metaplecticCompletionWeight, OAI.CubicFirstMoment.cubeCompletionSeries, OAI.CubicFirstMoment.metaplecticPrimeCompletionWeights
def OAI.CubicFirstMoment.metaplecticGaussIdealSeries line 70
lemma OAI.CubicFirstMoment.metaplecticGaussIdealSeries_at_primary line 75
theorem OAI.CubicFirstMoment.metaplectic_gauss_primary_inverse line 84
Source documentation
The inverted coefficients are the literal angular Gauss coefficients, including the original norm twist.
```
theorem metaplectic_gauss_primary_inverse
    (r : Eisenstein) (ℓ : ℤ) (t F : ℝ) (W : ℝ → ℂ) :
    (∑ b ∈ primaryElementBall F, W (norm b)*
      (gauss (r*b)*theta ℓ (r*b)*mellinPhase t (norm b))) =
      ∑ b ∈ primaryElementBall F, W (norm b)*
        ∑ n ∈ primaryCubeFiber F b,
          ((idealMoebius (n 0):ℂ)*metaplecticCompletionWeight r ℓ t (n 0))*
            MvPowerSeries.coeff (idealExponentOf (n 1))
              (cubeCompletionSeries (metaplecticPrimeCompletionWeights r ℓ t)*
                metaplecticGaussIdealSeries r ℓ t) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.theta, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.primaryCubeFiber, OAI.CubicFirstMoment.idealMoebius, OAI.CubicFirstMoment.metaplecticCompletionWeight, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.cubeCompletionSeries, OAI.CubicFirstMoment.metaplecticPrimeCompletionWeights, OAI.CubicFirstMoment.metaplecticGaussIdealSeries