OAI/NumberTheory/CubicMoment/Transform/MetaplecticTransformContour.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Contour motion for the actual angular metaplectic transform. The two fixed shifted Hecke Gamma strip estimates are the same published Stirling input already used for the individual Hecke transforms.

  1. lemma OAI.CubicFirstMoment.metaplecticGamma_shift_factor line 13
  2. lemma OAI.CubicFirstMoment.metaplecticGamma_strip_bound line 30
  3. lemma OAI.CubicFirstMoment.differentiableOn_metaplecticGammaQuotient line 45
  4. lemma OAI.CubicFirstMoment.norm_angularGammaFEQuotient_half line 73
  5. lemma OAI.CubicFirstMoment.norm_metaplecticGamma_half line 87
  6. lemma OAI.CubicFirstMoment.metaplectic_scale_strip line 93
  7. theorem OAI.CubicFirstMoment.metaplectic_transform_contour line 102

    Source documentation

    Exact vertical contour move for the transform integrand. The scale may lie on either side of one.

    theorem metaplectic_transform_contour (ℓ : ℤ) (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {a b v : ℝ} (hab : a ≤ b) (hb : b ≤ 1/2)
    (hv : 0 < v)
    (hm : AngularGammaQuotientStripBound (metaplecticAngularShift ℓ-1/6) a)
    (hp : AngularGammaQuotientStripBound (metaplecticAngularShift ℓ+1/6) a) :
    (∫ t : ℝ, (v:ℂ)^((a:ℂ)+(t:ℂ)*Complex.I)*
      metaplecticGammaQuotient ℓ ((a:ℂ)+(t:ℂ)*Complex.I)*
      mellin W ((a:ℂ)+(t:ℂ)*Complex.I)) =
    ∫ t : ℝ, (v:ℂ)^((b:ℂ)+(t:ℂ)*Complex.I)*
      metaplecticGammaQuotient ℓ ((b:ℂ)+(t:ℂ)*Complex.I)*
      mellin W ((b:ℂ)+(t:ℂ)*Complex.I) := by
…

    Mentions: OAI.CubicFirstMoment.AngularGammaQuotientStripBound, OAI.CubicFirstMoment.metaplecticAngularShift, OAI.CubicFirstMoment.metaplecticGammaQuotient