← Mathematical handbook

Conditional CDFs with exact endpoints at every predictor

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

Removing the null response endpoint makes rescaling identities pointwise.

Equations

• Verification.normalizedCDF C u v = if v = 0 then 0 else C.conditionalCDF u v

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

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

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

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

theorem Verification.normalizedCDF_mono (C : ProbabilityTheory.Copula 2) (u : ↑unitInterval) : Monotone (normalizedCDF C u)

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

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

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

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

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

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