OAI/NumberTheory/CubicMoment/Estimates/RieszFubini.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Absolute convergence for the Gaussian representation of the Riesz pairing.

  1. lemma OAI.CubicFirstMoment.ae_complex_ne_zero line 13
  2. def OAI.CubicFirstMoment.rieszGaussianWeight line 17
  3. lemma OAI.CubicFirstMoment.rieszGaussianWeight_integral line 20
  4. lemma OAI.CubicFirstMoment.rieszGaussianWeight_nonneg line 29
  5. theorem OAI.CubicFirstMoment.integrable_riesz_gaussian_product line 35

    Source documentation

    Tonelli's integrability criterion makes the subsequent interchange of the Gaussian and spatial integrals legitimate.

    theorem integrable_riesz_gaussian_product (F : š“¢(ā„‚,ā„‚)) {a : ā„}
    (ha : 0 < a) (ha1 : a < 1) :
    Integrable (fun p : ā„‚ Ɨ ā„ => (rieszGaussianWeight a p.1 p.2 : ā„‚)*F p.1)
      (volume.prod (volume.restrict (Ioi 0))) := by
ā€¦

    Mentions: OAI.CubicFirstMoment.rieszGaussianWeight

  6. theorem OAI.CubicFirstMoment.riesz_integral_eq_gaussian_integral line 70

    Source documentation

    Fubini applied to the absolutely integrable Gaussian representation.

    theorem riesz_integral_eq_gaussian_integral (F : š“¢(ā„‚,ā„‚)) {a : ā„}
    (ha : 0 < a) (ha1 : a < 1) :
    (Real.Gamma a:ā„‚)*(āˆ« z : ā„‚, ((ā€–zā€–^(-2*a):ā„):ā„‚)*F z) =
      āˆ« t in Ioi (0:ā„), āˆ« z : ā„‚, (rieszGaussianWeight a z t:ā„‚)*F z := by
ā€¦

    Mentions: OAI.CubicFirstMoment.rieszGaussianWeight