OAI/NumberTheory/CubicMoment/Estimates/CubicWhittakerConvergence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Absolute Mellin convergence of the fixed cubic Whittaker kernel.

  1. lemma OAI.CubicFirstMoment.cubicThetaWhittaker_mellinConvergent line 11
  2. lemma OAI.CubicFirstMoment.cubicThetaWhittaker_scaled_mellinConvergent line 25
  3. lemma OAI.CubicFirstMoment.cubicWhittaker_norm_mass_scale line 32

    Source documentation

    The norm mass changes by the exact Mellin scaling power.

    lemma cubicWhittaker_norm_mass_scale (σ : ℝ) {r : ℝ} (hr : 0 < r) :
    (∫ v in Ioi (0:ℝ), v^(σ-1)*‖cubicThetaWhittaker (r*v)‖) =
      r^(-σ)*(∫ v in Ioi (0:ℝ), v^(σ-1)*‖cubicThetaWhittaker v‖) := by
…

    Mentions: OAI.CubicFirstMoment.cubicThetaWhittaker