# mathlib3documentation

probability.kernel.cond_cdf

# Conditional cumulative distribution function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given ρ : measure (α × ℝ), we define the conditional cumulative distribution function (conditional cdf) of ρ. It is a function cond_cdf ρ : α → ℝ → ℝ such that if ρ is a finite measure, then for all a : α cond_cdf ρ a is monotone and right-continuous with limit 0 at -∞ and limit 1 at +∞, and such that for all x : ℝ, a ↦ cond_cdf ρ a x is measurable. For all x : ℝ and measurable set s, that function satisfies ∫⁻ a in s, ennreal.of_real (cond_cdf ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x).

## Main definitions #

• probability_theory.cond_cdf ρ : α → stieltjes_function: the conditional cdf of ρ : measure (α × ℝ). A stieltjes_function is a function ℝ → ℝ which is monotone and right-continuous.

## Main statements #

• probability_theory.set_lintegral_cond_cdf: for all a : α and x : ℝ, all measurable set s, ∫⁻ a in s, ennreal.of_real (cond_cdf ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x).

## References #

The construction of the conditional cdf in this file follows the proof of Theorem 3.4 in O. Kallenberg, Foundations of modern probability.

## TODO #

• The conditional cdf can be used to define the cdf of a real measure by using the conditional cdf of (measure.dirac unit.star).prod μ : measure (unit × ℝ).
theorem directed.sequence_anti {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α β} (hf : f) :
antitone (f hf)
theorem directed.sequence_le {α : Type u_1} {β : Type u_2} [encodable α] [inhabited α] [preorder β] {f : α β} (hf : f) (a : α) :
f hf + 1)) f a
theorem prod_Inter {α : Type u_1} {β : Type u_2} {ι : Type u_3} {s : set α} {t : ι set β} [hι : nonempty ι] :
(s ×ˢ (i : ι), t i) = (i : ι), s ×ˢ t i
theorem real.Inter_Iic_rat  :
( (r : ), set.Iic r) =
theorem at_bot_le_nhds_bot {α : Type u_1} [linear_order α] [order_bot α]  :
theorem at_top_le_nhds_top {α : Type u_1} [linear_order α] [order_top α]  :
theorem tendsto_of_antitone {ι : Type u_1} {α : Type u_2} [preorder ι] {f : ι α} (h_mono : antitone f) :
(l : α),
theorem ennreal.of_real_cinfi {α : Type u_1} (f : α ) [nonempty α] :
ennreal.of_real ( (i : α), f i) = (i : α), ennreal.of_real (f i)
theorem lintegral_infi_directed_of_measurable {α : Type u_1} {β : Type u_2} {mα : measurable_space α} [countable β] {f : β } {μ : measure_theory.measure α} (hμ : μ 0) (hf : (b : β), measurable (f b)) (hf_int : (b : β), ∫⁻ (a : α), f b a μ ) (h_directed : f) :
∫⁻ (a : α), ( (b : β), f b a) μ = (b : β), ∫⁻ (a : α), f b a μ

Monotone convergence for an infimum over a directed family and indexed by a countable type

theorem is_pi_system_Iic {α : Type u_1}  :
theorem is_pi_system_Ici {α : Type u_1}  :
noncomputable def measure_theory.measure.Iic_snd {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) :

Measure on α such that for a measurable set s, ρ.Iic_snd r s = ρ (s ×ˢ Iic r).

Equations
theorem measure_theory.measure.Iic_snd_apply {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) {s : set α} (hs : measurable_set s) :
(ρ.Iic_snd r) s = ρ (s ×ˢ set.Iic r)
theorem measure_theory.measure.Iic_snd_mono {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) {r r' : } (h_le : r r') :
ρ.Iic_snd r ρ.Iic_snd r'
theorem measure_theory.measure.Iic_snd_le_fst {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) :
ρ.Iic_snd r ρ.fst
theorem measure_theory.measure.infi_Iic_snd_gt {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (t : ) {s : set α} (hs : measurable_set s)  :
( (r : {r' // t < r'}), (ρ.Iic_snd r) s) = (ρ.Iic_snd t) s

### Auxiliary definitions #

We build towards the definition of probability_theory.cond_cdf. We first define probability_theory.pre_cdf, a function defined on α × ℚ with the properties of a cdf almost everywhere. We then introduce probability_theory.cond_cdf_rat, a function on α × ℚ which has the properties of a cdf for all a : α. We finally extend to ℝ.

noncomputable def probability_theory.pre_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) :

pre_cdf is the Radon-Nikodym derivative of ρ.Iic_snd with respect to ρ.fst at each r : ℚ. This function ℚ → α → ℝ≥0∞ is such that for almost all a : α, the function ℚ → ℝ≥0∞ satisfies the properties of a cdf (monotone with limit 0 at -∞ and 1 at +∞, right-continuous).

We define this function on ℚ and not ℝ because ℚ is countable, which allows us to prove properties of the form ∀ᵐ a ∂ρ.fst, ∀ q, P (pre_cdf q a), instead of the weaker ∀ q, ∀ᵐ a ∂ρ.fst, P (pre_cdf q a).

Equations
theorem probability_theory.set_lintegral_pre_cdf_fst {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) {s : set α} (hs : measurable_set s)  :
∫⁻ (x : α) in s, ρ.fst = (ρ.Iic_snd r) s
theorem probability_theory.monotone_pre_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × ))  :
∀ᵐ (a : α) ρ.fst, monotone (λ (r : ),
theorem probability_theory.set_lintegral_infi_gt_pre_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (t : ) {s : set α} (hs : measurable_set s) :
∫⁻ (x : α) in s, ( (r : (set.Ioi t)), ρ.fst = (ρ.Iic_snd t) s
theorem probability_theory.pre_cdf_le_one {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × ))  :
∀ᵐ (a : α) ρ.fst, (r : ), 1
theorem probability_theory.inf_gt_pre_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × ))  :
∀ᵐ (a : α) ρ.fst, (t : ), ( (r : (set.Ioi t)), =
structure probability_theory.has_cond_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) :
Prop

A product measure on α × ℝ is said to have a conditional cdf at a : α if pre_cdf is monotone with limit 0 at -∞ and 1 at +∞, and is right continuous. This property holds almost everywhere (see has_cond_cdf_ae).

theorem probability_theory.has_cond_cdf_ae {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × ))  :
∀ᵐ (a : α) ρ.fst,

A measurable set of elements of α such that ρ has a conditional cdf at all a ∈ cond_cdf_set.

Equations
theorem probability_theory.has_cond_cdf_of_mem_cond_cdf_set {α : Type u_1} {mα : measurable_space α} {ρ : measure_theory.measure × )} {a : α} (h : a ) :
noncomputable def probability_theory.cond_cdf_rat {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) :
α

Conditional cdf of the measure given the value on α, restricted to the rationals. It is defined to be pre_cdf if a ∈ cond_cdf_set, and a default cdf-like function otherwise. This is an auxiliary definition used to define cond_cdf.

Equations
theorem probability_theory.cond_cdf_rat_of_not_mem {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (h : a ) {r : } :
= ite (r < 0) 0 1
theorem probability_theory.cond_cdf_rat_of_mem {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (h : a ) (r : ) :
theorem probability_theory.monotone_cond_cdf_rat {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) :
theorem probability_theory.measurable_cond_cdf_rat {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (q : ) :
measurable (λ (a : α),
theorem probability_theory.cond_cdf_rat_nonneg {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (r : ) :
theorem probability_theory.cond_cdf_rat_le_one {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (r : ) :
theorem probability_theory.cond_cdf_rat_ae_eq {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) :
(λ (a : α), =ᵐ[ρ.fst] λ (a : α), a).to_real
theorem probability_theory.of_real_cond_cdf_rat_ae_eq {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) :
(λ (a : α), =ᵐ[ρ.fst]
theorem probability_theory.inf_gt_cond_cdf_rat {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (t : ) :
( (r : (set.Ioi t)), =
@[irreducible]
noncomputable def probability_theory.cond_cdf' {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) :
α

Conditional cdf of the measure given the value on α, as a plain function. This is an auxiliary definition used to define cond_cdf.

Equations
theorem probability_theory.cond_cdf'_def {α : Type u_1} {mα : measurable_space α} {ρ : measure_theory.measure × )} {a : α} {x : } :
= (r : {r // x < r}),
theorem probability_theory.cond_cdf'_eq_cond_cdf_rat {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (r : ) :
theorem probability_theory.cond_cdf'_nonneg {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (r : ) :
theorem probability_theory.bdd_below_range_cond_cdf_rat_gt {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (x : ) :
bdd_below (set.range (λ (r : {r' // x < r'}),
theorem probability_theory.monotone_cond_cdf' {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) :

### Conditional cdf #

noncomputable def probability_theory.cond_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) :

Conditional cdf of the measure given the value on α, as a Stieltjes function.

Equations
theorem probability_theory.cond_cdf_eq_cond_cdf_rat {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (r : ) :
theorem probability_theory.cond_cdf_nonneg {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (r : ) :
0 r

The conditional cdf is non-negative for all a : α.

theorem probability_theory.cond_cdf_le_one {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (x : ) :
x 1

The conditional cdf is lower or equal to 1 for all a : α.

theorem probability_theory.tendsto_cond_cdf_at_bot {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) :

The conditional cdf tends to 0 at -∞ for all a : α.

theorem probability_theory.tendsto_cond_cdf_at_top {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) :

The conditional cdf tends to 1 at +∞ for all a : α.

theorem probability_theory.cond_cdf_ae_eq {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) :
(λ (a : α), r) =ᵐ[ρ.fst] λ (a : α), a).to_real
theorem probability_theory.of_real_cond_cdf_ae_eq {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) :
(λ (a : α), ennreal.of_real ( r)) =ᵐ[ρ.fst]
theorem probability_theory.measurable_cond_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (x : ) :
measurable (λ (a : α), x)

The conditional cdf is a measurable function of a : α for all x : ℝ.

theorem probability_theory.set_lintegral_cond_cdf_rat {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (r : ) {s : set α} (hs : measurable_set s) :
∫⁻ (a : α) in s, ρ.fst = ρ (s ×ˢ set.Iic r)

Auxiliary lemma for set_lintegral_cond_cdf.

theorem probability_theory.set_lintegral_cond_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (x : ) {s : set α} (hs : measurable_set s) :
∫⁻ (a : α) in s, ρ.fst = ρ (s ×ˢ set.Iic x)
theorem probability_theory.lintegral_cond_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (x : ) :
∫⁻ (a : α), ρ.fst = ρ

The conditional cdf is a strongly measurable function of a : α for all x : ℝ.

theorem probability_theory.integrable_cond_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (x : ) :
measure_theory.integrable (λ (a : α), x) ρ.fst
theorem probability_theory.set_integral_cond_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (x : ) {s : set α} (hs : measurable_set s) :
(a : α) in s, x ρ.fst = (ρ (s ×ˢ set.Iic x)).to_real
theorem probability_theory.integral_cond_cdf {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (x : ) :
(a : α), x ρ.fst = (ρ (set.univ ×ˢ set.Iic x)).to_real
theorem probability_theory.measure_cond_cdf_Iic {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) (x : ) :
theorem probability_theory.measure_cond_cdf_univ {α : Type u_1} {mα : measurable_space α} (ρ : measure_theory.measure × )) (a : α) :
= 1
@[protected, instance]

The function a ↦ (cond_cdf ρ a).measure is measurable.