← Mathematical handbook

noncomputable def Verification.bb5 (θ δ : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) : ProbabilityTheory.Copula 2

Equations

• Verification.bb5 θ δ hθ hδ = Verification.extremeValuePower (Verification.galambos δ hδ) ⋯ θ hθ

theorem Papers.AnsariRockel2024.bb5_cdf_interior (θ δ : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) (u v : ↑unitInterval) (hu : ↑u ∈ Set.Ioo 0 1) (hv : ↑v ∈ Set.Ioo 0 1) : (Verification.bb5 θ δ hθ hδ).cdf ![u, v] = Real.exp (-Verification.bb5TailKernel θ δ (-Real.log ↑u) (-Real.log ↑v))

theorem Papers.AnsariRockel2024.bb5_cdf_full (θ δ : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) (u v : ↑unitInterval) : (Verification.bb5 θ δ hθ hδ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else if u = 1 then ↑v else if v = 1 then ↑u else Real.exp (-((-Real.log ↑u) ^ θ + (-Real.log ↑v) ^ θ - ((-Real.log ↑u) ^ (-δ * θ) + (-Real.log ↑v) ^ (-δ * θ)) ^ (-1 / δ)) ^ (1 / θ))