← Mathematical handbook

An explicit conditional CDF for Cuadras–Augé

noncomputable def Verification.cuadrasConditional (δ u v : ↑unitInterval) : ℝ

Equations

• Verification.cuadrasConditional δ u v = if u < v then ↑v ^ (1 - ↑δ) else (1 - ↑δ) * ↑u ^ (-↑δ) * ↑v

theorem Verification.conditionalCDF_cuadrasAuge (δ v : ↑unitInterval) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.cuadrasAuge δ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => cuadrasConditional δ u v

theorem Verification.cuadrasConditional_measurable (δ : ↑unitInterval) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => cuadrasConditional δ p.1 p.2

theorem Verification.cuadrasConditional_sq_joint_integrable (δ : ↑unitInterval) : MeasureTheory.Integrable (fun (p : ↑unitInterval × ↑unitInterval) => cuadrasConditional δ p.2 p.1 ^ 2) MeasureTheory.volume