← Mathematical handbook

theorem Papers.AnsariRockel2024.galambos_pickands_midpoint (δ : ℝ) (hδ : 0 < δ) : Verification.copulaPickands (Verification.galambos δ hδ) ProbabilityTheory.Copula.unitHalf = 1 - 2 ^ (-1 / δ) / 2

theorem Papers.AnsariRockel2024.galambos_pickands_midpoint_gt_half (δ : ℝ) (hδ : 0 < δ) : 1 / 2 < Verification.copulaPickands (Verification.galambos δ hδ) ProbabilityTheory.Copula.unitHalf

theorem Papers.AnsariRockel2024.galambos_printed_midpoint_counterexample : Verification.copulaPickands (Verification.galambos 1 ⋯) ProbabilityTheory.Copula.unitHalf = 3 / 4 ∧ 2 ^ ((1 - 1) / 1) = 1

theorem Papers.AnsariRockel2024.galambos_printed_midpoint_false : ¬∀ (δ : ℝ) (hδ : 0 < δ), Verification.copulaPickands (Verification.galambos δ hδ) ProbabilityTheory.Copula.unitHalf = 2 ^ ((1 - δ) / δ)