MetaplecticBlockCoefficient.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual critical-line coefficients of a retained Voronoi block. The free-variable inverse-square-root bound follows from the published coefficient support and the two proved common-divisor bounds.

def OAI.CubicFirstMoment.metaplecticNormalizedDualCoefficient line 16
lemma OAI.CubicFirstMoment.norm_metaplecticNormalizedDualCoefficient_le line 25
lemma OAI.CubicFirstMoment.metaplectic_free_coefficient_sq line 42

lemma OAI.CubicFirstMoment.metaplectic_actual_free_coefficient_sq line 53

Source documentation

All dependence on the free primary element has been extracted as its inverse square root. The coefficient is the actual Voronoi one.

lemma metaplectic_actual_free_coefficient_sq
    {a : Eisenstein → MetaplecticDualArgument → ℂ} {C : ℝ} (hC : 0 ≤ C)
    {r : Eisenstein} (hr : primary r) (d : PrimaryArgument) (ℓ : ℤ)
    (n : MetaplecticDualArgument) {j : ℤ} (hj : -1 ≤ j) (ζ : Eisensteinˣ)
    {h h' w : Eisenstein} (hh : primary h) (hh' : primary h') (hw : primary w)
    (hwr : IsCoprime w r)
    (he : metaplecticFrequency n = traceLambda^j*(ζ.val:ℂ)*(h:ℂ)*(w:ℂ)*(h':ℂ)^3)
    (ha : ‖a r n‖ ≤ C*3^((max j 0:ℤ)/3:ℝ)*Real.sqrt (norm h')) :
    ‖metaplecticNormalizedDualCoefficient a r ℓ (n,d)‖^2 ≤
      (C*3^((max j 0:ℤ)/3:ℝ)*Real.sqrt (norm h')*
        min (norm r) (norm h*norm h') /
        (Real.sqrt ((3:ℝ)^((j+1).toNat-1:ℝ)*norm h*norm h'^3)*norm d))^2/norm w := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.PrimaryArgument, OAI.CubicFirstMoment.metaplecticFrequency, OAI.CubicFirstMoment.traceLambda, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticNormalizedDualCoefficient