OAI/NumberTheory/CubicMoment/Transform/MetaplecticTransformDecay.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact far-left height bound for the shifted metaplectic transform. The power of the height is 4m, proved by finite Gamma recurrence.

  1. def OAI.CubicFirstMoment.metaplecticShiftTransform line 12
  2. lemma OAI.CubicFirstMoment.metaplecticShiftTransform_zero line 18
  3. theorem OAI.CubicFirstMoment.metaplecticShiftTransform_far_left line 24

    Source documentation

    Uniform in the scale and height; the constant depends only on the fixed angular mode, weight and chosen far-left line.

    theorem metaplecticShiftTransform_far_left (ℓ : ℤ) (m : ℕ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ v : ℝ, 0 < v → ∀ t : ℝ,
      ‖metaplecticShiftTransform ℓ W (1/2-(m:ℝ)) v t‖ ≤
        C*v^(1/2-(m:ℝ))*(1+|t|)^(4*m) := by
…

    Mentions: OAI.CubicFirstMoment.metaplecticShiftTransform