mathlib documentation

probability.ident_distrib

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 #

There are two main kind 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 ident_distrib.foo_eq, the second one as ident_distrib.foo_snd (in the latter case, to deduce a property of f from one of g, use h.symm.foo_snd where h : ident_distrib f g μ ν). For instance:

We also register several dot notation shortcuts for convenience. For instance, if h : ident_distrib 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 probability_theory.ident_distrib {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] (f : α → γ) (g : β → γ) (μ : measure_theory.measure α . "volume_tac") (ν : measure_theory.measure β . "volume_tac") :
Prop

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.

@[protected]
theorem probability_theory.ident_distrib.refl {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} {f : α → γ} (hf : ae_measurable f μ) :
@[protected]
theorem probability_theory.ident_distrib.symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} (h : probability_theory.ident_distrib f g μ ν) :
@[protected]
theorem probability_theory.ident_distrib.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} {ρ : measure_theory.measure δ} {h : δ → γ} (h₁ : probability_theory.ident_distrib f g μ ν) (h₂ : probability_theory.ident_distrib g h ν ρ) :
@[protected]
theorem probability_theory.ident_distrib.comp_of_ae_measurable {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} {u : γ → δ} (h : probability_theory.ident_distrib f g μ ν) (hu : ae_measurable u (measure_theory.measure.map f μ)) :
@[protected]
theorem probability_theory.ident_distrib.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} {u : γ → δ} (h : probability_theory.ident_distrib f g μ ν) (hu : measurable u) :
@[protected]
theorem probability_theory.ident_distrib.of_ae_eq {α : Type u_1} {γ : Type u_3} [measurable_space α] [measurable_space γ] {μ : measure_theory.measure α} {f g : α → γ} (hf : ae_measurable f μ) (heq : f =ᵐ[μ] g) :
theorem probability_theory.ident_distrib.measure_mem_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} (h : probability_theory.ident_distrib f g μ ν) {s : set γ} (hs : measurable_set s) :
μ (f ⁻¹' s) = ν (g ⁻¹' s)
theorem probability_theory.ident_distrib.measure_preimage_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} (h : probability_theory.ident_distrib f g μ ν) {s : set γ} (hs : measurable_set s) :
μ (f ⁻¹' s) = ν (g ⁻¹' s)

Alias of probability_theory.ident_distrib.measure_mem_eq.

theorem probability_theory.ident_distrib.ae_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} (h : probability_theory.ident_distrib f g μ ν) {p : γ → Prop} (pmeas : measurable_set {x : γ | p x}) (hp : ∀ᵐ (x : α) ∂μ, p (f x)) :
∀ᵐ (x : β) ∂ν, p (g x)
theorem probability_theory.ident_distrib.ae_mem_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} (h : probability_theory.ident_distrib f g μ ν) {t : set γ} (tmeas : measurable_set t) (ht : ∀ᵐ (x : α) ∂μ, f x t) :
∀ᵐ (x : β) ∂ν, g x t

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.ae_strongly_measurable_fst as h.ae_strongly_measurable_snd has a different meaning.

If f and g are identically distributed and f is a.e. strongly measurable, so is g.

theorem probability_theory.ident_distrib.lintegral_eq {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → ennreal} {g : β → ennreal} (h : probability_theory.ident_distrib f g μ ν) :
∫⁻ (x : α), f x μ = ∫⁻ (x : β), g x ν
theorem probability_theory.ident_distrib.integral_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [normed_add_comm_group γ] [normed_space γ] [complete_space γ] [borel_space γ] (h : probability_theory.ident_distrib f g μ ν) :
(x : α), f x μ = (x : β), g x ν
theorem probability_theory.ident_distrib.snorm_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [normed_add_comm_group γ] [opens_measurable_space γ] (h : probability_theory.ident_distrib f g μ ν) (p : ennreal) :
theorem probability_theory.ident_distrib.mem_ℒp_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [normed_add_comm_group γ] [borel_space γ] {p : ennreal} (h : probability_theory.ident_distrib f g μ ν) (hf : measure_theory.mem_ℒp f p μ) :
theorem probability_theory.ident_distrib.mem_ℒp_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [normed_add_comm_group γ] [borel_space γ] {p : ennreal} (h : probability_theory.ident_distrib f g μ ν) :
theorem probability_theory.ident_distrib.integrable_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [normed_add_comm_group γ] [borel_space γ] (h : probability_theory.ident_distrib f g μ ν) (hf : measure_theory.integrable f μ) :
theorem probability_theory.ident_distrib.integrable_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [normed_add_comm_group γ] [borel_space γ] (h : probability_theory.ident_distrib f g μ ν) :
@[protected]
theorem probability_theory.ident_distrib.norm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [normed_add_comm_group γ] [borel_space γ] (h : probability_theory.ident_distrib f g μ ν) :
probability_theory.ident_distrib (λ (x : α), f x) (λ (x : β), g x) μ ν
@[protected]
theorem probability_theory.ident_distrib.nnnorm {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [normed_add_comm_group γ] [borel_space γ] (h : probability_theory.ident_distrib f g μ ν) :
probability_theory.ident_distrib (λ (x : α), f x∥₊) (λ (x : β), g x∥₊) μ ν
@[protected]
theorem probability_theory.ident_distrib.pow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_pow γ ] [has_measurable_pow γ ] (h : probability_theory.ident_distrib f g μ ν) {n : } :
probability_theory.ident_distrib (λ (x : α), f x ^ n) (λ (x : β), g x ^ n) μ ν
@[protected]
theorem probability_theory.ident_distrib.sq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_pow γ ] [has_measurable_pow γ ] (h : probability_theory.ident_distrib f g μ ν) :
probability_theory.ident_distrib (λ (x : α), f x ^ 2) (λ (x : β), g x ^ 2) μ ν
@[protected]
theorem probability_theory.ident_distrib.coe_nnreal_ennreal {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → nnreal} {g : β → nnreal} (h : probability_theory.ident_distrib f g μ ν) :
probability_theory.ident_distrib (λ (x : α), (f x)) (λ (x : β), (g x)) μ ν
theorem probability_theory.ident_distrib.mul_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_mul γ] [has_measurable_mul γ] (h : probability_theory.ident_distrib f g μ ν) (c : γ) :
probability_theory.ident_distrib (λ (x : α), f x * c) (λ (x : β), g x * c) μ ν
theorem probability_theory.ident_distrib.add_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_add γ] [has_measurable_add γ] (h : probability_theory.ident_distrib f g μ ν) (c : γ) :
probability_theory.ident_distrib (λ (x : α), f x + c) (λ (x : β), g x + c) μ ν
theorem probability_theory.ident_distrib.const_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_mul γ] [has_measurable_mul γ] (h : probability_theory.ident_distrib f g μ ν) (c : γ) :
probability_theory.ident_distrib (λ (x : α), c * f x) (λ (x : β), c * g x) μ ν
theorem probability_theory.ident_distrib.const_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_add γ] [has_measurable_add γ] (h : probability_theory.ident_distrib f g μ ν) (c : γ) :
probability_theory.ident_distrib (λ (x : α), c + f x) (λ (x : β), c + g x) μ ν
theorem probability_theory.ident_distrib.sub_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_sub γ] [has_measurable_sub γ] (h : probability_theory.ident_distrib f g μ ν) (c : γ) :
probability_theory.ident_distrib (λ (x : α), f x - c) (λ (x : β), g x - c) μ ν
theorem probability_theory.ident_distrib.div_const {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_div γ] [has_measurable_div γ] (h : probability_theory.ident_distrib f g μ ν) (c : γ) :
probability_theory.ident_distrib (λ (x : α), f x / c) (λ (x : β), g x / c) μ ν
theorem probability_theory.ident_distrib.const_div {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_div γ] [has_measurable_div γ] (h : probability_theory.ident_distrib f g μ ν) (c : γ) :
probability_theory.ident_distrib (λ (x : α), c / f x) (λ (x : β), c / g x) μ ν
theorem probability_theory.ident_distrib.const_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} [measurable_space α] [measurable_space β] [measurable_space γ] {μ : measure_theory.measure α} {ν : measure_theory.measure β} {f : α → γ} {g : β → γ} [has_sub γ] [has_measurable_sub γ] (h : probability_theory.ident_distrib f g μ ν) (c : γ) :
probability_theory.ident_distrib (λ (x : α), c - f x) (λ (x : β), c - g x) μ ν
theorem probability_theory.mem_ℒp.uniform_integrable_of_ident_distrib_aux {α : Type u_1} [measurable_space α] {E : Type u_5} [measurable_space E] [normed_add_comm_group E] [borel_space E] [topological_space.second_countable_topology E] {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {ι : Type u_2} {f : ι → α → E} {j : ι} {p : ennreal} (hp : 1 p) (hp' : p ) (hℒp : measure_theory.mem_ℒp (f j) p μ) (hfmeas : ∀ (i : ι), measure_theory.strongly_measurable (f i)) (hf : ∀ (i : ι), probability_theory.ident_distrib (f i) (f j) μ μ) :

This lemma is superceded by mem_ℒp.uniform_integrable_of_ident_distrib which only require ae_strongly_measurable.

theorem probability_theory.mem_ℒp.uniform_integrable_of_ident_distrib {α : Type u_1} [measurable_space α] {E : Type u_5} [measurable_space E] [normed_add_comm_group E] [borel_space E] [topological_space.second_countable_topology E] {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] {ι : Type u_2} {f : ι → α → E} {j : ι} {p : ennreal} (hp : 1 p) (hp' : p ) (hℒp : measure_theory.mem_ℒp (f j) p μ) (hf : ∀ (i : ι), probability_theory.ident_distrib (f i) (f j) μ μ) :

A sequence of identically distributed Lᵖ functions is p-uniformly integrable.