OAI/NumberTheory/CubicMoment/Estimates/MellinSmooth.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Analytic properties of the actual compactly supported smooth norm weights. Passing to logarithmic coordinates realizes every vertical Mellin line as a Schwartz Fourier transform.

  1. lemma OAI.CubicFirstMoment.logPullback_compact line 17
  2. def OAI.CubicFirstMoment.mellinLogSchwartz line 28
  3. lemma OAI.CubicFirstMoment.mellinLogSchwartz_apply line 35
  4. lemma OAI.CubicFirstMoment.mellin_frequency_growth line 39
  5. def OAI.CubicFirstMoment.mellinVerticalSchwartz line 49
  6. lemma OAI.CubicFirstMoment.mellinVerticalSchwartz_apply line 56
  7. theorem OAI.CubicFirstMoment.smooth_mellin_vertical_integrable line 65
  8. theorem OAI.CubicFirstMoment.smooth_mellin_vertical_decay line 75
  9. lemma OAI.CubicFirstMoment.smooth_mellin_power_bounds line 90
  10. theorem OAI.CubicFirstMoment.smooth_mellin_convergent line 105
  11. theorem OAI.CubicFirstMoment.smooth_mellin_entire line 112
  12. theorem OAI.CubicFirstMoment.smooth_mellin_inversion line 121

    Source documentation

    The Mellin inversion used for a single norm weight, with convergence and the vertical integral discharged from its actual smooth support.

    theorem smooth_mellin_inversion (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hpos : tsupport W ⊆ Ioi 0) (hsm : ContDiff ℝ ∞ W) (σ : ℝ)
    {x : ℝ} (hx : 0 < x) : mellinInv σ (mellin W) x = W x :=
…