structure
ProbabilityTheory.HasLaw
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
(X : Ω → 𝓧)
(μ : MeasureTheory.Measure 𝓧)
(P : MeasureTheory.Measure Ω := by volume_tac)
:
The predicate HasLaw X μ P registers the fact that the random variable X has law μ under
the measure P, in other words that P.map X = μ. We also require X to be AEMeasurable,
to allow for nice interactions with operations on the codomain of X. See for instance
HasLaw.comp, IndepFun.hasLaw_mul and IndepFun.hasLaw_add.
- aemeasurable : AEMeasurable X P
Instances For
theorem
ProbabilityTheory.HasLaw.congr
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{Y : Ω → 𝓧}
(hX : HasLaw X μ P)
(hY : Y =ᵐ[P] X)
:
HasLaw Y μ P
theorem
ProbabilityTheory.MeasurePreserving.hasLaw
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(h : MeasureTheory.MeasurePreserving X P μ)
:
HasLaw X μ P
theorem
ProbabilityTheory.HasLaw.measurePreserving
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(h₁ : HasLaw X μ P)
(h₂ : Measurable X)
:
theorem
ProbabilityTheory.HasLaw.comp
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_3}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{𝒴 : Type u_2}
{m𝒴 : MeasurableSpace 𝒴}
{ν : MeasureTheory.Measure 𝒴}
{Y : 𝓧 → 𝒴}
(hY : HasLaw Y ν μ)
(hX : HasLaw X μ P)
:
theorem
ProbabilityTheory.HasLaw.fun_comp
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_3}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{𝒴 : Type u_2}
{m𝒴 : MeasurableSpace 𝒴}
{ν : MeasureTheory.Measure 𝒴}
{Y : 𝓧 → 𝒴}
(hY : HasLaw Y ν μ)
(hX : HasLaw X μ P)
:
HasLaw (fun (ω : Ω) => Y (X ω)) ν P
theorem
ProbabilityTheory.IndepFun.hasLaw_mul
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{M : Type u_2}
[Monoid M]
{mM : MeasurableSpace M}
[MeasurableMul₂ M]
{μ ν : MeasureTheory.Measure M}
{X Y : Ω → M}
(hX : HasLaw X μ P)
(hY : HasLaw Y ν P)
(hXY : IndepFun X Y P)
:
theorem
ProbabilityTheory.IndepFun.hasLaw_add
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{M : Type u_2}
[AddMonoid M]
{mM : MeasurableSpace M}
[MeasurableAdd₂ M]
{μ ν : MeasureTheory.Measure M}
{X Y : Ω → M}
(hX : HasLaw X μ P)
(hY : HasLaw Y ν P)
(hXY : IndepFun X Y P)
:
theorem
ProbabilityTheory.IndepFun.hasLaw_fun_mul
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{M : Type u_2}
[Monoid M]
{mM : MeasurableSpace M}
[MeasurableMul₂ M]
{μ ν : MeasureTheory.Measure M}
{X Y : Ω → M}
(hX : HasLaw X μ P)
(hY : HasLaw Y ν P)
(hXY : IndepFun X Y P)
:
theorem
ProbabilityTheory.IndepFun.hasLaw_fun_add
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{M : Type u_2}
[AddMonoid M]
{mM : MeasurableSpace M}
[MeasurableAdd₂ M]
{μ ν : MeasureTheory.Measure M}
{X Y : Ω → M}
(hX : HasLaw X μ P)
(hY : HasLaw Y ν P)
(hXY : IndepFun X Y P)
:
theorem
ProbabilityTheory.HasLaw.integral_comp
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_3}
{m𝓧 : MeasurableSpace 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{X : Ω → 𝓧}
(hX : HasLaw X μ P)
{f : 𝓧 → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
theorem
ProbabilityTheory.HasLaw.lintegral_comp
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
(hX : HasLaw X μ P)
{f : 𝓧 → ENNReal}
(hf : AEMeasurable f μ)
:
theorem
ProbabilityTheory.HasLaw.integral_eq
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
{mE : MeasurableSpace E}
[OpensMeasurableSpace E]
{μ : MeasureTheory.Measure E}
{X : Ω → E}
(hX : HasLaw X μ P)
:
theorem
ProbabilityTheory.HasLaw.variance_eq
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{μ : MeasureTheory.Measure ℝ}
{X : Ω → ℝ}
(hX : HasLaw X μ 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
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.eval
{ι : Type u_4}
{Ω : Type u_5}
{E : ι → Type u_6}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[(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
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
(p : ENNReal)
[Fact (1 ≤ p)]
{ι : 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}
[HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P]
:
HasGaussianLaw (fun (ω : Ω) => WithLp.toLp p fun (x : ι) => X x ω) P
instance
ProbabilityTheory.IsGaussian.map_eval
{ι : Type u_4}
[Fintype ι]
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
{mE : (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.map_eval_piLp
(p : ENNReal)
[Fact (1 ≤ p)]
{ι : Type u_4}
[Fintype ι]
{E : ι → Type u_5}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
{mE : (i : ι) → MeasurableSpace (E i)}
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
{μ : MeasureTheory.Measure (PiLp p E)}
[IsGaussian μ]
(i : ι)
:
HasGaussianLaw (fun (x : PiLp p E) => x i) μ
instance
ProbabilityTheory.HasGaussianLaw.sub
{ι : Type u_4}
{Ω : Type u_5}
{E : Type u_6}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{X : ι → Ω → E}
[h : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P]
(i j : ι)
:
HasGaussianLaw (X i - X j) P
instance
ProbabilityTheory.IsGaussian.map_eval_sub_eval
{ι : Type u_4}
{E : Type u_5}
[Fintype ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{μ : MeasureTheory.Measure (ι → E)}
[IsGaussian μ]
(i j : ι)
:
HasGaussianLaw (fun (x : ι → E) => x i - x j) μ
instance
ProbabilityTheory.IsGaussian.map_eval_sub_eval_piLp
(p : ENNReal)
[Fact (1 ≤ p)]
{ι : Type u_4}
{E : Type u_5}
[Fintype ι]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{μ : MeasureTheory.Measure (PiLp p fun (x : ι) => E)}
[IsGaussian μ]
(i j : ι)
:
HasGaussianLaw (fun (x : PiLp p fun (x : ι) => E) => x i - x j) μ