Documentation

BrownianMotion.Gaussian.Fernique

Gaussian distributions in Banach spaces: Fernique's theorem #

source
theorem ProbabilityTheory.IsGaussian.memLp_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [IsGaussian μ] (p : ENNReal) (hp : p ≠ ⊤) :
MeasureTheory.MemLp id p μ

A Gaussian measure has moments of all orders. That is, the identity is in Lp for all finite p.

source
theorem ProbabilityTheory.IsGaussian.memLp_two_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] :
MeasureTheory.MemLp id 2 μ
source
theorem ProbabilityTheory.IsGaussian.integrable_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] :
MeasureTheory.Integrable id μ
source
theorem ProbabilityTheory.IsGaussian.integrable_fun_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] :
MeasureTheory.Integrable (fun (x : E) => x) μ
source
theorem ProbabilityTheory.IsGaussian.integral_dual {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [SecondCountableTopology E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [IsGaussian μ] (L : NormedSpace.Dual ℝ E) :
∫ (x : E), L x ∂μ = L (∫ (x : E), x ∂μ)
source
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.

source
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
source
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] :
MeasureTheory.Integrable X P