MetaplecticFreeFrequency.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Literal free-variable parametrization of each supported Voronoi block, including the ramified exponent k=0 (j=-1).

lemma OAI.CubicFirstMoment.metaplectic_lambda_ne_zero line 11
def OAI.CubicFirstMoment.metaplecticFreeArgument line 17
lemma OAI.CubicFirstMoment.metaplecticFreeArgument_val line 26
lemma OAI.CubicFirstMoment.metaplecticFreeArgument_frequency line 31
lemma OAI.CubicFirstMoment.metaplecticFreeArgument_injective line 41
lemma OAI.CubicFirstMoment.metaplectic_free_sum_reindex line 53
Source documentation
Within a fixed supported block, the free primary variable indexes exactly the original frequencies, without multiplicity loss.
```
lemma metaplectic_free_sum_reindex (k : ℕ) (ζ : Eisensteinˣ)
    (h h' : PrimaryArgument) (S : Finset MetaplecticDualArgument)
    (w : MetaplecticDualArgument → Eisenstein)
    (hw : ∀ n ∈ S, primary (w n))
    (he : ∀ n ∈ S, n.val = lambdaE^k*ζ.val*h.val*w n*h'.val^3)
    (F : MetaplecticDualArgument → ℂ) :
    (∑ n ∈ S, F n) =
      ∑ b ∈ S.image w, F (metaplecticFreeArgument k ζ h h' b) := by
…
```
Mentions: OAI.CubicFirstMoment.PrimaryArgument, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.lambdaE, OAI.CubicFirstMoment.metaplecticFreeArgument