Conditional cumulative distribution function

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

condCDF is build from the more general tools about kernel CDFs developed in the file Probability.Kernel.Disintegration.CDFToKernel. In that file, we build a function α × β → StieltjesFunction (which is α × β → ℝ → ℝ with additional properties) from a function α × β → ℚ → ℝ. The restriction to ℚ allows to prove some properties like measurability more easily. Here we apply that construction to the case β = Unit and then drop β to build condCDF : α → StieltjesFunction.

Main definitions

• ProbabilityTheory.condCDF ρ : α → StieltjesFunction: the conditional cdf of ρ : Measure (α × ℝ). A StieltjesFunction is a function ℝ → ℝ which is monotone and right-continuous.

Main statements

• ProbabilityTheory.setLIntegral_condCDF: for all a : α and x : ℝ, all measurable set s, ∫⁻ a in s, ENNReal.ofReal (condCDF ρ a x) ∂ρ.fst = ρ (s ×ˢ Iic x).

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

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

Equations

• ρ.IicSnd r = (ρ.restrict (Set.univ ×ˢ Set.Iic r)).fst

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

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

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

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

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

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

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

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

theorem MeasureTheory.Measure.tendsto_IicSnd_atBot {α : Type u_1} {mα : MeasurableSpace α} (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] {s : Set α} (hs : MeasurableSet s) : Filter.Tendsto (fun (r : ℚ) => (ρ.IicSnd ↑r) s) Filter.atBot (nhds 0)

Auxiliary definitions

We build towards the definition of ProbabilityTheory.condCDF. We first define ProbabilityTheory.preCDF, a function defined on α × ℚ with the properties of a cdf almost everywhere.

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

preCDF 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 = (ρ.IicSnd ↑r).rnDeriv ρ.fst

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

theorem ProbabilityTheory.measurable_preCDF' {α : Type u_1} {mα : MeasurableSpace α} {ρ : MeasureTheory.Measure (α × ℝ)} : Measurable fun (a : α) (r : ℚ) => (preCDF ρ r a).toReal

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

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

theorem ProbabilityTheory.lintegral_preCDF_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) [MeasureTheory.IsFiniteMeasure ρ] : ∫⁻ (x : α), preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) Set.univ

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

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

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

theorem ProbabilityTheory.integral_preCDF_fst {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℚ) [MeasureTheory.IsFiniteMeasure ρ] : ∫ (x : α), (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd ↑r).real Set.univ

theorem ProbabilityTheory.integrable_preCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (x : ℚ) : MeasureTheory.Integrable (fun (a : α) => (preCDF ρ x a).toReal) ρ.fst

theorem ProbabilityTheory.isRatCondKernelCDFAux_preCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : IsRatCondKernelCDFAux (fun (p : Unit × α) (r : ℚ) => (preCDF ρ r p.2).toReal) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

theorem ProbabilityTheory.isRatCondKernelCDF_preCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : IsRatCondKernelCDF (fun (p : Unit × α) (r : ℚ) => (preCDF ρ r p.2).toReal) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

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

theorem ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) : condCDF ρ a = stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) => (preCDF ρ r p.2).toReal) ⋯ ((), a)

theorem ProbabilityTheory.isCondKernelCDF_condCDF {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] : IsCondKernelCDF (fun (p : Unit × α) => condCDF ρ p.2) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

theorem ProbabilityTheory.condCDF_nonneg {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α) (r : ℝ) : 0 ≤ ↑(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 : ℝ) : ↑(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 (↑(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 (↑(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 : α) => ↑(condCDF ρ a) ↑r) =ᵐ[ρ.fst] fun (a : α) => (preCDF ρ r a).toReal

theorem ProbabilityTheory.ofReal_condCDF_ae_eq {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ] (r : ℚ) : (fun (a : α) => ENNReal.ofReal (↑(condCDF ρ a) ↑r)) =ᵐ[ρ.fst] preCDF ρ r

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

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

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

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

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

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

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

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

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

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

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

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

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

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