MetaplecticRetainedSupport.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Choose the literal published support representation once for each nonzero retained coefficient. The resulting finite code set decodes injectively to the original frequency set.

abbrev OAI.CubicFirstMoment.MetaplecticSupportPrefix line 14
abbrev OAI.CubicFirstMoment.MetaplecticRetainedCode line 17
def OAI.CubicFirstMoment.metaplecticDivisorPrimary line 20
def OAI.CubicFirstMoment.metaplecticPrefixArgument line 23
def OAI.CubicFirstMoment.metaplecticRetainedDecode line 27
lemma OAI.CubicFirstMoment.metaplecticNormalizedDualCoefficient_zero line 31

theorem OAI.CubicFirstMoment.metaplectic_retained_support_partition line 41

Source documentation

The index stores only genuine supported factors. Neither a free coefficient bound nor a moment estimate is included in this reindexing.

theorem metaplectic_retained_support_partition
    {a : Eisenstein → MetaplecticDualArgument → ℂ} (ha : MetaplecticCoefficientBounds a) :
    ∃ C : ℝ, 0 < C ∧ ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ S : Finset (MetaplecticDualArgument × PrimaryArgument),
      ∃ T : Finset (MetaplecticRetainedCode r),
        (∀ z ∈ T, metaplecticRetainedDecode r z ∈ S ∧
          (∃ k : ℕ, z.2.1.2.2.2.val ∣ r^k) ∧ IsCoprime z.2.2.val r ∧
          Squarefree (z.2.1.2.2.1.val*z.2.2.val) ∧
          ‖a r (metaplecticRetainedDecode r z).1‖ ≤
            C*3^((max ((z.2.1.1:ℤ)-1) 0:ℤ)/3:ℝ)*Real.sqrt (norm z.2.1.2.2.2)) ∧
        ∀ (ℓ : ℤ) (t : ℝ),
          (∑ nd ∈ S, metaplecticNormalizedDualCoefficient a r ℓ nd*
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.MetaplecticCoefficientBounds, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.PrimaryArgument, OAI.CubicFirstMoment.MetaplecticRetainedCode, OAI.CubicFirstMoment.metaplecticRetainedDecode, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticNormalizedDualCoefficient