Theorems · Theorem · special functions

integrableOn_rpow_mul_exp_neg_mul_sq

∀ {b : ℝ},
  0 < b →
    ∀ {s : ℝ},
      -1 < s → MeasureTheory.IntegrableOn (fun x => x ^ s * Real.exp (-b * x ^ 2)) (Set.Ioi 0) MeasureTheory.volume

Defined in: Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
Cited by: 1 results in Mathlib
Foundations: Depth 283 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Set.Ioistatement and proof · cited by 1,463
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323
Real.expstatement and proof · cited by 871
MeasureTheory.IntegrableOnstatement and proof · cited by 548
two_posproof · cited by 68
integrableOn_rpow_mul_exp_neg_mul_rpowproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

integrable_rpow_mul_exp_neg_mul_sqproof · cited by 2