← Copula mathematical handbook

Conditional CDF of the two-parameter Marshall–Olkin family

noncomputable def ProbabilityTheory.Copula.marshallOlkinConditional (α β u v : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.marshallOlkinConditional α β u v = if ↑u ^ ↑α < ↑v ^ ↑β then ↑v ^ (1 - ↑β) else (1 - ↑α) * ↑u ^ (-↑α) * ↑v

theorem ProbabilityTheory.Copula.conditionalCDF_marshallOlkin (α β v : ↑unitInterval) (ha : 0 < ↑α) : (fun (u : ↑unitInterval) => (marshallOlkin α β).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => marshallOlkinConditional α β u v

theorem ProbabilityTheory.Copula.marshallOlkinConditional_measurable (α β : ↑unitInterval) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => marshallOlkinConditional α β p.1 p.2

theorem ProbabilityTheory.Copula.marshallOlkinConditional_sq_joint_integrable (α β : ↑unitInterval) (ha : 0 < ↑α) : MeasureTheory.Integrable (fun (p : ↑unitInterval × ↑unitInterval) => marshallOlkinConditional α β p.2 p.1 ^ 2) MeasureTheory.volume