OAI/NumberTheory/CubicMoment/Transform/MetaplecticCodePartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact finite partition of the chosen retained frequencies by their supported prefix. The remaining index is the literal primary free variable.

  1. def OAI.CubicFirstMoment.metaplecticCodeFreeSet line 12
  2. lemma OAI.CubicFirstMoment.metaplectic_code_ext line 16
  3. lemma OAI.CubicFirstMoment.metaplectic_decode_of_prefix line 24
  4. lemma OAI.CubicFirstMoment.metaplectic_mem_codeFreeSet line 31
  5. lemma OAI.CubicFirstMoment.metaplectic_codeFreeSet_primary line 42
  6. lemma OAI.CubicFirstMoment.metaplectic_code_prefix_sum line 48
  7. theorem OAI.CubicFirstMoment.metaplectic_code_partition line 62

    Source documentation

    No extra multiplicity is introduced by separating the fixed support parameters from the free primary argument.

    theorem metaplectic_code_partition {r : Eisenstein} (T : Finset (MetaplecticRetainedCode r))
    (F : MetaplecticDualArgument × PrimaryArgument → ℂ) :
    (∑ z ∈ T, F (metaplecticRetainedDecode r z)) =
      ∑ p ∈ T.image metaplecticCodePrefix,
        ∑ w ∈ metaplecticCodeFreeSet T p, F (metaplecticPrefixArgument r p.2 w,p.1) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticRetainedCode, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.PrimaryArgument, OAI.CubicFirstMoment.metaplecticRetainedDecode, OAI.CubicFirstMoment.metaplecticCodePrefix, OAI.CubicFirstMoment.metaplecticCodeFreeSet, OAI.CubicFirstMoment.metaplecticPrefixArgument

  8. lemma OAI.CubicFirstMoment.metaplectic_codeFreeSet_dyad line 79
  9. lemma OAI.CubicFirstMoment.metaplectic_codeFreeSet_length_one line 91