Identically distributed random variables #
Two random variables defined on two (possibly different) probability spaces but taking value in the same space are identically distributed if their distributions (i.e., the image probability measures on the target space) coincide. We define this concept and establish its basic properties in this file.
Main definitions and results #
IdentDistrib f g μ νregisters that the image ofμunderfcoincides with the image ofνunderg(and thatfandgare almost everywhere measurable, as otherwise the image measures don't make sense). The measures can be kept implicit as inIdentDistrib f gif the spaces are registered as measure spaces.IdentDistrib.comp: being identically distributed is stable under composition with measurable maps.
There are two main kinds of lemmas, under the assumption that f and g are identically
distributed: lemmas saying that two quantities computed for f and g are the same, and lemmas
saying that if f has some property then g also has it. The first kind is registered as
IdentDistrib.foo_fst, the second one as IdentDistrib.foo_snd (in the latter case, to deduce
a property of f from one of g, use h.symm.foo_snd where h : IdentDistrib f g μ ν). For
instance:
IdentDistrib.measure_mem_eq: iffandgare identically distributed, then the probabilities that they belong to a given measurable set are the same.IdentDistrib.integral_eq: iffandgare identically distributed, then their integrals are the same.IdentDistrib.variance_eq: iffandgare identically distributed, then their variances are the same.IdentDistrib.aestronglyMeasurable_snd: iffandgare identically distributed andfis almost everywhere strongly measurable, then so isg.IdentDistrib.memℒp_snd: iffandgare identically distributed andfbelongs toℒp, then so doesg.
We also register several dot notation shortcuts for convenience.
For instance, if h : IdentDistrib f g μ ν, then h.sq states that f^2 and g^2 are
identically distributed, and h.norm states that ‖f‖ and ‖g‖ are identically distributed, and
so on.
structure
ProbabilityTheory.IdentDistrib
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
(f : α → γ)
(g : β → γ)
(μ : MeasureTheory.Measure α := by volume_tac)
(ν : MeasureTheory.Measure β := by volume_tac)
:
Two functions defined on two (possibly different) measure spaces are identically distributed if their image measures coincide. This only makes sense when the functions are ae measurable (as otherwise the image measures are not defined), so we require this as well in the definition.
- aemeasurable_fst : AEMeasurable f μ
- aemeasurable_snd : AEMeasurable g ν
- map_eq : MeasureTheory.Measure.map f μ = MeasureTheory.Measure.map g ν
Instances For
theorem
ProbabilityTheory.IdentDistrib.refl
{α : Type u_1}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{f : α → γ}
(hf : AEMeasurable f μ)
:
ProbabilityTheory.IdentDistrib f f μ μ
theorem
ProbabilityTheory.IdentDistrib.symm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
ProbabilityTheory.IdentDistrib g f ν μ
theorem
ProbabilityTheory.IdentDistrib.trans
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
{ρ : MeasureTheory.Measure δ}
{h : δ → γ}
(h₁ : ProbabilityTheory.IdentDistrib f g μ ν)
(h₂ : ProbabilityTheory.IdentDistrib g h ν ρ)
:
ProbabilityTheory.IdentDistrib f h μ ρ
theorem
ProbabilityTheory.IdentDistrib.comp_of_aemeasurable
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
{u : γ → δ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(hu : AEMeasurable u (MeasureTheory.Measure.map f μ))
:
ProbabilityTheory.IdentDistrib (u ∘ f) (u ∘ g) μ ν
theorem
ProbabilityTheory.IdentDistrib.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
{u : γ → δ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(hu : Measurable u)
:
ProbabilityTheory.IdentDistrib (u ∘ f) (u ∘ g) μ ν
theorem
ProbabilityTheory.IdentDistrib.of_ae_eq
{α : Type u_1}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{f g : α → γ}
(hf : AEMeasurable f μ)
(heq : f =ᵐ[μ] g)
:
ProbabilityTheory.IdentDistrib f g μ μ
theorem
MeasureTheory.AEMeasurable.identDistrib_mk
{α : Type u_1}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{f : α → γ}
(hf : AEMeasurable f μ)
:
ProbabilityTheory.IdentDistrib f (AEMeasurable.mk f hf) μ μ
theorem
MeasureTheory.AEStronglyMeasurable.identDistrib_mk
{α : Type u_1}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{f : α → γ}
[TopologicalSpace γ]
[TopologicalSpace.PseudoMetrizableSpace γ]
[BorelSpace γ]
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
theorem
ProbabilityTheory.IdentDistrib.measure_mem_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
{s : Set γ}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.IdentDistrib.measure_preimage_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
{s : Set γ}
(hs : MeasurableSet s)
:
theorem
ProbabilityTheory.IdentDistrib.ae_snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
{p : γ → Prop}
(pmeas : MeasurableSet {x : γ | p x})
(hp : ∀ᵐ (x : α) ∂μ, p (f x))
:
∀ᵐ (x : β) ∂ν, p (g x)
theorem
ProbabilityTheory.IdentDistrib.ae_mem_snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
{t : Set γ}
(tmeas : MeasurableSet t)
(ht : ∀ᵐ (x : α) ∂μ, f x ∈ t)
:
∀ᵐ (x : β) ∂ν, g x ∈ t
theorem
ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[TopologicalSpace γ]
[TopologicalSpace.MetrizableSpace γ]
[OpensMeasurableSpace γ]
[SecondCountableTopology γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
In a second countable topology, the first function in an identically distributed pair is a.e.
strongly measurable. So is the second function, but use h.symm.aestronglyMeasurable_fst as
h.aestronglyMeasurable_snd has a different meaning.
theorem
ProbabilityTheory.IdentDistrib.aestronglyMeasurable_snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[TopologicalSpace γ]
[TopologicalSpace.MetrizableSpace γ]
[BorelSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(hf : MeasureTheory.AEStronglyMeasurable f μ)
:
If f and g are identically distributed and f is a.e. strongly measurable, so is g.
theorem
ProbabilityTheory.IdentDistrib.aestronglyMeasurable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[TopologicalSpace γ]
[TopologicalSpace.MetrizableSpace γ]
[BorelSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
theorem
ProbabilityTheory.IdentDistrib.essSup_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[ConditionallyCompleteLinearOrder γ]
[TopologicalSpace γ]
[OpensMeasurableSpace γ]
[OrderClosedTopology γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
theorem
ProbabilityTheory.IdentDistrib.lintegral_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → ENNReal}
{g : β → ENNReal}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
∫⁻ (x : α), f x ∂μ = ∫⁻ (x : β), g x ∂ν
theorem
ProbabilityTheory.IdentDistrib.integral_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[NormedSpace ℝ γ]
[BorelSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν
theorem
ProbabilityTheory.IdentDistrib.eLpNorm_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[OpensMeasurableSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p ν
@[deprecated ProbabilityTheory.IdentDistrib.eLpNorm_eq]
theorem
ProbabilityTheory.IdentDistrib.snorm_eq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[OpensMeasurableSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(p : ENNReal)
:
MeasureTheory.eLpNorm f p μ = MeasureTheory.eLpNorm g p ν
theorem
ProbabilityTheory.IdentDistrib.memℒp_snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[BorelSpace γ]
{p : ENNReal}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(hf : MeasureTheory.Memℒp f p μ)
:
MeasureTheory.Memℒp g p ν
theorem
ProbabilityTheory.IdentDistrib.memℒp_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[BorelSpace γ]
{p : ENNReal}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
MeasureTheory.Memℒp f p μ ↔ MeasureTheory.Memℒp g p ν
theorem
ProbabilityTheory.IdentDistrib.integrable_snd
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[BorelSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(hf : MeasureTheory.Integrable f μ)
:
theorem
ProbabilityTheory.IdentDistrib.integrable_iff
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[BorelSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
theorem
ProbabilityTheory.IdentDistrib.norm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[BorelSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => ‖f x‖) (fun (x : β) => ‖g x‖) μ ν
theorem
ProbabilityTheory.IdentDistrib.nnnorm
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[NormedAddCommGroup γ]
[BorelSpace γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => ‖f x‖₊) (fun (x : β) => ‖g x‖₊) μ ν
theorem
ProbabilityTheory.IdentDistrib.pow
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Pow γ ℕ]
[MeasurablePow γ ℕ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
{n : ℕ}
:
ProbabilityTheory.IdentDistrib (fun (x : α) => f x ^ n) (fun (x : β) => g x ^ n) μ ν
theorem
ProbabilityTheory.IdentDistrib.sq
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Pow γ ℕ]
[MeasurablePow γ ℕ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => f x ^ 2) (fun (x : β) => g x ^ 2) μ ν
theorem
ProbabilityTheory.IdentDistrib.coe_nnreal_ennreal
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → NNReal}
{g : β → NNReal}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => ↑(f x)) (fun (x : β) => ↑(g x)) μ ν
theorem
ProbabilityTheory.IdentDistrib.mul_const
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Mul γ]
[MeasurableMul γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(c : γ)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => f x * c) (fun (x : β) => g x * c) μ ν
theorem
ProbabilityTheory.IdentDistrib.add_const
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Add γ]
[MeasurableAdd γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(c : γ)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => f x + c) (fun (x : β) => g x + c) μ ν
theorem
ProbabilityTheory.IdentDistrib.const_mul
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Mul γ]
[MeasurableMul γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(c : γ)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => c * f x) (fun (x : β) => c * g x) μ ν
theorem
ProbabilityTheory.IdentDistrib.const_add
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Add γ]
[MeasurableAdd γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(c : γ)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => c + f x) (fun (x : β) => c + g x) μ ν
theorem
ProbabilityTheory.IdentDistrib.div_const
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Div γ]
[MeasurableDiv γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(c : γ)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => f x / c) (fun (x : β) => g x / c) μ ν
theorem
ProbabilityTheory.IdentDistrib.sub_const
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Sub γ]
[MeasurableSub γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(c : γ)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => f x - c) (fun (x : β) => g x - c) μ ν
theorem
ProbabilityTheory.IdentDistrib.const_div
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Div γ]
[MeasurableDiv γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(c : γ)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => c / f x) (fun (x : β) => c / g x) μ ν
theorem
ProbabilityTheory.IdentDistrib.const_sub
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Sub γ]
[MeasurableSub γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
(c : γ)
:
ProbabilityTheory.IdentDistrib (fun (x : α) => c - f x) (fun (x : β) => c - g x) μ ν
theorem
ProbabilityTheory.IdentDistrib.inv
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Inv γ]
[MeasurableInv γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
theorem
ProbabilityTheory.IdentDistrib.neg
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → γ}
{g : β → γ}
[Neg γ]
[MeasurableNeg γ]
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
ProbabilityTheory.IdentDistrib (-f) (-g) μ ν
theorem
ProbabilityTheory.IdentDistrib.evariance_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → ℝ}
{g : β → ℝ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
theorem
ProbabilityTheory.IdentDistrib.variance_eq
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
{f : α → ℝ}
{g : β → ℝ}
(h : ProbabilityTheory.IdentDistrib f g μ ν)
:
theorem
ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib_aux
{α : Type u_1}
[MeasurableSpace α]
{E : Type u_5}
[MeasurableSpace E]
[NormedAddCommGroup E]
[BorelSpace E]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{ι : Type u_6}
{f : ι → α → E}
{j : ι}
{p : ENNReal}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hℒp : MeasureTheory.Memℒp (f j) p μ)
(hfmeas : ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i))
(hf : ∀ (i : ι), ProbabilityTheory.IdentDistrib (f i) (f j) μ μ)
:
This lemma is superseded by Memℒp.uniformIntegrable_of_identDistrib which only requires
AEStronglyMeasurable.
theorem
ProbabilityTheory.Memℒp.uniformIntegrable_of_identDistrib
{α : Type u_1}
[MeasurableSpace α]
{E : Type u_5}
[MeasurableSpace E]
[NormedAddCommGroup E]
[BorelSpace E]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{ι : Type u_6}
{f : ι → α → E}
{j : ι}
{p : ENNReal}
(hp : 1 ≤ p)
(hp' : p ≠ ⊤)
(hℒp : MeasureTheory.Memℒp (f j) p μ)
(hf : ∀ (i : ι), ProbabilityTheory.IdentDistrib (f i) (f j) μ μ)
:
A sequence of identically distributed Lᵖ functions is p-uniformly integrable.
theorem
ProbabilityTheory.indepFun_of_identDistrib_pair
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
[MeasurableSpace α]
[MeasurableSpace β]
[MeasurableSpace γ]
[MeasurableSpace δ]
{μ : MeasureTheory.Measure γ}
{μ' : MeasureTheory.Measure δ}
[MeasureTheory.IsFiniteMeasure μ]
[MeasureTheory.IsFiniteMeasure μ']
{X : γ → α}
{X' : δ → α}
{Y : γ → β}
{Y' : δ → β}
(h_indep : ProbabilityTheory.IndepFun X Y μ)
(h_ident : ProbabilityTheory.IdentDistrib (fun (ω : γ) => (X ω, Y ω)) (fun (ω : δ) => (X' ω, Y' ω)) μ μ')
:
ProbabilityTheory.IndepFun X' Y' μ'
If X and Y are independent and (X, Y) and (X', Y') are identically distributed,
then X' and Y' are independent.