Gaussian distributions in Banach spaces: Fernique's theorem #
theorem
ProbabilityTheory.HasGaussianLaw.memLp
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
[CompleteSpace E]
[MeasurableSpace E]
[BorelSpace E]
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : Ω → E}
[hX : HasGaussianLaw X P]
{p : ENNReal}
(hp : p ≠ ⊤)
:
MeasureTheory.MemLp X p P
A Gaussian random variable has moments of all orders.
theorem
ProbabilityTheory.HasGaussianLaw.memLp_two
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
[CompleteSpace E]
[MeasurableSpace E]
[BorelSpace E]
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : Ω → E}
[HasGaussianLaw X P]
:
MeasureTheory.MemLp X 2 P
theorem
ProbabilityTheory.HasGaussianLaw.integrable
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
[CompleteSpace E]
[MeasurableSpace E]
[BorelSpace E]
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : Ω → E}
[HasGaussianLaw X P]
: