MetaplecticPrimaryCompletion.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The expanded ideal kernel is exactly a primary cube-divisor sum. This reindexing retains the finite norm cutoff and arbitrary complex coefficients; no analytic summability assumption enters the inversion.

def OAI.CubicFirstMoment.weightedCubeSeries line 14
lemma OAI.CubicFirstMoment.weightedCubeSeries_coeff line 17
lemma OAI.CubicFirstMoment.primary_cube line 23
lemma OAI.CubicFirstMoment.primary_cube_injective line 26
lemma OAI.CubicFirstMoment.weightedCubeSeries_nonzero_primary line 36
def OAI.CubicFirstMoment.primaryCubeFiber line 54
theorem OAI.CubicFirstMoment.weightedCubeSeries_product_primary line 60
Source documentation
Multiplying by the expanded series is a literal sum over primary cube divisors, with every argument bounded by the original norm cutoff.
```
theorem weightedCubeSeries_product_primary
    (B A : ComplexIdealSeries) (x : EisensteinIdealPrime → ℂ)
    {b : Eisenstein} (hb : primary b) {F : ℝ} (hbF : norm b ≤ F) :
    MvPowerSeries.coeff (idealExponentOf b) (weightedCubeSeries B x*A) =
      ∑ n ∈ primaryCubeFiber F b,
        ((idealExponentOf (n 0)).prod (fun p k => x p^k)*
          MvPowerSeries.coeff (idealExponentOf (n 0)) B)*
          MvPowerSeries.coeff (idealExponentOf (n 1)) A := by
…
```
Mentions: OAI.CubicFirstMoment.ComplexIdealSeries, OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.weightedCubeSeries, OAI.CubicFirstMoment.primaryCubeFiber