Lemmas about HasLaw #
theorem
AEMeasurable.hasLaw_map
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{P : MeasureTheory.Measure Ω}
{X : Ω → 𝓧}
(hX : AEMeasurable X P)
:
theorem
Measurable.hasLaw_map
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{X : Ω → 𝓧}
(hX : Measurable X)
(P : MeasureTheory.Measure Ω)
:
theorem
ProbabilityTheory.identDistrib_of_forall_identDistrib_cond
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{P : MeasureTheory.Measure Ω}
{ι : Type u_3}
[Countable ι]
{mι : MeasurableSpace ι}
[MeasurableSingletonClass ι]
[MeasureTheory.IsFiniteMeasure P]
{g : Ω → ι}
(hg : Measurable g)
{X Y : Ω → 𝓧}
(hX : Measurable X)
(hY : Measurable Y)
(h : ∀ (i : ι), IdentDistrib X Y P[|g ⁻¹' {i}] P[|g ⁻¹' {i}])
:
IdentDistrib X Y P P
Two random variables which are identically distributed conditionally on each atom of a countable measurable partition are identically distributed.
theorem
ProbabilityTheory.hasLaw_of_forall_hasLaw_cond
{Ω : Type u_1}
{𝓧 : Type u_2}
{mΩ : MeasurableSpace Ω}
{m𝓧 : MeasurableSpace 𝓧}
{P : MeasureTheory.Measure Ω}
{ι : Type u_3}
[Countable ι]
{mι : MeasurableSpace ι}
[MeasurableSingletonClass ι]
[MeasureTheory.IsProbabilityMeasure P]
{g : Ω → ι}
(hg : Measurable g)
{X : Ω → 𝓧}
(hX : Measurable X)
{μ : MeasureTheory.Measure 𝓧}
(h : ∀ (i : ι), P (g ⁻¹' {i}) ≠ 0 → HasLaw X μ P[|g ⁻¹' {i}])
:
HasLaw X μ P
If a random variable has law μ conditionally on each atom of positive probability of a
countable measurable partition, then it has law μ.
theorem
ProbabilityTheory.hasLaw_of_forall_eventually_eq
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_3}
{𝓧 : ι → Type u_4}
[(i : ι) → MeasurableSpace (𝓧 i)]
[MeasureTheory.IsFiniteMeasure P]
{κ : Type u_5}
{L : Filter κ}
[L.NeBot]
[L.IsCountablyGenerated]
{μ : MeasureTheory.Measure ((i : ι) → 𝓧 i)}
{Y : κ → Ω → (i : ι) → 𝓧 i}
{Y' : Ω → (i : ι) → 𝓧 i}
(hY : ∀ (n : κ), Measurable (Y n))
(hY' : AEMeasurable Y' P)
(h_law : ∀ (n : κ), HasLaw (Y n) μ P)
(h_lim : ∀ (ω : Ω) (i : ι), ∀ᶠ (n : κ) in L, Y n ω i = Y' ω i)
:
HasLaw Y' μ P
Let Y n : Ω → Π i, 𝓧 i be random variables with law μ, indexed by a countably generated
filter L. If for every ω and i, Y n ω i is eventually equal to Y' ω i along L, then Y'
also has law μ.