← Mathematical handbook

Further FGM and Nelsen 7 table entries

Density TP2 is explicitly distinguished from TP2 of the CDF. The FGM classification below concerns its displayed continuous density, together with a genuine density witness in the nonnegative parameter range.

theorem Papers.AnsariRockel2024.fgm_density (θ : ℝ) (hθ : |θ| ≤ 1) : (ProbabilityTheory.Copula.fgm θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (1 + θ * (1 - 2 * ↑(x 0)) * (1 - 2 * ↑(x 1)))

theorem Papers.AnsariRockel2024.fgm_density_tp2_iff (θ : ℝ) : (ProbabilityTheory.IsTP2 fun (u v : ↑unitInterval) => 1 + θ * (1 - 2 * ↑u) * (1 - 2 * ↑v)) ↔ 0 ≤ θ

theorem Papers.AnsariRockel2024.fgm_has_tp2_density (θ : ℝ) (hθ : |θ| ≤ 1) (hpos : 0 ≤ θ) : (ProbabilityTheory.Copula.fgm θ hθ).HasMTP2Density

theorem Papers.AnsariRockel2024.nelsen7_cdf (θ u v : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).cdf ![u, v] = max 0 (↑θ * ↑u * ↑v + (1 - ↑θ) * (↑u + ↑v - 1))

theorem Papers.AnsariRockel2024.nelsen7_endpoints : ProbabilityTheory.Copula.nelsen7 0 = ProbabilityTheory.Copula.countermonotonic ∧ ProbabilityTheory.Copula.nelsen7 1 = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.nelsen7_cd (θ : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).IsCD

theorem Papers.AnsariRockel2024.nelsen7_lowerOrthant_iff (θ η : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).LowerOrthantLE (ProbabilityTheory.Copula.nelsen7 η) ↔ θ ≤ η

theorem Papers.AnsariRockel2024.nelsen7_tails (θ : ↑unitInterval) : (ProbabilityTheory.Copula.nelsen7 θ).HasLowerTailDependence 0 ∧ (ProbabilityTheory.Copula.nelsen7 θ).HasUpperTailDependence 0