OAI/NumberTheory/CubicMoment/Transform/MetaplecticCriticalKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

At the critical line the angular Gamma quotient has modulus one. Thus the actual translated Mellin kernel has one common integrable weight, independent of height and of the retained frequency polynomial.

  1. lemma OAI.CubicFirstMoment.continuous_metaplecticGamma_half line 14
  2. def OAI.CubicFirstMoment.metaplecticCriticalKernel line 27
  3. lemma OAI.CubicFirstMoment.norm_metaplecticCriticalKernel line 33
  4. lemma OAI.CubicFirstMoment.continuous_metaplecticCriticalKernel line 40
  5. lemma OAI.CubicFirstMoment.metaplectic_mellin_half_integrable line 53
  6. lemma OAI.CubicFirstMoment.metaplecticCriticalKernel_integrable line 62
  7. theorem OAI.CubicFirstMoment.metaplectic_critical_kernel_mean line 81

    Source documentation

    A uniform translated polynomial mean passes through the literal critical-line Gamma kernel with the L1 mass of the actual Mellin transform.

    theorem metaplectic_critical_kernel_mean (ℓ : ℤ) (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) (c : ℝ) (P : ℝ → ℂ) (hP : Continuous P)
    {T B : ℝ} (hT : 0 < T)
    (hmean : ∀ τ : ℝ, (∫ t in T..2*T, ‖P (τ-t)‖)/T ≤ B) :
    (∫ t in T..2*T, ‖∫ τ : ℝ, metaplecticCriticalKernel ℓ W c P τ t‖)/T ≤
      B*(∫ τ : ℝ, ‖mellin W ((1/2:ℂ)+(τ:ℂ)*Complex.I)‖) := by
…

    Mentions: OAI.CubicFirstMoment.metaplecticCriticalKernel