← Mathematical handbook

theorem Papers.AnsariRockel2024.galambos_cdf_full (δ : ℝ) (hδ : 0 < δ) (u : Fin 2 → ↑unitInterval) : (Verification.galambos δ hδ).cdf u = if u 0 = 0 ∨ u 1 = 0 then 0 else if u 0 = 1 then ↑(u 1) else if u 1 = 1 then ↑(u 0) else ↑(u 0) * ↑(u 1) * Real.exp (((-Real.log ↑(u 0)) ^ (-δ) + (-Real.log ↑(u 1)) ^ (-δ)) ^ (-1 / δ))

theorem Papers.AnsariRockel2024.galambos_cdf_interior (δ : ℝ) (hδ : 0 < δ) (u v : ↑unitInterval) (hu : ↑u ∈ Set.Ioo 0 1) (hv : ↑v ∈ Set.Ioo 0 1) : (Verification.galambos δ hδ).cdf ![u, v] = ↑u * ↑v * Real.exp (((-Real.log ↑u) ^ (-δ) + (-Real.log ↑v) ^ (-δ)) ^ (-1 / δ))

theorem Papers.AnsariRockel2024.galambos_survivalClayton_maxima_limit (δ : ℝ) (hδ : 0 < δ) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (n : ℕ) => (Verification.normalizedMaxima (ProbabilityTheory.Copula.clayton 2 δ hδ).survivalCopula n).cdf u) Filter.atTop (nhds ((Verification.galambos δ hδ).cdf u))