← Mathematical handbook

Conditional CDF of the two-parameter Marshall–Olkin family

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

Equations

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

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

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

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