← Mathematical handbook

The exact density-TP2 domain of Marshall–Olkin copulas

theorem Verification.unitPower_powerSample (a : ↑unitInterval) (ha : 0 < a) (u : ↑unitInterval) : ProbabilityTheory.Copula.unitPower (ProbabilityTheory.Copula.powerSample a u) ↑a ⋯ = u

noncomputable def Verification.shockCurve (α β : ↑unitInterval) : Set (Fin 2 → ↑unitInterval)

Equations

• Verification.shockCurve α β = {x : Fin 2 → ↑unitInterval | ProbabilityTheory.Copula.unitPower (x 0) ↑α ⋯ = ProbabilityTheory.Copula.unitPower (x 1) ↑β ⋯}

theorem Verification.shockCurve_measurable (α β : ↑unitInterval) : MeasurableSet (shockCurve α β)

theorem Verification.shockCurve_volume_zero (α β : ↑unitInterval) (hβ : 0 < β) : MeasureTheory.volume (shockCurve α β) = 0

theorem Verification.marshallOlkin_shockCurve_ne_zero (α β : ↑unitInterval) (hα : 0 < α) (hβ : 0 < β) : (ProbabilityTheory.Copula.marshallOlkin α β).toMeasure (shockCurve α β) ≠ 0

The common shock charges a Lebesgue-null power curve whenever both weights are positive.

theorem Verification.marshallOlkin_zero_left (β : ↑unitInterval) : ProbabilityTheory.Copula.marshallOlkin 0 β = ProbabilityTheory.Copula.independence 2

theorem Verification.marshallOlkin_zero_right (α : ↑unitInterval) : ProbabilityTheory.Copula.marshallOlkin α 0 = ProbabilityTheory.Copula.independence 2

theorem Verification.marshallOlkin_absolutelyContinuous_iff (α β : ↑unitInterval) : (ProbabilityTheory.Copula.marshallOlkin α β).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ α = 0 ∨ β = 0

theorem Verification.marshallOlkin_density_tp2_iff (α β : ↑unitInterval) : (ProbabilityTheory.Copula.marshallOlkin α β).HasMTP2Density ↔ α = 0 ∨ β = 0