OAI/NumberTheory/CubicMoment/Estimates/RieszHeatKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Laplace representations of the two radial powers in the Riesz calculation.

  1. lemma OAI.CubicFirstMoment.laplace_rpow line 11
  2. lemma OAI.CubicFirstMoment.integrable_laplace_rpow line 18
  3. lemma OAI.CubicFirstMoment.riesz_gaussian_representation line 27

    Source documentation

    The singular power is a convergent integral of Gaussians away from zero.

    lemma riesz_gaussian_representation {a : ℝ} (ha : 0 < a) {z : ℂ} (hz : z ≠ 0) :
    (∫ t in Ioi (0:ℝ), t^(a-1)*Real.exp (-t*‖z‖^2)) =
      Real.Gamma a*‖z‖^(-2*a) := by
…
  4. lemma OAI.CubicFirstMoment.inverse_gaussian_moment line 46

    Source documentation

    The inverted Gaussian moment is the dual radial power.

    lemma inverse_gaussian_moment {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    (∫ t in Ioi (0:ℝ), t^(-a-1)*Real.exp (-b/t)) = Real.Gamma a*b^(-a) := by
…