Gaussian random variables #
In this file we prove basic properties of Gaussian random variables.
Implementation note #
Many lemmas are duplicated with an expanded form of some function. For instance there is
HasGaussianLaw.add and HasGaussianLaw.fun_add. The reason is that if someone wants for instance
to rewrite using HasGaussianLaw.charFunDual_map_eq and provide the proof of HasGaussianLaw
directly through dot notation, the lemma used must syntactically correspond to the random variable.
Tags #
Gaussian random variable
theorem
ProbabilityTheory.HasGaussianLaw.congr
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
{X Y : Ω → E}
(hX : HasGaussianLaw X P)
(h : X =ᵐ[P] Y)
:
HasGaussianLaw Y P
theorem
ProbabilityTheory.IsGaussian.hasGaussianLaw
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
{X : Ω → E}
[IsGaussian (MeasureTheory.Measure.map X P)]
:
HasGaussianLaw X P
theorem
ProbabilityTheory.IsGaussian.hasGaussianLaw_id
{E : Type u_2}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
{mE : MeasurableSpace E}
{μ : MeasureTheory.Measure E}
[IsGaussian μ]
:
theorem
ProbabilityTheory.HasGaussianLaw.aemeasurable
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
{X : Ω → E}
(hX : HasGaussianLaw X P)
:
AEMeasurable X P
theorem
ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
{X : Ω → E}
(hX : HasGaussianLaw X P)
:
theorem
ProbabilityTheory.HasLaw.hasGaussianLaw
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
{mE : MeasurableSpace E}
{X : Ω → E}
{μ : MeasureTheory.Measure E}
(hX : HasLaw X μ P)
[IsGaussian μ]
:
HasGaussianLaw X P
theorem
ProbabilityTheory.HasGaussianLaw.map_of_measurable
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
{X : Ω → E}
{F : Type u_5}
[TopologicalSpace F]
[AddCommMonoid F]
[Module ℝ F]
[MeasurableSpace F]
[OpensMeasurableSpace F]
(L : E →L[ℝ] F)
(hX : HasGaussianLaw X P)
(hL : Measurable ⇑L)
:
HasGaussianLaw (⇑L ∘ X) P
theorem
ProbabilityTheory.HasGaussianLaw.charFun_map_eq
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[InnerProductSpace ℝ E]
(t : E)
(hX : HasGaussianLaw X P)
:
theorem
ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[CompleteSpace E]
[InnerProductSpace ℝ E]
[MeasureTheory.IsFiniteMeasure P]
(hX : AEMeasurable X P)
:
HasGaussianLaw X P ↔ ∀ (t : E),
MeasureTheory.charFun (MeasureTheory.Measure.map X P) t = Complex.exp
(↑(∫ (x : Ω), (fun (ω : Ω) => inner ℝ t (X ω)) x ∂P) * Complex.I - ↑(variance (fun (ω : Ω) => inner ℝ t (X ω)) P) / 2)
theorem
ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
(L : StrongDual ℝ E)
(hX : HasGaussianLaw X P)
:
MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) L = Complex.exp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * Complex.I - ↑(variance (⇑L ∘ X) P) / 2)
theorem
ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[MeasureTheory.IsFiniteMeasure P]
(hX : AEMeasurable X P)
:
HasGaussianLaw X P ↔ ∀ (L : StrongDual ℝ E),
MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) L = Complex.exp (↑(∫ (x : Ω), (⇑L ∘ X) x ∂P) * Complex.I - ↑(variance (⇑L ∘ X) P) / 2)
theorem
ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
(L : StrongDual ℝ E)
(hX : HasGaussianLaw X P)
:
MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) L = Complex.exp (↑(∫ (ω : Ω), L (X ω) ∂P) * Complex.I - ↑(variance (fun (ω : Ω) => L (X ω)) P) / 2)
theorem
ProbabilityTheory.HasGaussianLaw.memLp
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[SecondCountableTopology 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
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[SecondCountableTopology E]
(hX : HasGaussianLaw X P)
:
MeasureTheory.MemLp X 2 P
theorem
ProbabilityTheory.HasGaussianLaw.integrable
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[CompleteSpace E]
[SecondCountableTopology E]
(hX : HasGaussianLaw X P)
:
theorem
ProbabilityTheory.HasGaussianLaw.map
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
(hX : HasGaussianLaw X P)
(L : E →L[ℝ] F)
:
HasGaussianLaw (⇑L ∘ X) P
theorem
ProbabilityTheory.HasGaussianLaw.map_fun
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
(hX : HasGaussianLaw X P)
(L : E →L[ℝ] F)
:
HasGaussianLaw (fun (ω : Ω) => L (X ω)) P
theorem
ProbabilityTheory.HasGaussianLaw.map_equiv
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
(hX : HasGaussianLaw X P)
(L : E ≃L[ℝ] F)
:
HasGaussianLaw (⇑L ∘ X) P
theorem
ProbabilityTheory.HasGaussianLaw.map_equiv_fun
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
(hX : HasGaussianLaw X P)
(L : E ≃L[ℝ] F)
:
HasGaussianLaw (fun (ω : Ω) => L (X ω)) P
theorem
ProbabilityTheory.HasGaussianLaw.smul
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
(c : ℝ)
(hX : HasGaussianLaw X P)
:
HasGaussianLaw (c • X) P
theorem
ProbabilityTheory.HasGaussianLaw.fun_smul
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
(c : ℝ)
(hX : HasGaussianLaw X P)
:
HasGaussianLaw (fun (ω : Ω) => c • X ω) P
theorem
ProbabilityTheory.HasGaussianLaw.neg
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
(hX : HasGaussianLaw X P)
:
HasGaussianLaw (-X) P
theorem
ProbabilityTheory.HasGaussianLaw.fun_neg
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
(hX : HasGaussianLaw X P)
:
HasGaussianLaw (fun (ω : Ω) => -X ω) P
theorem
ProbabilityTheory.HasGaussianLaw.toLp_prodMk
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
{Y : Ω → F}
[SecondCountableTopologyEither E F]
(p : ENNReal)
[Fact (1 ≤ p)]
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
:
HasGaussianLaw (fun (ω : Ω) => WithLp.toLp p (X ω, Y ω)) P
theorem
ProbabilityTheory.HasGaussianLaw.fst
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
{Y : Ω → F}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
:
HasGaussianLaw X P
theorem
ProbabilityTheory.HasGaussianLaw.snd
{Ω : Type u_1}
{E : Type u_2}
{F : Type u_3}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
{Y : Ω → F}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
:
HasGaussianLaw Y P
theorem
ProbabilityTheory.HasGaussianLaw.add
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[SecondCountableTopology E]
{Y : Ω → E}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
:
HasGaussianLaw (X + Y) P
theorem
ProbabilityTheory.HasGaussianLaw.fun_add
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[SecondCountableTopology E]
{Y : Ω → E}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
:
HasGaussianLaw (fun (ω : Ω) => X ω + Y ω) P
theorem
ProbabilityTheory.HasGaussianLaw.sub
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[SecondCountableTopology E]
{Y : Ω → E}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
:
HasGaussianLaw (X - Y) P
theorem
ProbabilityTheory.HasGaussianLaw.fun_sub
{Ω : Type u_1}
{E : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
{X : Ω → E}
[NormedSpace ℝ E]
[SecondCountableTopology E]
{Y : Ω → E}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
:
HasGaussianLaw (fun (ω : Ω) => X ω - Y ω) P
theorem
ProbabilityTheory.HasGaussianLaw.eval
{Ω : Type u_1}
{ι : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
{X : (i : ι) → Ω → E i}
(hX : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P)
(i : ι)
:
HasGaussianLaw (X i) P
theorem
ProbabilityTheory.HasGaussianLaw.prodMk
{Ω : Type u_1}
{ι : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
{X : (i : ι) → Ω → E i}
[∀ (i : ι), SecondCountableTopology (E i)]
[Finite ι]
(hX : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P)
(i j : ι)
:
HasGaussianLaw (fun (ω : Ω) => (X i ω, X j ω)) P
theorem
ProbabilityTheory.HasGaussianLaw.toLp_pi
{Ω : Type u_1}
{ι : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
{X : (i : ι) → Ω → E i}
[∀ (i : ι), SecondCountableTopology (E i)]
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
(hX : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P)
:
HasGaussianLaw (fun (ω : Ω) => WithLp.toLp p fun (x : ι) => X x ω) P
theorem
ProbabilityTheory.HasGaussianLaw.sum
{Ω : Type u_1}
{ι : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[Fintype ι]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{X : ι → Ω → E}
(hX : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P)
:
HasGaussianLaw (∑ i : ι, X i) P
theorem
ProbabilityTheory.HasGaussianLaw.fun_sum
{Ω : Type u_1}
{ι : Type u_4}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[Fintype ι]
{E : Type u_6}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{X : ι → Ω → E}
(hX : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P)
:
HasGaussianLaw (fun (ω : Ω) => ∑ i : ι, X i ω) P