Gaussian distributions in Banach spaces: Fernique's theorem #
instance
ProbabilityTheory.instIsGaussianMapHAdd_brownianMotion
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
{μ : MeasureTheory.Measure E}
(c : E)
:
IsGaussian (MeasureTheory.Measure.map (fun (x : E) => x + c) μ)
instance
ProbabilityTheory.instIsGaussianMapHAdd_brownianMotion_1
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
{μ : MeasureTheory.Measure E}
(c : E)
:
IsGaussian (MeasureTheory.Measure.map (fun (x : E) => c + x) μ)
instance
ProbabilityTheory.instIsGaussianMapHSub_brownianMotion
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
{μ : MeasureTheory.Measure E}
(c : E)
:
IsGaussian (MeasureTheory.Measure.map (fun (x : E) => x - c) μ)
theorem
ProbabilityTheory.IsGaussian.exists_integrable_exp_sq
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
(μ : MeasureTheory.Measure E)
[IsGaussian μ]
:
Fernique's theorem: for a Gaussian measure, there exists C > 0
such that the function
x ↦ exp (C * ‖x‖ ^ 2)
is integrable.
theorem
ProbabilityTheory.IsGaussian.memLp_id
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
(μ : MeasureTheory.Measure E)
[IsGaussian μ]
(p : ENNReal)
(hp : p ≠ ⊤)
:
A Gaussian measure has moments of all orders.
That is, the identity is in Lp for all finite p
.
theorem
ProbabilityTheory.IsGaussian.integral_dual
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{μ : MeasureTheory.Measure E}
[IsGaussian μ]
[SecondCountableTopology E]
[CompleteSpace E]
(L : NormedSpace.Dual ℝ E)
: