← Mathematical handbook

Compatibility names for the dependence results now proved in the pinned copula library.

theorem Verification.frechet_exchangeable (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).IsExchangeable

theorem Verification.frechet_si_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).IsSI ↔ b = 0

theorem Verification.frechet_sd_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).IsSD ↔ a = 0

theorem Verification.frechet_ci_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).IsCI ↔ b = 0

theorem Verification.frechet_cd_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).IsCD ↔ a = 0

theorem Verification.frechet_measure (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).toMeasure = ENNReal.ofReal a • (ProbabilityTheory.Copula.comonotonic 2).toMeasure + ENNReal.ofReal b • ProbabilityTheory.Copula.countermonotonic.toMeasure + ENNReal.ofReal (1 - a - b) • (ProbabilityTheory.Copula.independence 2).toMeasure

theorem Verification.frechet_absolutelyContinuous_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).toMeasure.AbsolutelyContinuous MeasureTheory.volume ↔ a = 0 ∧ b = 0

theorem Verification.frechet_density_tp2_iff (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b ≤ 1) : (ProbabilityTheory.Copula.frechet a b ha hb hab).HasMTP2Density ↔ a = 0 ∧ b = 0