MetaplecticDualScaling.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact scaling of the actual angular Voronoi terms.

lemma OAI.CubicFirstMoment.norm_complexAngular line 11
lemma OAI.CubicFirstMoment.metaplectic_argument_power line 15
lemma OAI.CubicFirstMoment.metaplectic_dual_scalar line 37

lemma OAI.CubicFirstMoment.metaplecticDualTerm_norm_le line 58

Source documentation

The actual dual term has the separated coefficient/d-variable majorant supplied by the published formula and the derived transform bound.

lemma metaplecticDualTerm_norm_le
    (a : Eisenstein → MetaplecticDualArgument → ℂ) {r : Eisenstein} (hr : primary r)
    (ℓ : ℤ) (W : ℝ → ℂ) {σ X C : ℝ} (hX : 0 < X) (hC : 0 ≤ C)
    (hW : ∀ v : ℝ, 0 < v → ‖metaplecticTransform ℓ W σ v‖ ≤ C*v^(-σ))
    (nd : MetaplecticDualArgument × PrimaryArgument) :
    ‖metaplecticDualTerm a r ℓ W σ X nd‖ ≤
      (C*((2*Real.pi)^(-4*σ)*X^(-σ)*norm r^(2*σ)))*
        metaplecticCoefficientMassTerm a r σ nd.1*norm nd.2^(-5/2-3*σ) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.metaplecticTransform, OAI.CubicFirstMoment.PrimaryArgument, OAI.CubicFirstMoment.metaplecticDualTerm, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticCoefficientMassTerm