Law of a random variable #
We introduce a predicate HasLaw X μ P stating that the random variable X has law μ under
the measure P. This is expressed as P.map X = μ. We also require X to be P-almost-everywhere
measurable. Indeed, if X is not almost-everywhere measurable then P.map X is defined to be 0,
so that HasLaw X 0 P would be true. The measurability hypothesis ensures nice interactions with
operations on the codomain of X.
See for instance HasLaw.comp, IndepFun.hasLaw_mul and IndepFun.hasLaw_add.
structure
ProbabilityTheory.HasLaw
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{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}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{Y : Ω → 𝓧}
(hX : HasLaw X μ P)
(hY : Y =ᵐ[P] X)
:
HasLaw Y μ P
theorem
MeasureTheory.MeasurePreserving.hasLaw
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : Measure 𝓧}
{P : Measure Ω}
(h : MeasurePreserving X P μ)
:
ProbabilityTheory.HasLaw X μ P
theorem
ProbabilityTheory.HasLaw.measurePreserving
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(h₁ : HasLaw X μ P)
(h₂ : Measurable X)
:
theorem
ProbabilityTheory.HasLaw.comp
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{𝒴 : Type u_3}
{m𝒴 : MeasurableSpace 𝒴}
{ν : MeasureTheory.Measure 𝒴}
{Y : 𝓧 → 𝒴}
(hY : HasLaw Y ν μ)
(hX : HasLaw X μ P)
:
theorem
ProbabilityTheory.HasLaw.fun_comp
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{𝒴 : Type u_3}
{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 Ω}
{M : Type u_3}
[Monoid M]
{mM : MeasurableSpace M}
[MeasurableMul₂ M]
{μ ν : MeasureTheory.Measure M}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{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 Ω}
{M : Type u_3}
[AddMonoid M]
{mM : MeasurableSpace M}
[MeasurableAdd₂ M]
{μ ν : MeasureTheory.Measure M}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{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 Ω}
{M : Type u_3}
[Monoid M]
{mM : MeasurableSpace M}
[MeasurableMul₂ M]
{μ ν : MeasureTheory.Measure M}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{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 Ω}
{M : Type u_3}
[AddMonoid M]
{mM : MeasurableSpace M}
[MeasurableAdd₂ M]
{μ ν : MeasureTheory.Measure M}
[MeasureTheory.SigmaFinite μ]
[MeasureTheory.SigmaFinite ν]
{X Y : Ω → M}
(hX : HasLaw X μ P)
(hY : HasLaw Y ν P)
(hXY : IndepFun X Y P)
:
theorem
ProbabilityTheory.HasLaw.integral_comp
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{X : Ω → 𝓧}
(hX : HasLaw X μ P)
{f : 𝓧 → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
theorem
ProbabilityTheory.HasLaw.lintegral_comp
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{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_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[SecondCountableTopology E]
{mE : MeasurableSpace E}
[OpensMeasurableSpace E]
{μ : MeasureTheory.Measure E}
{X : Ω → E}
(hX : HasLaw X μ P)
:
theorem
ProbabilityTheory.HasLaw.covariance_comp
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : HasLaw X μ P)
{f g : 𝓧 → ℝ}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
theorem
ProbabilityTheory.HasLaw.covariance_fun_comp
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : HasLaw X μ P)
{f g : 𝓧 → ℝ}
(hf : AEMeasurable f μ)
(hg : AEMeasurable g μ)
:
theorem
ProbabilityTheory.HasLaw.variance_eq
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{μ : MeasureTheory.Measure ℝ}
{X : Ω → ℝ}
(hX : HasLaw X μ P)
:
theorem
ProbabilityTheory.HasPDF.hasLaw
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
[h : MeasureTheory.HasPDF X P μ]
:
HasLaw X (μ.withDensity (MeasureTheory.pdf X P μ)) P