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} [Encodable α] [Inhabited α] [Preorder β] {f : α → β} (hf : Directed (fun x x_1 => x ≥ x_1) f) : Antitone (f ∘ Directed.sequence f hf)

theorem Directed.sequence_le {α : Type u_1} {β : Type u_2} [Encodable α] [Inhabited α] [Preorder β] {f : α → β} (hf : Directed (fun x x_1 => x ≥ x_1) f) (a : α) : f (Directed.sequence f hf (Encodable.encode a + 1)) ≤ f a

theorem prod_iInter {α : 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.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} [TopologicalSpace α] [LinearOrder α] [OrderBot α] [OrderTopology α] : Filter.atBot ≤ nhds ⊥

theorem atTop_le_nhds_top {α : Type u_4} [TopologicalSpace α] [LinearOrder α] [OrderTop α] [OrderTopology α] : Filter.atTop ≤ nhds ⊤

theorem tendsto_of_antitone {ι : Type u_4} {α : Type u_5} [Preorder ι] [TopologicalSpace α] [ConditionallyCompleteLinearOrder α] [OrderTopology α] {f : ι → α} (h_mono : Antitone f) : Filter.Tendsto f Filter.atTop Filter.atBot ∨ ∃ l, Filter.Tendsto f Filter.atTop (nhds l)

theorem ENNReal.ofReal_cinfi {α : Type u_1} (f : α → ℝ) [Nonempty α] : ENNReal.ofReal (⨅ (i : α), f i) = ⨅ (i : α), ENNReal.ofReal (f i)

theorem lintegral_iInf_directed_of_measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [Countable β] {f : β → α → ENNReal} {μ : MeasureTheory.Measure α} (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α : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ) : MeasureTheory.Measure α

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

theorem MeasureTheory.Measure.IicSnd_apply {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ) {s : Set α} (hs : MeasurableSet s) : ↑↑(MeasureTheory.Measure.IicSnd ρ r) s = ↑↑ρ (s ×ˢ Set.Iic r)

theorem MeasureTheory.Measure.IicSnd_univ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ) : ↑↑(MeasureTheory.Measure.IicSnd ρ r) Set.univ = ↑↑ρ (Set.univ ×ˢ Set.Iic r)

theorem MeasureTheory.Measure.IicSnd_mono {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) {r : ℝ} {r' : ℝ} (h_le : r ≤ r') : MeasureTheory.Measure.IicSnd ρ r ≤ MeasureTheory.Measure.IicSnd ρ r'

theorem MeasureTheory.Measure.IicSnd_le_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ) : MeasureTheory.Measure.IicSnd ρ r ≤ MeasureTheory.Measure.fst ρ

theorem MeasureTheory.Measure.IicSnd_ac_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ) : MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.Measure.IicSnd ρ r) (MeasureTheory.Measure.fst ρ)

theorem MeasureTheory.Measure.IsFiniteMeasure.IicSnd {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} [MeasureTheory.IsFiniteMeasure ρ] (r : ℝ) : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.IicSnd ρ r)

theorem MeasureTheory.Measure.iInf_IicSnd_gt {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (t : ℚ) {s : Set α} (hs : MeasurableSet s) [MeasureTheory.IsFiniteMeasure ρ] : ⨅ (r : { r' // t < r' }), ↑↑(MeasureTheory.Measure.IicSnd ρ ↑↑r) s = ↑↑(MeasureTheory.Measure.IicSnd ρ ↑t) s

theorem MeasureTheory.Measure.tendsto_IicSnd_atTop {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) {s : Set α} (hs : MeasurableSet s) : Filter.Tendsto (fun r => ↑↑(MeasureTheory.Measure.IicSnd ρ ↑r) s) Filter.atTop (nhds (↑↑(MeasureTheory.Measure.fst ρ) s))

theorem MeasureTheory.Measure.tendsto_IicSnd_atBot {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] {s : Set α} (hs : MeasurableSet s) : Filter.Tendsto (fun r => ↑↑(MeasureTheory.Measure.IicSnd ρ ↑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α : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (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).

theorem ProbabilityTheory.measurable_preCdf {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} {r : ℚ} : Measurable (ProbabilityTheory.preCdf ρ r)

theorem ProbabilityTheory.withDensity_preCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) [MeasureTheory.IsFiniteMeasure ρ] : MeasureTheory.Measure.withDensity (MeasureTheory.Measure.fst ρ) (ProbabilityTheory.preCdf ρ r) = MeasureTheory.Measure.IicSnd ρ ↑r

theorem ProbabilityTheory.set_lintegral_preCdf_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) {s : Set α} (hs : MeasurableSet s) [MeasureTheory.IsFiniteMeasure ρ] : ∫⁻ (x : α) in s, ProbabilityTheory.preCdf ρ r x ∂MeasureTheory.Measure.fst ρ = ↑↑(MeasureTheory.Measure.IicSnd ρ ↑r) s

theorem ProbabilityTheory.monotone_preCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : ∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ, Monotone fun r => ProbabilityTheory.preCdf ρ r a

theorem ProbabilityTheory.set_lintegral_iInf_gt_preCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (t : ℚ) {s : Set α} (hs : MeasurableSet s) : ∫⁻ (x : α) in s, ⨅ (r : ↑(Set.Ioi t)), ProbabilityTheory.preCdf ρ (↑r) x ∂MeasureTheory.Measure.fst ρ = ↑↑(MeasureTheory.Measure.IicSnd ρ ↑t) s

theorem ProbabilityTheory.preCdf_le_one {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : ∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ, ∀ (r : ℚ), ProbabilityTheory.preCdf ρ r a ≤ 1

theorem ProbabilityTheory.tendsto_lintegral_preCdf_atTop {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : Filter.Tendsto (fun r => ∫⁻ (a : α), ProbabilityTheory.preCdf ρ r a ∂MeasureTheory.Measure.fst ρ) Filter.atTop (nhds (↑↑ρ Set.univ))

theorem ProbabilityTheory.tendsto_lintegral_preCdf_atBot {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : Filter.Tendsto (fun r => ∫⁻ (a : α), ProbabilityTheory.preCdf ρ r a ∂MeasureTheory.Measure.fst ρ) Filter.atBot (nhds 0)

theorem ProbabilityTheory.tendsto_preCdf_atTop_one {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : ∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ, Filter.Tendsto (fun r => ProbabilityTheory.preCdf ρ r a) Filter.atTop (nhds 1)

theorem ProbabilityTheory.tendsto_preCdf_atBot_zero {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : ∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ, Filter.Tendsto (fun r => ProbabilityTheory.preCdf ρ r a) Filter.atBot (nhds 0)

theorem ProbabilityTheory.inf_gt_preCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : ∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ, ∀ (t : ℚ), ⨅ (r : ↑(Set.Ioi t)), ProbabilityTheory.preCdf ρ (↑r) a = ProbabilityTheory.preCdf ρ t a

structure ProbabilityTheory.HasCondCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : Prop

• mono : Monotone fun r => ProbabilityTheory.preCdf ρ r a
• le_one : ∀ (r : ℚ), ProbabilityTheory.preCdf ρ r a ≤ 1
• tendsto_atTop_one : Filter.Tendsto (fun r => ProbabilityTheory.preCdf ρ r a) Filter.atTop (nhds 1)
• tendsto_atBot_zero : Filter.Tendsto (fun r => ProbabilityTheory.preCdf ρ r a) Filter.atBot (nhds 0)
• iInf_rat_gt_eq : ∀ (t : ℚ), ⨅ (r : ↑(Set.Ioi t)), ProbabilityTheory.preCdf ρ (↑r) a = ProbabilityTheory.preCdf ρ t 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).

theorem ProbabilityTheory.hasCondCdf_ae {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : ∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ, ProbabilityTheory.HasCondCdf ρ a

def ProbabilityTheory.condCdfSet {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) : Set α

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

theorem ProbabilityTheory.measurableSet_condCdfSet {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) : MeasurableSet (ProbabilityTheory.condCdfSet ρ)

theorem ProbabilityTheory.hasCondCdf_of_mem_condCdfSet {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} {a : α} (h : a ∈ ProbabilityTheory.condCdfSet ρ) : ProbabilityTheory.HasCondCdf ρ a

theorem ProbabilityTheory.mem_condCdfSet_ae {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : ∀ᵐ (a : α) ∂MeasureTheory.Measure.fst ρ, a ∈ ProbabilityTheory.condCdfSet ρ

noncomputable def ProbabilityTheory.condCdfRat {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) : α → ℚ → ℝ

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.

theorem ProbabilityTheory.condCdfRat_of_not_mem {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (h : ¬a ∈ ProbabilityTheory.condCdfSet ρ) {r : ℚ} : ProbabilityTheory.condCdfRat ρ a r = if r < 0 then 0 else 1

theorem ProbabilityTheory.condCdfRat_of_mem {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (h : a ∈ ProbabilityTheory.condCdfSet ρ) (r : ℚ) : ProbabilityTheory.condCdfRat ρ a r = ENNReal.toReal (ProbabilityTheory.preCdf ρ r a)

theorem ProbabilityTheory.monotone_condCdfRat {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : Monotone (ProbabilityTheory.condCdfRat ρ a)

theorem ProbabilityTheory.measurable_condCdfRat {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (q : ℚ) : Measurable fun a => ProbabilityTheory.condCdfRat ρ a q

theorem ProbabilityTheory.condCdfRat_nonneg {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℚ) : 0 ≤ ProbabilityTheory.condCdfRat ρ a r

theorem ProbabilityTheory.condCdfRat_le_one {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℚ) : ProbabilityTheory.condCdfRat ρ a r ≤ 1

theorem ProbabilityTheory.tendsto_condCdfRat_atBot {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : Filter.Tendsto (ProbabilityTheory.condCdfRat ρ a) Filter.atBot (nhds 0)

theorem ProbabilityTheory.tendsto_condCdfRat_atTop {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : Filter.Tendsto (ProbabilityTheory.condCdfRat ρ a) Filter.atTop (nhds 1)

theorem ProbabilityTheory.condCdfRat_ae_eq {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (r : ℚ) : (fun a => ProbabilityTheory.condCdfRat ρ a r) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.fst ρ)] fun a => ENNReal.toReal (ProbabilityTheory.preCdf ρ r a)

theorem ProbabilityTheory.ofReal_condCdfRat_ae_eq {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (r : ℚ) : (fun a => ENNReal.ofReal (ProbabilityTheory.condCdfRat ρ a r)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.fst ρ)] ProbabilityTheory.preCdf ρ r

theorem ProbabilityTheory.inf_gt_condCdfRat {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (t : ℚ) : ⨅ (r : ↑(Set.Ioi t)), ProbabilityTheory.condCdfRat ρ a ↑r = ProbabilityTheory.condCdfRat ρ a t

@[irreducible]

noncomputable def ProbabilityTheory.condCdf' {α : Type u_4} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) : α → ℝ → ℝ

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

theorem ProbabilityTheory.condCdf'_def {α : Type u_4} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (t : ℝ) : ProbabilityTheory.condCdf' ρ a t = ⨅ (r : { r' // t < ↑r' }), ProbabilityTheory.condCdfRat ρ a ↑r

theorem ProbabilityTheory.condCdf'_def' {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} {a : α} {x : ℝ} : ProbabilityTheory.condCdf' ρ a x = ⨅ (r : { r // x < ↑r }), ProbabilityTheory.condCdfRat ρ a ↑r

theorem ProbabilityTheory.condCdf'_eq_condCdfRat {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℚ) : ProbabilityTheory.condCdf' ρ a ↑r = ProbabilityTheory.condCdfRat ρ a r

theorem ProbabilityTheory.condCdf'_nonneg {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℝ) : 0 ≤ ProbabilityTheory.condCdf' ρ a r

theorem ProbabilityTheory.bddBelow_range_condCdfRat_gt {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (x : ℝ) : BddBelow (Set.range fun r => ProbabilityTheory.condCdfRat ρ a ↑r)

theorem ProbabilityTheory.monotone_condCdf' {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : Monotone (ProbabilityTheory.condCdf' ρ a)

theorem ProbabilityTheory.continuousWithinAt_condCdf'_Ici {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (x : ℝ) : ContinuousWithinAt (ProbabilityTheory.condCdf' ρ a) (Set.Ici x) x

Conditional cdf

noncomputable def ProbabilityTheory.condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : StieltjesFunction

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

theorem ProbabilityTheory.condCdf_eq_condCdfRat {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℚ) : ↑(ProbabilityTheory.condCdf ρ a) ↑r = ProbabilityTheory.condCdfRat ρ a r

theorem ProbabilityTheory.condCdf_nonneg {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℝ) : 0 ≤ ↑(ProbabilityTheory.condCdf ρ a) r

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

theorem ProbabilityTheory.condCdf_le_one {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (x : ℝ) : ↑(ProbabilityTheory.condCdf ρ a) x ≤ 1

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

theorem ProbabilityTheory.tendsto_condCdf_atBot {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : Filter.Tendsto (↑(ProbabilityTheory.condCdf ρ a)) Filter.atBot (nhds 0)

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

theorem ProbabilityTheory.tendsto_condCdf_atTop {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : Filter.Tendsto (↑(ProbabilityTheory.condCdf ρ a)) Filter.atTop (nhds 1)

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

theorem ProbabilityTheory.condCdf_ae_eq {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (r : ℚ) : (fun a => ↑(ProbabilityTheory.condCdf ρ a) ↑r) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.fst ρ)] fun a => ENNReal.toReal (ProbabilityTheory.preCdf ρ r a)

theorem ProbabilityTheory.ofReal_condCdf_ae_eq {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (r : ℚ) : (fun a => ENNReal.ofReal (↑(ProbabilityTheory.condCdf ρ a) ↑r)) =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.fst ρ)] ProbabilityTheory.preCdf ρ r

theorem ProbabilityTheory.measurable_condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (x : ℝ) : Measurable fun a => ↑(ProbabilityTheory.condCdf ρ a) x

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

theorem ProbabilityTheory.set_lintegral_condCdf_rat {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (r : ℚ) {s : Set α} (hs : MeasurableSet s) : ∫⁻ (a : α) in s, ENNReal.ofReal (↑(ProbabilityTheory.condCdf ρ a) ↑r) ∂MeasureTheory.Measure.fst ρ = ↑↑ρ (s ×ˢ Set.Iic ↑r)

Auxiliary lemma for set_lintegral_cond_cdf.

theorem ProbabilityTheory.set_lintegral_condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ) {s : Set α} (hs : MeasurableSet s) : ∫⁻ (a : α) in s, ENNReal.ofReal (↑(ProbabilityTheory.condCdf ρ a) x) ∂MeasureTheory.Measure.fst ρ = ↑↑ρ (s ×ˢ Set.Iic x)

theorem ProbabilityTheory.lintegral_condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ) : ∫⁻ (a : α), ENNReal.ofReal (↑(ProbabilityTheory.condCdf ρ a) x) ∂MeasureTheory.Measure.fst ρ = ↑↑ρ (Set.univ ×ˢ Set.Iic x)

theorem ProbabilityTheory.stronglyMeasurable_condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (x : ℝ) : MeasureTheory.StronglyMeasurable fun a => ↑(ProbabilityTheory.condCdf ρ a) x

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

theorem ProbabilityTheory.integrable_condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ) : MeasureTheory.Integrable fun a => ↑(ProbabilityTheory.condCdf ρ a) x

theorem ProbabilityTheory.set_integral_condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ) {s : Set α} (hs : MeasurableSet s) : ∫ (a : α) in s, ↑(ProbabilityTheory.condCdf ρ a) x ∂MeasureTheory.Measure.fst ρ = ENNReal.toReal (↑↑ρ (s ×ˢ Set.Iic x))

theorem ProbabilityTheory.integral_condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℝ) : ∫ (a : α), ↑(ProbabilityTheory.condCdf ρ a) x ∂MeasureTheory.Measure.fst ρ = ENNReal.toReal (↑↑ρ (Set.univ ×ˢ Set.Iic x))

theorem ProbabilityTheory.measure_condCdf_Iic {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (x : ℝ) : ↑↑(StieltjesFunction.measure (ProbabilityTheory.condCdf ρ a)) (Set.Iic x) = ENNReal.ofReal (↑(ProbabilityTheory.condCdf ρ a) x)

theorem ProbabilityTheory.measure_condCdf_univ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : ↑↑(StieltjesFunction.measure (ProbabilityTheory.condCdf ρ a)) Set.univ = 1

instance ProbabilityTheory.instIsProbabilityMeasure {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : MeasureTheory.IsProbabilityMeasure (StieltjesFunction.measure (ProbabilityTheory.condCdf ρ a))

theorem ProbabilityTheory.measurable_measure_condCdf {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) : Measurable fun a => StieltjesFunction.measure (ProbabilityTheory.condCdf ρ a)

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