← Copula mathematical handbook

Conditional CDFs with exact endpoints at every predictor

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF (C : Copula 2) (u v : ↑unitInterval) : ℝ

Removing the null response endpoint makes rescaling identities pointwise.

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF C u v = if v = 0 then 0 else C.conditionalCDF u v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_measurable (C : Copula 2) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => normalizedCDF C p.2 p.1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_mem (C : Copula 2) (u v : ↑unitInterval) : normalizedCDF C u v ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_zero (C : Copula 2) (u : ↑unitInterval) : normalizedCDF C u 0 = 0

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_one (C : Copula 2) (u : ↑unitInterval) : normalizedCDF C u 1 = 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_mono (C : Copula 2) (u : ↑unitInterval) : Monotone (normalizedCDF C u)

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_ae (C : Copula 2) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => normalizedCDF C u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => C.conditionalCDF u v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_response_ae (C : Copula 2) (u : ↑unitInterval) : normalizedCDF C u =ᵐ[MeasureTheory.volume] C.conditionalCDF u

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_integrable (C : Copula 2) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => normalizedCDF C u v) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_mean (C : Copula 2) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), normalizedCDF C u v = ↑v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_response_integrable (C : Copula 2) (u : ↑unitInterval) : MeasureTheory.Integrable (normalizedCDF C u) MeasureTheory.volume

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.normalizedCDF_response_integral (C : Copula 2) (u : ↑unitInterval) : ∫ (v : ↑unitInterval), normalizedCDF C u v = 1 - conditionalMean C u