← Mathematical handbook

theorem Verification.galambosTailKernel_pos (δ x y : ℝ) (hx : 0 < x) (hy : 0 < y) : 0 < galambosTailKernel δ x y

theorem Verification.galambosTailKernel_le_min (δ : ℝ) (hδ : 0 < δ) (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : galambosTailKernel δ x y ≤ min x y

noncomputable def Verification.bb5TailKernel (θ δ x y : ℝ) : ℝ

The BB5 logarithmic exponent on strictly positive coordinates. The copula construction and the boundary extension are separate obligations.

Equations

• Verification.bb5TailKernel θ δ x y = (x ^ θ + y ^ θ - Verification.galambosTailKernel δ (x ^ θ) (y ^ θ)) ^ (1 / θ)

theorem Verification.bb5TailKernel_inner_pos (θ δ x y : ℝ) (hδ : 0 < δ) (hx : 0 < x) (hy : 0 < y) : 0 < x ^ θ + y ^ θ - galambosTailKernel δ (x ^ θ) (y ^ θ)

theorem Verification.bb5TailKernel_bounds (θ δ x y : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) (hx : 0 < x) (hy : 0 < y) : max x y ≤ bb5TailKernel θ δ x y ∧ bb5TailKernel θ δ x y ≤ x + y

theorem Verification.bb5TailKernel_shape_one (δ x y : ℝ) : bb5TailKernel 1 δ x y = x + y - galambosTailKernel δ x y

theorem Verification.galambosTailKernel_homogeneous (δ : ℝ) (hδ : 0 < δ) (c x y : ℝ) (hc : 0 < c) (hx : 0 ≤ x) (hy : 0 ≤ y) : galambosTailKernel δ (c * x) (c * y) = c * galambosTailKernel δ x y

theorem Verification.bb5TailKernel_homogeneous (θ δ c x y : ℝ) (hθ : 1 ≤ θ) (hδ : 0 < δ) (hc : 0 < c) (hx : 0 < x) (hy : 0 < y) : bb5TailKernel θ δ (c * x) (c * y) = c * bb5TailKernel θ δ x y

theorem Verification.bb5TailKernel_formula (θ δ x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : bb5TailKernel θ δ x y = (x ^ θ + y ^ θ - (x ^ (-δ * θ) + y ^ (-δ * θ)) ^ (-1 / δ)) ^ (1 / θ)