← Mathematical handbook

Gumbel–Hougaard conditional law and reduction of the Table 6 tau integral

theorem Papers.AnsariRockel2024.gumbel_conditionalCDF {θ : ℝ} (hθ : 1 ≤ θ) (v : ↑unitInterval) (hv : ↑v ∈ Set.Ioo 0 1) : (fun (u : ↑unitInterval) => (ProbabilityTheory.Copula.gumbel θ hθ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.gumbelPartial θ ↑u ↑v

theorem Papers.AnsariRockel2024.gumbel_kendallTau_generator_integral {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).kendallTau = 1 - 4 * ∫ (x : ℝ) (y : ℝ) in Set.Ioi 0, Verification.gumbelPsiDeriv θ⁻¹ (x + y) ^ 2

theorem Papers.AnsariRockel2024.gumbel_kendallTau {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).kendallTau = (θ - 1) / θ

theorem Papers.AnsariRockel2024.gumbel_spearmanRho_ratio_integral {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).spearmanRho = (12 * ∫ (s : ℝ) in Set.Ioi 0, (1 / (1 + s + (1 + s ^ θ) ^ θ⁻¹)) ^ 2) - 3

theorem Papers.AnsariRockel2024.gumbel_spearmanRho {θ : ℝ} (hθ : 1 ≤ θ) : (ProbabilityTheory.Copula.gumbel θ hθ).spearmanRho = (12 / θ * ∫ (t : ℝ) in 0..1, (t * (1 - t)) ^ (1 / θ - 1) / (1 + t ^ (1 / θ) + (1 - t) ^ (1 / θ)) ^ 2) - 3