← Mathematical handbook

Lower-orthant and Schur parameter order of the signed Clayton family

The signed family is the positive Clayton copula for θ>0, independence at θ=0, and the truncated negative branch for -1≤θ<0. Within the positive branch the comparison reduces to superadditivity of x ↦ (1+x)^r-1 (r≥1), within the negative branch to the concave four-point inequality for x ↦ x^r (r≤1), and across zero to PQD/NQD. CI and CD transfer the orthant order to the Schur order.

noncomputable def Verification.claytonSigned (θ : ℝ) : ProbabilityTheory.Copula 2

The signed Clayton family (junk value Π below -1).

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.claytonSigned_pos {θ : ℝ} (h : 0 < θ) : claytonSigned θ = ProbabilityTheory.Copula.clayton 2 θ h

theorem Verification.claytonSigned_zero : claytonSigned 0 = ProbabilityTheory.Copula.independence 2

theorem Verification.claytonSigned_neg {θ : ℝ} (hθ : -1 ≤ θ) (hn : θ < 0) : claytonSigned θ = ProbabilityTheory.Copula.claytonNegative θ hθ hn

theorem Verification.convex_four_point {f : ℝ → ℝ} {s : Set ℝ} (hf : ConvexOn ℝ s f) {a b c d : ℝ} (ha : a ∈ s) (hd : d ∈ s) (hab : a ≤ b) (hbd : b ≤ d) (hs : a + d = b + c) : f b + f c ≤ f a + f d

Convex four-point inequality: f b + f c ≤ f a + f d for a ≤ b,c ≤ d, a+d=b+c.

theorem Verification.rpow_add_sub_one_le {r A B : ℝ} (hr : 1 ≤ r) (hA : 1 ≤ A) (hB : 1 ≤ B) : A ^ r + B ^ r ≤ (A + B - 1) ^ r + 1

For r≥1 and A,B≥1: A^r+B^r ≤ (A+B-1)^r+1.

theorem Verification.rpow_concave_four {r x y : ℝ} (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (_hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hy1 : y ≤ 1) (hs : 1 ≤ x + y) : (x + y - 1) ^ r + 1 ≤ x ^ r + y ^ r

For 0<r≤1, x,y∈[0,1], x+y≥1: (x+y-1)^r+1 ≤ x^r+y^r.

theorem Verification.clayton_cdf_mono {θ η : ℝ} (hθ : 0 < θ) (hθη : θ ≤ η) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.clayton 2 θ hθ).cdf ![u, v] ≤ (ProbabilityTheory.Copula.clayton 2 η ⋯).cdf ![u, v]

Positive branch: the Clayton CDF increases with the parameter.

theorem Verification.claytonNegative_cdf_mono {θ η : ℝ} (hθ : -1 ≤ θ) (hθη : θ ≤ η) (hη : η < 0) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.claytonNegative θ hθ ⋯).cdf ![u, v] ≤ (ProbabilityTheory.Copula.claytonNegative η ⋯ hη).cdf ![u, v]

Negative branch: the truncated Clayton CDF increases with the parameter.

theorem Verification.claytonSigned_isCI {θ : ℝ} (hθ : 0 ≤ θ) : (claytonSigned θ).IsCI

theorem Verification.claytonSigned_isCD {θ : ℝ} (hθ : -1 ≤ θ) (h0 : θ ≤ 0) : (claytonSigned θ).IsCD

theorem Verification.claytonSigned_lowerOrthant_mono {θ η : ℝ} (hθ : -1 ≤ θ) (hθη : θ ≤ η) : (claytonSigned θ).LowerOrthantLE (claytonSigned η)

Table 3: the signed Clayton family increases in lower-orthant order on [-1,∞).

theorem Verification.lowerOrthantLE_transpose {C D : ProbabilityTheory.Copula 2} (h : C.LowerOrthantLE D) : C.transpose.LowerOrthantLE D.transpose

theorem Verification.claytonSigned_schur_nonnegative {θ η : ℝ} (hθ : 0 ≤ θ) (hθη : θ ≤ η) : (claytonSigned θ).SchurBothLE (claytonSigned η)

Table 3: Schur order increases with θ on θ≥0.

theorem Verification.claytonSigned_schur_nonpositive {θ η : ℝ} (hθ : -1 ≤ θ) (hθη : θ ≤ η) (hη : η ≤ 0) : (claytonSigned η).SchurBothLE (claytonSigned θ)

Table 3: Schur order decreases with θ on -1≤θ≤0.

theorem Verification.claytonNegative_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), -1 ≤ θ a) (hn : ∀ (a : α), θ a < 0) (hlim : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (ProbabilityTheory.Copula.claytonNegative (θ a) ⋯ ⋯).cdf ![u, v]) l (nhds (↑u * ↑v))

Table 2: negative parameters tending to zero give the independence CDF.