← Mathematical handbook

Table 3: Clayton parameter orders on the full signed range

Verification.claytonSigned θ is the positive Clayton copula for θ>0, independence at θ=0 and the truncated negative branch for -1≤θ<0.

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

theorem Papers.AnsariRockel2024.clayton_signed_zero : Verification.claytonSigned 0 = ProbabilityTheory.Copula.independence 2

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

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

Table 3: lower-orthant order increases with θ on all of [-1,∞).

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

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

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

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

theorem Papers.AnsariRockel2024.clayton_negative_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 independence, pointwise on the square.