← Mathematical handbook

Conditional distributions of the second coordinate given the first

noncomputable def ProbabilityTheory.Copula.conditionalKernel (C : Copula 2) : Kernel ↑unitInterval ↑unitInterval

A regular conditional distribution of coordinate 1 given coordinate 0. Its values on a null set of conditioning points are immaterial.

Equations

• C.conditionalKernel = ProbabilityTheory.condDistrib (fun (x : Fin 2 → ↑unitInterval) => x 1) (fun (x : Fin 2 → ↑unitInterval) => x 0) C.toMeasure

instance ProbabilityTheory.Copula.instIsMarkovKernelElemRealUnitIntervalConditionalKernel (C : Copula 2) : IsMarkovKernel C.conditionalKernel

noncomputable def ProbabilityTheory.Copula.conditionalCDF (C : Copula 2) (u t : ↑unitInterval) : ℝ

The conditional CDF P(V ≤ t | U = u), for a fixed version of the kernel.

Equations

• C.conditionalCDF u t = (C.conditionalKernel u).real (Set.Iic t)

theorem ProbabilityTheory.Copula.conditionalCDF_nonneg (C : Copula 2) (u t : ↑unitInterval) : 0 ≤ C.conditionalCDF u t

theorem ProbabilityTheory.Copula.conditionalCDF_le_one (C : Copula 2) (u t : ↑unitInterval) : C.conditionalCDF u t ≤ 1

theorem ProbabilityTheory.Copula.measurable_conditionalCDF (C : Copula 2) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => C.conditionalCDF p.2 p.1

theorem ProbabilityTheory.Copula.measurable_conditionalCDF_left (C : Copula 2) (t : ↑unitInterval) : Measurable fun (u : ↑unitInterval) => C.conditionalCDF u t

theorem ProbabilityTheory.Copula.integrable_conditionalCDF (C : Copula 2) (t : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => C.conditionalCDF u t) MeasureTheory.volume

theorem ProbabilityTheory.Copula.conditionalKernel_comp_volume (C : Copula 2) : MeasureTheory.volume.bind ⇑C.conditionalKernel = MeasureTheory.volume

theorem ProbabilityTheory.Copula.integral_conditionalCDF (C : Copula 2) (t : ↑unitInterval) : ∫ (u : ↑unitInterval), C.conditionalCDF u t = ↑t

Averaging a conditional CDF recovers the uniform second marginal.

theorem ProbabilityTheory.Copula.integrable_conditionalCDF_sq (C : Copula 2) (t : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => C.conditionalCDF u t ^ 2) MeasureTheory.volume

theorem ProbabilityTheory.Copula.integral_conditionalCDF_sq_le (C : Copula 2) (t : ↑unitInterval) : ∫ (u : ↑unitInterval), C.conditionalCDF u t ^ 2 ≤ ↑t