← Mathematical handbook

Clayton family: full bivariate CDF branches and limiting cases

theorem Papers.AnsariRockel2024.clayton_positive_cdf (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : (ProbabilityTheory.Copula.clayton 2 θ hθ).cdf ![u, v] = (↑u ^ (-θ) + ↑v ^ (-θ) - 1) ^ (-1 / θ)

Tables 1–2: the Clayton CDF for positive parameters at positive coordinates.

theorem Papers.AnsariRockel2024.clayton_negative_cdf (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (ProbabilityTheory.Copula.claytonNegative θ hθ hn).cdf ![u, v] = max 0 (↑u ^ (-θ) + ↑v ^ (-θ) - 1) ^ (-θ)⁻¹

Tables 1–2: the negative Clayton branch, with truncation before the power.

theorem Papers.AnsariRockel2024.clayton_positive_zero_axes (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.clayton 2 θ hθ).cdf ![0, v] = 0 ∧ (ProbabilityTheory.Copula.clayton 2 θ hθ).cdf ![u, 0] = 0

Table 1: the positive Clayton CDF vanishes on the coordinate axes.

theorem Papers.AnsariRockel2024.clayton_negative_zero_axes (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) (u v : ↑unitInterval) : (ProbabilityTheory.Copula.claytonNegative θ hθ hn).cdf ![0, v] = 0 ∧ (ProbabilityTheory.Copula.claytonNegative θ hθ hn).cdf ![u, 0] = 0

Table 1: the negative Clayton CDF also vanishes on the coordinate axes.

theorem Papers.AnsariRockel2024.clayton_one_cdf (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : (ProbabilityTheory.Copula.clayton 2 1 ⋯).cdf ![u, v] = ↑u * ↑v / (↑u + ↑v - ↑u * ↑v)

Table 2: the positive-parameter θ = 1 special case on the open square.

theorem Papers.AnsariRockel2024.clayton_negative_one : ProbabilityTheory.Copula.claytonNegative (-1) ⋯ ⋯ = ProbabilityTheory.Copula.countermonotonic

Table 2: the θ = −1 copula is the lower Fréchet bound.

theorem Papers.AnsariRockel2024.clayton_positive_ci (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).IsCI

Table 3: every positive Clayton copula is conditionally increasing in both directions.

theorem Papers.AnsariRockel2024.clayton_positive_not_cd (θ : ℝ) (hθ : 0 < θ) : ¬(ProbabilityTheory.Copula.clayton 2 θ hθ).IsCD

Table 3: no positive Clayton parameter is conditionally decreasing.

theorem Papers.AnsariRockel2024.clayton_positive_pqd (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).IsPQD

Table 3: the quadrant-dependence consequence of the positive Clayton CI entry.

theorem Papers.AnsariRockel2024.clayton_zero_ci_cd : (ProbabilityTheory.Copula.independence 2).IsCI ∧ (ProbabilityTheory.Copula.independence 2).IsCD

Table 3: the zero-parameter limit is independence, hence both CI and CD.

theorem Papers.AnsariRockel2024.clayton_negative_one_cd : (ProbabilityTheory.Copula.claytonNegative (-1) ⋯ ⋯).IsCD

Table 3: the negative endpoint is the countermonotonic copula, hence CD.

theorem Papers.AnsariRockel2024.clayton_negative_cd (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : (ProbabilityTheory.Copula.claytonNegative θ hθ hn).IsCD

Table 3: every admissible negative Clayton copula is conditionally decreasing in both directions.

theorem Papers.AnsariRockel2024.clayton_negative_not_ci (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : ¬(ProbabilityTheory.Copula.claytonNegative θ hθ hn).IsCI

Table 3: no admissible negative Clayton parameter is conditionally increasing.

theorem Papers.AnsariRockel2024.clayton_negative_nqd (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : (ProbabilityTheory.Copula.claytonNegative θ hθ hn).IsNQD

Table 3: negative Clayton parameters are negatively quadrant dependent.

theorem Papers.AnsariRockel2024.clayton_positive_cdf_tp2 (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).IsTP2CDF

Additional CDF-level result: every positive Clayton CDF is TP2. This is not density TP2.

theorem Papers.AnsariRockel2024.clayton_zero_cdf_tp2 : (ProbabilityTheory.Copula.independence 2).IsTP2CDF

At the zero parameter, independence has a TP2 CDF.

theorem Papers.AnsariRockel2024.clayton_negative_not_cdf_tp2 (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : ¬(ProbabilityTheory.Copula.claytonNegative θ hθ hn).IsTP2CDF

Additional CDF-level result: every admissible negative Clayton CDF fails TP2.

theorem Papers.AnsariRockel2024.clayton_negative_one_not_density_tp2 : ¬(ProbabilityTheory.Copula.claytonNegative (-1) ⋯ ⋯).HasMTP2Density

Table 3: at θ = −1, Clayton is W and has no Lebesgue MTP2 density.

theorem Papers.AnsariRockel2024.clayton_positive_lower_tail (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).HasLowerTailDependence (2 ^ (-1 / θ))

Table 3: positive Clayton has exact lower-tail coefficient 2 ^ (-1 / θ).

theorem Papers.AnsariRockel2024.clayton_positive_upper_tail (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).HasUpperTailDependence 0

Table 3: positive Clayton has zero upper-tail coefficient.

theorem Papers.AnsariRockel2024.clayton_negative_lower_tail (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : (ProbabilityTheory.Copula.claytonNegative θ hθ hn).HasLowerTailDependence 0

Table 3: negative Clayton has zero lower-tail coefficient.

theorem Papers.AnsariRockel2024.clayton_negative_upper_tail (θ : ℝ) (hθ : -1 ≤ θ) (hn : θ < 0) : (ProbabilityTheory.Copula.claytonNegative θ hθ hn).HasUpperTailDependence 0

Table 3: negative Clayton has zero upper-tail coefficient.

theorem Papers.AnsariRockel2024.clayton_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l (nhds 0)) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (ProbabilityTheory.Copula.clayton 2 (θ a) ⋯).cdf u) l (nhds ((ProbabilityTheory.Copula.independence 2).cdf u))

Table 2: positive Clayton parameters tending to zero give independence.

theorem Papers.AnsariRockel2024.clayton_tendsto_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (hlim : Filter.Tendsto θ l Filter.atTop) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (ProbabilityTheory.Copula.clayton 2 (θ a) ⋯).cdf u) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))

Table 2: positive Clayton parameters tending to infinity give the upper bound.