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.measure_eq
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : HasLaw X μ P)
{p : 𝓧 → Prop}
(hp : MeasurableSet {x : 𝓧 | p x})
:
theorem
ProbabilityTheory.HasLaw.measureReal_eq
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : HasLaw X μ P)
{p : 𝓧 → Prop}
(hp : MeasurableSet {x : 𝓧 | p x})
:
theorem
ProbabilityTheory.HasLaw.comp_of_hasLaw_comp
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
{Ω' : Type u_3}
{𝓨 : Type u_4}
{m' : MeasurableSpace Ω'}
{m𝓨 : MeasurableSpace 𝓨}
{P' : MeasureTheory.Measure Ω'}
{ν : MeasureTheory.Measure 𝓨}
{f : 𝓧 → 𝓨}
{Y : Ω' → 𝓧}
(hf : AEMeasurable f μ)
(hX : HasLaw X μ P)
(hY : HasLaw Y μ P')
(h : HasLaw (fun (ω : Ω) => f (X ω)) ν P)
:
HasLaw (fun (ω : Ω') => f (Y ω)) ν P'
If there is a random variable X with law μ such that f(X) has law ν, then
for any random variable Y with law μ, f(Y) has law ν.
theorem
ProbabilityTheory.HasLaw.congr
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X Y : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : HasLaw X μ P)
(hY : Y =ᵐ[P] X)
:
HasLaw Y μ P
theorem
ProbabilityTheory.hasLaw_congr
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X Y : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hXY : X =ᵐ[P] Y)
:
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.id
{𝓧 : Type u_2}
{m𝓧 : MeasurableSpace 𝓧}
{μ : MeasureTheory.Measure 𝓧}
:
theorem
ProbabilityTheory.HasLaw.ae_iff
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : HasLaw X μ P)
{p : 𝓧 → Prop}
(hp : Measurable p)
:
theorem
ProbabilityTheory.HasLaw.isFiniteMeasure_iff
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : HasLaw X μ P)
:
theorem
ProbabilityTheory.HasLaw.isProbabilityMeasure_iff
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
(hX : HasLaw X μ P)
:
theorem
ProbabilityTheory.HasLaw.isFiniteMeasure
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ]
(hX : HasLaw X μ P)
:
theorem
ProbabilityTheory.HasLaw.isProbabilityMeasure
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
(hX : HasLaw X μ P)
:
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
MeasureTheory.MeasurePreserving.comp_hasLaw
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : Measure 𝓧}
{P : Measure Ω}
{𝓨 : Type u_3}
{m𝓨 : MeasurableSpace 𝓨}
{ν : Measure 𝓨}
{Y : 𝓧 → 𝓨}
(hY : MeasurePreserving Y μ ν)
(hX : ProbabilityTheory.HasLaw X μ P)
:
ProbabilityTheory.HasLaw (Y ∘ X) ν P
theorem
MeasureTheory.MeasurePreserving.fun_comp_hasLaw
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : Measure 𝓧}
{P : Measure Ω}
{𝓨 : Type u_3}
{m𝓨 : MeasurableSpace 𝓨}
{ν : Measure 𝓨}
{Y : 𝓧 → 𝓨}
(hY : MeasurePreserving Y μ ν)
(hX : ProbabilityTheory.HasLaw X μ P)
:
ProbabilityTheory.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
theorem
ProbabilityTheory.indepFun_iff_hasLaw_prodMk_prod
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{𝓨 : Type u_3}
{m𝓨 : MeasurableSpace 𝓨}
{ν : MeasureTheory.Measure 𝓨}
{Y : Ω → 𝓨}
(hX : HasLaw X μ P)
(hY : HasLaw Y ν P)
:
theorem
ProbabilityTheory.IndepFun.hasLaw_prod
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
{μ : MeasureTheory.Measure 𝓧}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure P]
{𝓨 : Type u_3}
{m𝓨 : MeasurableSpace 𝓨}
{ν : MeasureTheory.Measure 𝓨}
{Y : Ω → 𝓨}
(hX : HasLaw X μ P)
(hY : HasLaw Y ν P)
:
Alias of the forward direction of ProbabilityTheory.indepFun_iff_hasLaw_prodMk_prod.
theorem
ProbabilityTheory.iIndepFun.hasLaw_pi
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_3}
[Fintype ι]
{𝓧 : ι → Type u_4}
{m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)}
{μ : (i : ι) → MeasureTheory.Measure (𝓧 i)}
{X : (i : ι) → Ω → 𝓧 i}
(hX : ∀ (i : ι), HasLaw (X i) (μ i) P)
(h : iIndepFun X P)
:
HasLaw (fun (ω : Ω) (i : ι) => X i ω) (MeasureTheory.Measure.pi μ) P
theorem
ProbabilityTheory.iIndepFun_iff_hasLaw_pi_pi
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure P]
{ι : Type u_3}
[Fintype ι]
{𝓧 : ι → Type u_4}
{m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)}
{μ : (i : ι) → MeasureTheory.Measure (𝓧 i)}
{X : (i : ι) → Ω → 𝓧 i}
(hX : ∀ (i : ι), HasLaw (X i) (μ i) P)
: