# 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.of_real (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.set_lintegral_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α : } (ρ : ) (r : ) :

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

Equations
• ρ.IicSnd r = (ρ.restrict (Set.univ ×ˢ )).fst
Instances For
theorem MeasureTheory.Measure.IicSnd_apply {α : Type u_1} {mα : } (ρ : ) (r : ) {s : Set α} (hs : ) :
(ρ.IicSnd r) s = ρ (s ×ˢ )
theorem MeasureTheory.Measure.IicSnd_univ {α : Type u_1} {mα : } (ρ : ) (r : ) :
(ρ.IicSnd r) Set.univ = ρ (Set.univ ×ˢ )
theorem MeasureTheory.Measure.IicSnd_mono {α : Type u_1} {mα : } (ρ : ) {r : } {r' : } (h_le : r r') :
ρ.IicSnd r ρ.IicSnd r'
theorem MeasureTheory.Measure.IicSnd_le_fst {α : Type u_1} {mα : } (ρ : ) (r : ) :
ρ.IicSnd r ρ.fst
theorem MeasureTheory.Measure.IicSnd_ac_fst {α : Type u_1} {mα : } (ρ : ) (r : ) :
(ρ.IicSnd r).AbsolutelyContinuous ρ.fst
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' }), (ρ.IicSnd r) s = (ρ.IicSnd t) s
theorem MeasureTheory.Measure.tendsto_IicSnd_atTop {α : Type u_1} {mα : } (ρ : ) {s : Set α} (hs : ) :
Filter.Tendsto (fun (r : ) => (ρ.IicSnd r) s) Filter.atTop (nhds (ρ.fst s))
theorem MeasureTheory.Measure.tendsto_IicSnd_atBot {α : Type u_1} {mα : } (ρ : ) {s : Set α} (hs : ) :
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α : } (ρ : ) (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
• = (ρ.IicSnd r).rnDeriv ρ.fst
Instances For
theorem ProbabilityTheory.measurable_preCDF {α : Type u_1} {mα : } {ρ : } {r : } :
theorem ProbabilityTheory.measurable_preCDF' {α : Type u_1} {mα : } {ρ : } :
Measurable fun (a : α) (r : ) => ().toReal
theorem ProbabilityTheory.withDensity_preCDF {α : Type u_1} {mα : } (ρ : ) (r : ) :
ρ.fst.withDensity () = ρ.IicSnd r
theorem ProbabilityTheory.set_lintegral_preCDF_fst {α : Type u_1} {mα : } (ρ : ) (r : ) {s : Set α} (hs : ) :
∫⁻ (x : α) in s, ρ.fst = (ρ.IicSnd r) s
theorem ProbabilityTheory.lintegral_preCDF_fst {α : Type u_1} {mα : } (ρ : ) (r : ) :
∫⁻ (x : α), ρ.fst = (ρ.IicSnd r) Set.univ
theorem ProbabilityTheory.monotone_preCDF {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂ρ.fst, Monotone fun (r : ) =>
theorem ProbabilityTheory.preCDF_le_one {α : Type u_1} {mα : } (ρ : ) :
∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ), 1
theorem ProbabilityTheory.setIntegral_preCDF_fst {α : Type u_1} {mα : } (ρ : ) (r : ) {s : Set α} (hs : ) :
∫ (x : α) in s, ().toRealρ.fst = ((ρ.IicSnd r) s).toReal
@[deprecated ProbabilityTheory.setIntegral_preCDF_fst]
theorem ProbabilityTheory.set_integral_preCDF_fst {α : Type u_1} {mα : } (ρ : ) (r : ) {s : Set α} (hs : ) :
∫ (x : α) in s, ().toRealρ.fst = ((ρ.IicSnd r) s).toReal

Alias of ProbabilityTheory.setIntegral_preCDF_fst.

theorem ProbabilityTheory.integral_preCDF_fst {α : Type u_1} {mα : } (ρ : ) (r : ) :
∫ (x : α), ().toRealρ.fst = ((ρ.IicSnd r) Set.univ).toReal
theorem ProbabilityTheory.integrable_preCDF {α : Type u_1} {mα : } (ρ : ) (x : ) :
MeasureTheory.Integrable (fun (a : α) => ().toReal) ρ.fst
theorem ProbabilityTheory.isRatCondKernelCDFAux_preCDF {α : Type u_1} {mα : } (ρ : ) :
ProbabilityTheory.IsRatCondKernelCDFAux (fun (p : ) (r : ) => ().toReal) ()
theorem ProbabilityTheory.isRatCondKernelCDF_preCDF {α : Type u_1} {mα : } (ρ : ) :
ProbabilityTheory.IsRatCondKernelCDF (fun (p : ) (r : ) => ().toReal) ()

### Conditional cdf #

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

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

Equations
Instances For
theorem ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod {α : Type u_1} {mα : } (ρ : ) (a : α) :
= ProbabilityTheory.stieltjesOfMeasurableRat (fun (p : ) (r : ) => ().toReal) ((), a)
theorem ProbabilityTheory.isCondKernelCDF_condCDF {α : Type u_1} {mα : } (ρ : ) :
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) =ᵐ[ρ.fst] fun (a : α) => ().toReal
theorem ProbabilityTheory.ofReal_condCDF_ae_eq {α : Type u_1} {mα : } (ρ : ) (r : ) :
(fun (a : α) => ENNReal.ofReal ( r)) =ᵐ[ρ.fst]
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.stronglyMeasurable_condCDF {α : Type u_1} {mα : } (ρ : ) (x : ) :
MeasureTheory.StronglyMeasurable fun (a : α) => x

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

theorem ProbabilityTheory.set_lintegral_condCDF {α : Type u_1} {mα : } (ρ : ) (x : ) {s : Set α} (hs : ) :
∫⁻ (a : α) in s, ENNReal.ofReal ( x)ρ.fst = ρ (s ×ˢ )
theorem ProbabilityTheory.lintegral_condCDF {α : Type u_1} {mα : } (ρ : ) (x : ) :
∫⁻ (a : α), ENNReal.ofReal ( x)ρ.fst = ρ (Set.univ ×ˢ )
theorem ProbabilityTheory.integrable_condCDF {α : Type u_1} {mα : } (ρ : ) (x : ) :
MeasureTheory.Integrable (fun (a : α) => x) ρ.fst
theorem ProbabilityTheory.setIntegral_condCDF {α : Type u_1} {mα : } (ρ : ) (x : ) {s : Set α} (hs : ) :
∫ (a : α) in s, xρ.fst = (ρ (s ×ˢ )).toReal
@[deprecated ProbabilityTheory.setIntegral_condCDF]
theorem ProbabilityTheory.set_integral_condCDF {α : Type u_1} {mα : } (ρ : ) (x : ) {s : Set α} (hs : ) :
∫ (a : α) in s, xρ.fst = (ρ (s ×ˢ )).toReal

Alias of ProbabilityTheory.setIntegral_condCDF.

theorem ProbabilityTheory.integral_condCDF {α : Type u_1} {mα : } (ρ : ) (x : ) :
∫ (a : α), xρ.fst = (ρ (Set.univ ×ˢ )).toReal
theorem ProbabilityTheory.measure_condCDF_Iic {α : Type u_1} {mα : } (ρ : ) (a : α) (x : ) :
.measure () = ENNReal.ofReal ( x)
theorem ProbabilityTheory.measure_condCDF_univ {α : Type u_1} {mα : } (ρ : ) (a : α) :
.measure Set.univ = 1
instance ProbabilityTheory.instIsProbabilityMeasureCondCDF {α : Type u_1} {mα : } (ρ : ) (a : α) :
Equations
• =
theorem ProbabilityTheory.measurable_measure_condCDF {α : Type u_1} {mα : } (ρ : ) :
Measurable fun (a : α) => .measure

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