← Mathematical handbook

Table 3: conditional increase for Nelsen 12 and 14

theorem Papers.AnsariRockel2024.nelsen12_ci (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen12 θ hθ).IsCI

theorem Papers.AnsariRockel2024.nelsen14_ci (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen14 θ hθ).IsCI

theorem Papers.AnsariRockel2024.nelsen12_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.nelsen12 θ hθ).SchurBothLE (ProbabilityTheory.Copula.nelsen12 η hη)

theorem Papers.AnsariRockel2024.nelsen12_density_tp2 (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen12 θ hθ).HasMTP2Density

theorem Papers.AnsariRockel2024.nelsen14_density_tp2 (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen14 θ hθ).HasMTP2Density

theorem Papers.AnsariRockel2024.nelsen12_toMeasure_density (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen12 θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.bbDensity 1 θ x)

theorem Papers.AnsariRockel2024.nelsen14_toMeasure_density (θ : ℝ) (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.nelsen14 θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.bbDensity θ⁻¹ θ x)

theorem Papers.AnsariRockel2024.nelsen14_lowerOrthant_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.nelsen14 θ hθ).LowerOrthantLE (ProbabilityTheory.Copula.nelsen14 η hη)

theorem Papers.AnsariRockel2024.nelsen14_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (ProbabilityTheory.Copula.nelsen14 θ hθ).SchurBothLE (ProbabilityTheory.Copula.nelsen14 η hη)