# Documentation

Mathlib.Probability.Kernel.CondCdf

# Conditional cumulative distribution function #

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][kallenberg2021].

## 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} [] [] [] {f : αβ} (hf : Directed (fun x x_1 => x x_1) f) :
theorem Directed.sequence_le {α : Type u_1} {β : Type u_2} [] [] [] {f : αβ} (hf : Directed (fun x x_1 => x x_1) f) (a : α) :
f (Directed.sequence f hf ()) f a
theorem prod_iInter {α : Type u_1} {β : Type u_2} {ι : Type u_3} {s : Set α} {t : ιSet β} [hι : ] :
s ×ˢ ⋂ (i : ι), t i = ⋂ (i : ι), s ×ˢ t i
theorem Real.iUnion_Iic_rat :
⋃ (r : ), Set.Iic r = Set.univ
theorem Real.iInter_Iic_rat :
⋂ (r : ), Set.Iic r =
theorem atBot_le_nhds_bot {α : Type u_4} [] [] [] [] :
Filter.atBot
theorem atTop_le_nhds_top {α : Type u_4} [] [] [] [] :
Filter.atTop
theorem tendsto_of_antitone {ι : Type u_4} {α : Type u_5} [] [] [] {f : ια} (h_mono : ) :
Filter.Tendsto f Filter.atTop Filter.atBot l, Filter.Tendsto f Filter.atTop (nhds l)
theorem ENNReal.ofReal_cinfi {α : Type u_1} (f : α) [] :
ENNReal.ofReal (⨅ (i : α), f i) = ⨅ (i : α), ENNReal.ofReal (f i)
theorem lintegral_iInf_directed_of_measurable {α : Type u_1} {β : Type u_2} {mα : } [] {f : βαENNReal} {μ : } (hμ : μ 0) (hf : ∀ (b : β), Measurable (f b)) (hf_int : ∀ (b : β), ∫⁻ (a : α), f b aμ ) (h_directed : Directed (fun x x_1 => x x_1) 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

noncomputable def MeasureTheory.Measure.IicSnd {α : Type u_1} {mα : } (ρ : ) (r : ) :

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

Instances For
theorem MeasureTheory.Measure.IicSnd_apply {α : Type u_1} {mα : } (ρ : ) (r : ) {s : Set α} (hs : ) :
↑() s = ρ (s ×ˢ )
theorem MeasureTheory.Measure.IicSnd_univ {α : Type u_1} {mα : } (ρ : ) (r : ) :
↑() Set.univ = ρ (Set.univ ×ˢ )
theorem MeasureTheory.Measure.IicSnd_mono {α : Type u_1} {mα : } (ρ : ) {r : } {r' : } (h_le : r r') :
theorem MeasureTheory.Measure.IicSnd_le_fst {α : Type u_1} {mα : } (ρ : ) (r : ) :
theorem MeasureTheory.Measure.IicSnd_ac_fst {α : Type u_1} {mα : } (ρ : ) (r : ) :
theorem MeasureTheory.Measure.IsFiniteMeasure.IicSnd {α : Type u_1} {mα : } {ρ : } (r : ) :
theorem MeasureTheory.Measure.iInf_IicSnd_gt {α : Type u_1} {mα : } (ρ : ) (t : ) {s : Set α} (hs : ) :
⨅ (r : { r' // t < r' }), ↑() s = ↑() s
theorem MeasureTheory.Measure.tendsto_IicSnd_atTop {α : Type u_1} {mα : } (ρ : ) {s : Set α} (hs : ) :
Filter.Tendsto (fun r => ↑() s) Filter.atTop (nhds ( s))
theorem MeasureTheory.Measure.tendsto_IicSnd_atBot {α : Type u_1} {mα : } (ρ : ) {s : Set α} (hs : ) :
Filter.Tendsto (fun r => ↑() s) Filter.atBot (nhds 0)

### 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 ProbabilityTheory.preCdf {α : Type u_1} {mα : } (ρ : ) (r : ) :
αENNReal

pre_cdf is the Radon-Nikodym derivative of ρ.IicSnd 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).

Instances For
theorem ProbabilityTheory.measurable_preCdf {α : Type u_1} {mα : } {ρ : } {r : } :
theorem ProbabilityTheory.withDensity_preCdf {α : Type u_1} {mα : } (ρ : ) (r : ) :
theorem ProbabilityTheory.set_lintegral_preCdf_fst {α : Type u_1} {mα : } (ρ : ) (r : ) {s : Set α} (hs : ) :
∫⁻ (x : α) in s, = ↑() s
theorem ProbabilityTheory.monotone_preCdf {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂, Monotone fun r =>
theorem ProbabilityTheory.set_lintegral_iInf_gt_preCdf {α : Type u_1} {mα : } (ρ : ) (t : ) {s : Set α} (hs : ) :
∫⁻ (x : α) in s, ⨅ (r : ↑()), ProbabilityTheory.preCdf ρ (r) x = ↑() s
theorem ProbabilityTheory.preCdf_le_one {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂, ∀ (r : ), 1
theorem ProbabilityTheory.tendsto_lintegral_preCdf_atTop {α : Type u_1} {mα : } (ρ : ) :
Filter.Tendsto (fun r => ∫⁻ (a : α), ) Filter.atTop (nhds (ρ Set.univ))
theorem ProbabilityTheory.tendsto_lintegral_preCdf_atBot {α : Type u_1} {mα : } (ρ : ) :
Filter.Tendsto (fun r => ∫⁻ (a : α), ) Filter.atBot (nhds 0)
theorem ProbabilityTheory.tendsto_preCdf_atTop_one {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂, Filter.Tendsto (fun r => ) Filter.atTop (nhds 1)
theorem ProbabilityTheory.tendsto_preCdf_atBot_zero {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂, Filter.Tendsto (fun r => ) Filter.atBot (nhds 0)
theorem ProbabilityTheory.inf_gt_preCdf {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂, ∀ (t : ), ⨅ (r : ↑()), ProbabilityTheory.preCdf ρ (r) a =
structure ProbabilityTheory.HasCondCdf {α : Type u_1} {mα : } (ρ : ) (a : α) :

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

Instances For
theorem ProbabilityTheory.hasCondCdf_ae {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂,
def ProbabilityTheory.condCdfSet {α : Type u_1} {mα : } (ρ : ) :
Set α

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

Instances For
theorem ProbabilityTheory.measurableSet_condCdfSet {α : Type u_1} {mα : } (ρ : ) :
theorem ProbabilityTheory.hasCondCdf_of_mem_condCdfSet {α : Type u_1} {mα : } {ρ : } {a : α} (h : ) :
theorem ProbabilityTheory.mem_condCdfSet_ae {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂,
noncomputable def ProbabilityTheory.condCdfRat {α : Type u_1} {mα : } (ρ : ) :
α

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

Instances For
theorem ProbabilityTheory.condCdfRat_of_not_mem {α : Type u_1} {mα : } (ρ : ) (a : α) (h : ) {r : } :
= if r < 0 then 0 else 1
theorem ProbabilityTheory.condCdfRat_of_mem {α : Type u_1} {mα : } (ρ : ) (a : α) (h : ) (r : ) :
theorem ProbabilityTheory.monotone_condCdfRat {α : Type u_1} {mα : } (ρ : ) (a : α) :
theorem ProbabilityTheory.measurable_condCdfRat {α : Type u_1} {mα : } (ρ : ) (q : ) :
Measurable fun a =>
theorem ProbabilityTheory.condCdfRat_nonneg {α : Type u_1} {mα : } (ρ : ) (a : α) (r : ) :
theorem ProbabilityTheory.condCdfRat_le_one {α : Type u_1} {mα : } (ρ : ) (a : α) (r : ) :
theorem ProbabilityTheory.tendsto_condCdfRat_atBot {α : Type u_1} {mα : } (ρ : ) (a : α) :
Filter.Tendsto () Filter.atBot (nhds 0)
theorem ProbabilityTheory.tendsto_condCdfRat_atTop {α : Type u_1} {mα : } (ρ : ) (a : α) :
Filter.Tendsto () Filter.atTop (nhds 1)
theorem ProbabilityTheory.condCdfRat_ae_eq {α : Type u_1} {mα : } (ρ : ) (r : ) :
(fun a => ) =ᶠ[] fun a =>
theorem ProbabilityTheory.ofReal_condCdfRat_ae_eq {α : Type u_1} {mα : } (ρ : ) (r : ) :
(fun a => ) =ᶠ[]
theorem ProbabilityTheory.inf_gt_condCdfRat {α : Type u_1} {mα : } (ρ : ) (a : α) (t : ) :
⨅ (r : ↑()), =
@[irreducible]
noncomputable def ProbabilityTheory.condCdf' {α : Type u_4} {mα : } (ρ : ) :
α

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

Instances For
theorem ProbabilityTheory.condCdf'_def {α : Type u_4} {mα : } (ρ : ) (a : α) (t : ) :
= ⨅ (r : { r' // t < r' }),
theorem ProbabilityTheory.condCdf'_def' {α : Type u_1} {mα : } {ρ : } {a : α} {x : } :
= ⨅ (r : { r // x < r }),
theorem ProbabilityTheory.condCdf'_eq_condCdfRat {α : Type u_1} {mα : } (ρ : ) (a : α) (r : ) :
theorem ProbabilityTheory.condCdf'_nonneg {α : Type u_1} {mα : } (ρ : ) (a : α) (r : ) :
0
theorem ProbabilityTheory.bddBelow_range_condCdfRat_gt {α : Type u_1} {mα : } (ρ : ) (a : α) (x : ) :
BddBelow (Set.range fun r => )
theorem ProbabilityTheory.monotone_condCdf' {α : Type u_1} {mα : } (ρ : ) (a : α) :
theorem ProbabilityTheory.continuousWithinAt_condCdf'_Ici {α : Type u_1} {mα : } (ρ : ) (a : α) (x : ) :

### Conditional cdf #

noncomputable def ProbabilityTheory.condCdf {α : Type u_1} {mα : } (ρ : ) (a : α) :

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

Instances For
theorem ProbabilityTheory.condCdf_eq_condCdfRat {α : Type u_1} {mα : } (ρ : ) (a : α) (r : ) :
↑() r =
theorem ProbabilityTheory.condCdf_nonneg {α : Type u_1} {mα : } (ρ : ) (a : α) (r : ) :
0 ↑() r

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

theorem ProbabilityTheory.condCdf_le_one {α : Type u_1} {mα : } (ρ : ) (a : α) (x : ) :
↑() x 1

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

theorem ProbabilityTheory.tendsto_condCdf_atBot {α : Type u_1} {mα : } (ρ : ) (a : α) :
Filter.Tendsto (↑()) Filter.atBot (nhds 0)

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

theorem ProbabilityTheory.tendsto_condCdf_atTop {α : Type u_1} {mα : } (ρ : ) (a : α) :
Filter.Tendsto (↑()) Filter.atTop (nhds 1)

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

theorem ProbabilityTheory.condCdf_ae_eq {α : Type u_1} {mα : } (ρ : ) (r : ) :
(fun a => ↑() r) =ᶠ[] fun a =>
theorem ProbabilityTheory.ofReal_condCdf_ae_eq {α : Type u_1} {mα : } (ρ : ) (r : ) :
(fun a => ENNReal.ofReal (↑() r)) =ᶠ[]
theorem ProbabilityTheory.measurable_condCdf {α : Type u_1} {mα : } (ρ : ) (x : ) :
Measurable fun a => ↑() x

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

theorem ProbabilityTheory.set_lintegral_condCdf_rat {α : Type u_1} {mα : } (ρ : ) (r : ) {s : Set α} (hs : ) :
∫⁻ (a : α) in s, ENNReal.ofReal (↑() r) = ρ (s ×ˢ Set.Iic r)

Auxiliary lemma for set_lintegral_cond_cdf.

theorem ProbabilityTheory.set_lintegral_condCdf {α : Type u_1} {mα : } (ρ : ) (x : ) {s : Set α} (hs : ) :
∫⁻ (a : α) in s, ENNReal.ofReal (↑() x) = ρ (s ×ˢ )
theorem ProbabilityTheory.lintegral_condCdf {α : Type u_1} {mα : } (ρ : ) (x : ) :
∫⁻ (a : α), ENNReal.ofReal (↑() x) = ρ (Set.univ ×ˢ )
theorem ProbabilityTheory.stronglyMeasurable_condCdf {α : Type u_1} {mα : } (ρ : ) (x : ) :

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

theorem ProbabilityTheory.integrable_condCdf {α : Type u_1} {mα : } (ρ : ) (x : ) :
MeasureTheory.Integrable fun a => ↑() x
theorem ProbabilityTheory.set_integral_condCdf {α : Type u_1} {mα : } (ρ : ) (x : ) {s : Set α} (hs : ) :
∫ (a : α) in s, ↑() x = ENNReal.toReal (ρ (s ×ˢ ))
theorem ProbabilityTheory.integral_condCdf {α : Type u_1} {mα : } (ρ : ) (x : ) :
∫ (a : α), ↑() x = ENNReal.toReal (ρ (Set.univ ×ˢ ))
theorem ProbabilityTheory.measure_condCdf_Iic {α : Type u_1} {mα : } (ρ : ) (a : α) (x : ) :
() = ENNReal.ofReal (↑() x)
theorem ProbabilityTheory.measure_condCdf_univ {α : Type u_1} {mα : } (ρ : ) (a : α) :
Set.univ = 1
instance ProbabilityTheory.instIsProbabilityMeasure {α : Type u_1} {mα : } (ρ : ) (a : α) :
theorem ProbabilityTheory.measurable_measure_condCdf {α : Type u_1} {mα : } (ρ : ) :
Measurable fun a =>

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