Documentation

Papers.AnsariRockel2024.GumbelJoeConditional

← Mathematical handbook

Table 3: Gumbel–Hougaard and Joe conditional increase and parameter orders #

theorem Papers.AnsariRockel2024.gumbel_ci (θ : ℝ) (hθ : 1 ≤ θ) :

(ProbabilityTheory.Copula.gumbel θ hθ).IsCI

theorem Papers.AnsariRockel2024.gumbel_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) :

(ProbabilityTheory.Copula.gumbel θ hθ).SchurBothLE (ProbabilityTheory.Copula.gumbel η hη)

theorem Papers.AnsariRockel2024.joe_ci (θ : ℝ) (hθ : 1 ≤ θ) :

(ProbabilityTheory.Copula.joe θ hθ).IsCI

theorem Papers.AnsariRockel2024.joe_lowerOrthant_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) :

(ProbabilityTheory.Copula.joe θ hθ).LowerOrthantLE (ProbabilityTheory.Copula.joe η hη)

theorem Papers.AnsariRockel2024.joe_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) :

(ProbabilityTheory.Copula.joe θ hθ).SchurBothLE (ProbabilityTheory.Copula.joe η hη)

theorem Papers.AnsariRockel2024.joe_toMeasure_density {θ : ℝ} (hθ : 1 ≤ θ) :

(ProbabilityTheory.Copula.joe θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.joeDensity θ x)

theorem Papers.AnsariRockel2024.joe_density_tp2 {θ : ℝ} (hθ : 1 ≤ θ) :

(ProbabilityTheory.Copula.joe θ hθ).HasMTP2Density

theorem Papers.AnsariRockel2024.gumbel_toMeasure_density {θ : ℝ} (hθ : 1 ≤ θ) :

(ProbabilityTheory.Copula.gumbel θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.gumbelDensity θ x)

theorem Papers.AnsariRockel2024.gumbel_density_tp2 {θ : ℝ} (hθ : 1 ≤ θ) :

(ProbabilityTheory.Copula.gumbel θ hθ).HasMTP2Density