← Mathematical handbook

Table 3: Frank density TP2 on the full real parameter range

noncomputable def Papers.AnsariRockel2024.frankSigned (θ : ℝ) : ProbabilityTheory.Copula 2

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.AnsariRockel2024.frank_positive_density (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.frank θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.frankDensity θ x)

theorem Papers.AnsariRockel2024.frank_positive_density_tp2 (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.frank θ hθ).HasMTP2Density

theorem Papers.AnsariRockel2024.frank_density_tp2_iff (θ : ℝ) : (frankSigned θ).HasMTP2Density ↔ 0 ≤ θ

theorem Papers.AnsariRockel2024.frank_ci_iff (θ : ℝ) : (frankSigned θ).IsCI ↔ 0 ≤ θ

theorem Papers.AnsariRockel2024.frank_cd_iff (θ : ℝ) : (frankSigned θ).IsCD ↔ θ ≤ 0