← Mathematical handbook

Conditional increase and order of Marshall–Olkin copulas

theorem Verification.isSI_of_concave_formula (C : ProbabilityTheory.Copula 2) (f : ↑unitInterval → ℝ → ℝ) (hf : ∀ (v : ↑unitInterval), ConcaveOn ℝ (Set.Icc 0 1) (f v)) (he : ∀ (u v : ↑unitInterval), C.cdf ![u, v] = f v ↑u) : C.IsSI

theorem Verification.marshallOlkin_cdf_min (α β u v : ↑unitInterval) : (ProbabilityTheory.Copula.marshallOlkin α β).cdf ![u, v] = min (↑u ^ (1 - ↑α) * ↑v) (↑u * ↑v ^ (1 - ↑β))

The paper's minimum formula, including all boundary and parameter endpoints.

theorem Verification.marshallOlkin_transpose (α β : ↑unitInterval) : (ProbabilityTheory.Copula.marshallOlkin α β).transpose = ProbabilityTheory.Copula.marshallOlkin β α

theorem Verification.marshallOlkin_isSI (α β : ↑unitInterval) : (ProbabilityTheory.Copula.marshallOlkin α β).IsSI

theorem Verification.marshallOlkin_isCI (α β : ↑unitInterval) : (ProbabilityTheory.Copula.marshallOlkin α β).IsCI

theorem Verification.marshallOlkin_lowerOrthant_mono {α β α' β' : ↑unitInterval} (ha : α ≤ α') (hb : β ≤ β') : (ProbabilityTheory.Copula.marshallOlkin α β).LowerOrthantLE (ProbabilityTheory.Copula.marshallOlkin α' β')

theorem Verification.marshallOlkin_schurBoth_mono {α β α' β' : ↑unitInterval} (ha : α ≤ α') (hb : β ≤ β') : (ProbabilityTheory.Copula.marshallOlkin α β).SchurBothLE (ProbabilityTheory.Copula.marshallOlkin α' β')