theorem
ProbabilityTheory.hasLaw_map
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : AEMeasurable X P)
:
HasLaw X (MeasureTheory.Measure.map X P) P
theorem
ProbabilityTheory.HasLaw.ae_eq_of_dirac'
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSingletonClass 𝓧]
{x : 𝓧}
{X : Ω → 𝓧}
(hX : HasLaw X (MeasureTheory.Measure.dirac x) P)
:
theorem
ProbabilityTheory.HasLaw.ae_eq_of_dirac
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
[MeasurableSingletonClass 𝓧]
{x : 𝓧}
{X : Ω → 𝓧}
(hX : HasLaw X (MeasureTheory.Measure.dirac x) P)
:
theorem
ProbabilityTheory.HasLaw.ae_eq_const_of_gaussianReal
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : Ω → ℝ}
{μ : ℝ}
(hX : HasLaw X (gaussianReal μ 0) P)
:
theorem
ProbabilityTheory.IndepFun.charFunDual_map_add_eq_mul
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[MeasureTheory.IsProbabilityMeasure P]
{X Y : Ω → E}
[NormedSpace ℝ E]
(mX : AEMeasurable X P)
(mY : AEMeasurable Y P)
(hXY : IndepFun X Y P)
:
theorem
ProbabilityTheory.IndepFun.charFun_map_add_eq_mul
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[MeasureTheory.IsProbabilityMeasure P]
{X Y : Ω → E}
[InnerProductSpace ℝ E]
(mX : AEMeasurable X P)
(mY : AEMeasurable Y P)
(hXY : IndepFun X Y P)
:
class
ProbabilityTheory.HasGaussianLaw
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
(X : Ω → E)
(P : MeasureTheory.Measure Ω)
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
:
The predicate HasGaussianLaw X P means that under the measure P,
X has a Gaussian distribution
- isGaussian_map : IsGaussian (MeasureTheory.Measure.map X P)
Instances
theorem
ProbabilityTheory.HasGaussianLaw.congr
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
{Y : Ω → E}
[HasGaussianLaw X P]
(h : ∀ᵐ (ω : Ω) ∂P, X ω = Y ω)
:
HasGaussianLaw Y P
instance
ProbabilityTheory.IsGaussian.hasGaussianLaw
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
[IsGaussian (MeasureTheory.Measure.map X P)]
:
HasGaussianLaw X P
instance
ProbabilityTheory.IsGaussian.hasGaussianLaw_fun
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
[IsGaussian (MeasureTheory.Measure.map X P)]
:
HasGaussianLaw (fun (ω : Ω) => X ω) P
instance
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}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
[hX : HasGaussianLaw X P]
:
AEMeasurable X P
theorem
ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
[mE : MeasurableSpace E]
[HasGaussianLaw X P]
:
theorem
ProbabilityTheory.HasLaw.hasGaussianLaw
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[TopologicalSpace E]
[AddCommMonoid E]
[Module ℝ E]
{mE : MeasurableSpace E}
{μ : MeasureTheory.Measure E}
(hX : HasLaw X μ P)
[IsGaussian μ]
:
HasGaussianLaw X P
instance
ProbabilityTheory.HasGaussianLaw.map
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
(L : E →L[ℝ] F)
[HasGaussianLaw X P]
:
HasGaussianLaw (⇑L ∘ X) P
instance
ProbabilityTheory.HasGaussianLaw.map_fun
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
(L : E →L[ℝ] F)
[hX : HasGaussianLaw X P]
:
HasGaussianLaw (fun (ω : Ω) => L (X ω)) P
instance
ProbabilityTheory.HasGaussianLaw.map_equiv
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
(L : E ≃L[ℝ] F)
[HasGaussianLaw X P]
:
HasGaussianLaw (⇑L ∘ X) P
instance
ProbabilityTheory.HasGaussianLaw.map_equiv_fun
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
(L : E ≃L[ℝ] F)
[hX : HasGaussianLaw X P]
:
HasGaussianLaw (fun (ω : Ω) => L (X ω)) P
instance
ProbabilityTheory.HasGaussianLaw.toLp_comp_prodMk
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
[SecondCountableTopologyEither E F]
{Y : Ω → F}
(p : ENNReal)
[Fact (1 ≤ p)]
[HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P]
:
HasGaussianLaw (fun (ω : Ω) => WithLp.toLp p (X ω, Y ω)) P
theorem
ProbabilityTheory.HasGaussianLaw.fst
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
[SecondCountableTopologyEither E F]
{Y : Ω → F}
[HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P]
:
HasGaussianLaw X P
theorem
ProbabilityTheory.HasGaussianLaw.snd
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{X : Ω → E}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[BorelSpace F]
[SecondCountableTopologyEither E F]
{Y : Ω → F}
[HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P]
:
HasGaussianLaw Y P
instance
ProbabilityTheory.HasGaussianLaw.sub
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{E : Type u_2}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{ι : Type u_4}
[Fintype ι]
{X : ι → Ω → E}
[h : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P]
(i j : ι)
:
HasGaussianLaw (X i - X j) P
instance
ProbabilityTheory.IsGaussian.hasGaussianLaw_sub_eval
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{ι : Type u_4}
[Fintype ι]
{μ : MeasureTheory.Measure (ι → E)}
[IsGaussian μ]
(i j : ι)
:
HasGaussianLaw (fun (x : ι → E) => x i - x j) μ
instance
ProbabilityTheory.IsGaussian.hasGaussianLaw_sub_eval_piLp
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{ι : Type u_4}
[Fintype ι]
(p : ENNReal)
[Fact (1 ≤ p)]
{μ : MeasureTheory.Measure (PiLp p fun (x : ι) => E)}
[IsGaussian μ]
(i j : ι)
:
HasGaussianLaw (fun (x : PiLp p fun (x : ι) => E) => x i - x j) μ
instance
ProbabilityTheory.HasGaussianLaw.eval
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_4}
[Fintype ι]
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
{X : (i : ι) → Ω → E i}
[h : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P]
(i : ι)
:
HasGaussianLaw (X i) P
instance
ProbabilityTheory.HasGaussianLaw.toLp_comp_pi
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_4}
[Fintype ι]
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
{X : (i : ι) → Ω → E i}
(p : ENNReal)
[Fact (1 ≤ p)]
[HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P]
:
HasGaussianLaw (fun (ω : Ω) => WithLp.toLp p fun (x : ι) => X x ω) P
instance
ProbabilityTheory.IsGaussian.hasGaussianLaw_eval
{ι : Type u_4}
[Fintype ι]
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
{μ : MeasureTheory.Measure ((i : ι) → E i)}
[IsGaussian μ]
(i : ι)
:
HasGaussianLaw (fun (x : (i : ι) → E i) => x i) μ
instance
ProbabilityTheory.IsGaussian.hasGaussianLaw_eval_piLp
{ι : Type u_4}
[Fintype ι]
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
(p : ENNReal)
[Fact (1 ≤ p)]
{μ : MeasureTheory.Measure (PiLp p E)}
[IsGaussian μ]
(i : ι)
:
HasGaussianLaw (fun (x : PiLp p E) => x i) μ