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 Real.iUnion_Iic_rat : ⋃ (r : ℚ), Set.Iic ↑r = Set.univ

theorem Real.iInter_Iic_rat : ⋂ (r : ℚ), Set.Iic ↑r = ∅

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).

Equations

• MeasureTheory.Measure.IicSnd ρ r = MeasureTheory.Measure.fst (MeasureTheory.Measure.restrict ρ (Set.univ ×ˢ Set.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 (preCDF q a), instead of the weaker ∀ q, ∀ᵐ a ∂ρ.fst, P (preCDF q a).

Equations

• ProbabilityTheory.preCDF ρ r = MeasureTheory.Measure.rnDeriv (MeasureTheory.Measure.IicSnd ρ ↑r) (MeasureTheory.Measure.fst ρ)

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

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).

• 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

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.

Equations

• ProbabilityTheory.condCDFSet ρ = (MeasureTheory.toMeasurable (MeasureTheory.Measure.fst ρ) {b : α | ¬ProbabilityTheory.HasCondCDF ρ b})ᶜ

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.

Equations

• ProbabilityTheory.condCDFRat ρ a = if a ∈ ProbabilityTheory.condCDFSet ρ then fun (r : ℚ) => (ProbabilityTheory.preCDF ρ r a).toReal else fun (r : ℚ) => if r < 0 then 0 else 1

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 = (ProbabilityTheory.preCDF ρ r a).toReal

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 : α) => (ProbabilityTheory.preCDF ρ r a).toReal

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.

Equations

• @ProbabilityTheory.condCDF' = ProbabilityTheory.wrapped✝.1

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 : { r' : ℚ // x < ↑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.

Equations

• ProbabilityTheory.condCDF ρ a = { toFun := ProbabilityTheory.condCDF' ρ a, mono' := ⋯, right_continuous' := ⋯ }

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 : α) => (ProbabilityTheory.preCDF ρ r a).toReal

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) (MeasureTheory.Measure.fst ρ)

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 ρ = (↑↑ρ (s ×ˢ Set.Iic x)).toReal

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

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))

Equations

• ⋯ = ⋯

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.