← Mathematical handbook

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

The analytic expression below is the CDF of the actual positive-Clayton copula on strictly positive unit coordinates.

theorem Papers.AnsariRockel2024.clayton_cdf_formula_hasDerivAt_first (θ u v : ℝ) (hθ : 0 < θ) (hu : 0 < u) (hv : 0 < v) (hu1 : u ≤ 1) (hv1 : v ≤ 1) : HasDerivAt (fun (x : ℝ) => Papers.AnsariRockel2024.claytonBaseReal✝ θ x v ^ (-1 / θ)) (u ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ u v ^ (-1 / θ - 1)) u

The actual positive-Clayton CDF formula has the expected first partial derivative on the positive unit square.

theorem Papers.AnsariRockel2024.clayton_cdf_formula_hasDerivAt_second (θ u v : ℝ) (hθ : 0 < θ) (hu : 0 < u) (hv : 0 < v) (hu1 : u ≤ 1) (hv1 : v ≤ 1) : HasDerivAt (fun (y : ℝ) => u ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ u y ^ (-1 / θ - 1)) ((1 + θ) * u ^ (-θ - 1) * v ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ u v ^ (-2 - 1 / θ)) v

The mixed derivative of the positive-Clayton CDF formula is its standard density formula on the positive unit square.

theorem Papers.AnsariRockel2024.clayton_mixed_derivative_eq_densityFormula (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : deriv (fun (y : ℝ) => ↑u ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ (↑u) y ^ (-1 / θ - 1)) ↑v = ProbabilityTheory.Copula.claytonDensityFormula θ ![u, v]

The analytic mixed derivative is exactly the pinned copula package's candidate density at every strictly positive coordinate.

theorem Papers.AnsariRockel2024.clayton_density_formula_integral_second (θ u a b : ℝ) (hθ : 0 < θ) (hu : 0 < u) (hu1 : u ≤ 1) (ha : 0 < a) (hab : a ≤ b) (hb1 : b ≤ 1) : ∫ (y : ℝ) in a..b, (1 + θ) * u ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ u y ^ (-2 - 1 / θ) = u ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ u b ^ (-1 / θ - 1) - u ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ u a ^ (-1 / θ - 1)

On a positive rectangle, integrating the mixed derivative in the second coordinate recovers the first-derivative increment.

theorem Papers.AnsariRockel2024.clayton_cdf_formula_integral_first (θ v a b : ℝ) (hθ : 0 < θ) (hv : 0 < v) (hv1 : v ≤ 1) (ha : 0 < a) (hab : a ≤ b) (hb1 : b ≤ 1) : ∫ (x : ℝ) in a..b, x ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x v ^ (-1 / θ - 1) = Papers.AnsariRockel2024.claytonBaseReal✝ θ b v ^ (-1 / θ) - Papers.AnsariRockel2024.claytonBaseReal✝ θ a v ^ (-1 / θ)

Integrating the first partial derivative over a positive interval recovers the Clayton CDF formula increment.

theorem Papers.AnsariRockel2024.clayton_density_formula_positive_rectangle (θ a b c d : ℝ) (hθ : 0 < θ) (ha : 0 < a) (hab : a ≤ b) (hb1 : b ≤ 1) (hc : 0 < c) (hcd : c ≤ d) (hd1 : d ≤ 1) : ∫ (x : ℝ) in a..b, ∫ (y : ℝ) in c..d, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) = Papers.AnsariRockel2024.claytonBaseReal✝ θ b d ^ (-1 / θ) - Papers.AnsariRockel2024.claytonBaseReal✝ θ a d ^ (-1 / θ) - Papers.AnsariRockel2024.claytonBaseReal✝ θ b c ^ (-1 / θ) + Papers.AnsariRockel2024.claytonBaseReal✝ θ a c ^ (-1 / θ)

The analytic Clayton density integrates to the exact CDF rectangle increment on every rectangle bounded away from both axes.

theorem Papers.AnsariRockel2024.clayton_density_formula_positive_rectangle_eq_measure (θ : ℝ) (hθ : 0 < θ) (a b c d : ↑unitInterval) (ha : 0 < ↑a) (hab : a ≤ b) (hc : 0 < ↑c) (hcd : c ≤ d) : ∫ (x : ℝ) in ↑a..↑b, ∫ (y : ℝ) in ↑c..↑d, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) = (ProbabilityTheory.Copula.clayton 2 θ hθ).toMeasure.real (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i))

On positive rectangles, the analytic density integrates to the mass of that rectangle under the actual Clayton copula measure.

theorem Papers.AnsariRockel2024.clayton_densityFormula_positive_rectangle_eq_measure (θ : ℝ) (hθ : 0 < θ) (a b c d : ↑unitInterval) (ha : 0 < ↑a) (hab : a ≤ b) (hc : 0 < ↑c) (hcd : c ≤ d) : ∫ (x : Fin 2 → ↑unitInterval) in Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i), ProbabilityTheory.Copula.claytonDensityFormula θ x = (ProbabilityTheory.Copula.clayton 2 θ hθ).toMeasure.real (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i))

The package's Clayton density candidate has exactly the actual copula measure on every positive half-open rectangle in the unit square.

theorem Papers.AnsariRockel2024.clayton_withDensity_positive_rectangle_eq_measure (θ : ℝ) (hθ : 0 < θ) (a b c d : ↑unitInterval) (ha : 0 < ↑a) (hab : a ≤ b) (hc : 0 < ↑c) (hcd : c ≤ d) : (MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (ProbabilityTheory.Copula.claytonDensityFormula θ x)) (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i)) = (ProbabilityTheory.Copula.clayton 2 θ hθ).toMeasure (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i))

The measure built from the pinned candidate density agrees with the Clayton copula measure on each positive half-open rectangle.

theorem Papers.AnsariRockel2024.clayton_withDensity_axis_zero (θ : ℝ) (i : Fin 2) : (MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (ProbabilityTheory.Copula.claytonDensityFormula θ x)) {x : Fin 2 → ↑unitInterval | x i = 0} = 0

The candidate-density measure assigns zero mass to either coordinate axis, as does every copula measure.

theorem Papers.AnsariRockel2024.clayton_withDensity_positive_lowerOrthant_eq_measure (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) (hu : 0 < ↑u) (hv : 0 < ↑v) : (MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (ProbabilityTheory.Copula.claytonDensityFormula θ x)) (Set.univ.pi fun (i : Fin 2) => Set.Ioc 0 (![u, v] i)) = (ProbabilityTheory.Copula.clayton 2 θ hθ).toMeasure (Set.univ.pi fun (i : Fin 2) => Set.Ioc 0 (![u, v] i))

The candidate's withDensity measure agrees with the Clayton copula measure on every positive lower orthant.

theorem Papers.AnsariRockel2024.clayton_withDensity_lowerOrthant_eq_measure (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (ProbabilityTheory.Copula.claytonDensityFormula θ x)) (Set.Iic ![u, v]) = (ProbabilityTheory.Copula.clayton 2 θ hθ).toMeasure (Set.Iic ![u, v])

The candidate's withDensity measure and the actual Clayton copula measure agree on every closed lower orthant, including the axes.

theorem Papers.AnsariRockel2024.clayton_toMeasure_eq_withDensity_positive (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (ProbabilityTheory.Copula.claytonDensityFormula θ x)

The pinned positive-Clayton density candidate generates exactly the copula's probability measure on the full unit square.

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

Positive Clayton has an actual nonnegative MTP2 density, given by the pinned copula package's explicit formula.

theorem Papers.AnsariRockel2024.clayton_positive_absolutelyContinuous (θ : ℝ) (hθ : 0 < θ) : (ProbabilityTheory.Copula.clayton 2 θ hθ).toMeasure.AbsolutelyContinuous MeasureTheory.volume

Positive Clayton is absolutely continuous with respect to uniform volume on the unit square.

theorem Papers.AnsariRockel2024.clayton_density_formula_cutoff_square (θ : ℝ) (hθ : 0 < θ) (r : ↑unitInterval) (hr : 0 < ↑r) : ∫ (x : ℝ) (y : ℝ) in ↑r..1, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) = 1 - 2 * ↑r + (ProbabilityTheory.Copula.clayton 2 θ hθ).cdf ![r, r]

The candidate's mass on the positive square with lower cutoff r reaches the Clayton copula's corresponding square mass.

theorem Papers.AnsariRockel2024.clayton_density_formula_cutoff_square_bounds (θ : ℝ) (hθ : 0 < θ) (r : ↑unitInterval) (hr : 0 < ↑r) : 1 - 2 * ↑r ≤ ∫ (x : ℝ) (y : ℝ) in ↑r..1, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) ∧ ∫ (x : ℝ) (y : ℝ) in ↑r..1, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) ≤ 1 - ↑r

The positive cutoff-square mass lies between 1 - 2r and 1 - r. This quantitative estimate is a boundary-control step for the density.

theorem Papers.AnsariRockel2024.clayton_density_formula_cutoff_square_tendsto_one (θ : ℝ) (hθ : 0 < θ) (r : ℕ → ↑unitInterval) (hr : ∀ (n : ℕ), 0 < ↑(r n)) (h0 : Filter.Tendsto (fun (n : ℕ) => ↑(r n)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) (y : ℝ) in ↑(r n)..1, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ)) Filter.atTop (nhds 1)

Along any positive cutoffs tending to zero, the analytic candidate's integral over the cutoff square tends to one.

theorem Papers.AnsariRockel2024.clayton_density_formula_positive_rectangle_cdf_bounds (θ : ℝ) (hθ : 0 < θ) (a b c d : ↑unitInterval) (ha : 0 < ↑a) (hab : a ≤ b) (hc : 0 < ↑c) (hcd : c ≤ d) : (ProbabilityTheory.Copula.clayton 2 θ hθ).cdf ![b, d] - ↑a - ↑c ≤ ∫ (x : ℝ) in ↑a..↑b, ∫ (y : ℝ) in ↑c..↑d, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) ∧ ∫ (x : ℝ) in ↑a..↑b, ∫ (y : ℝ) in ↑c..↑d, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) ≤ (ProbabilityTheory.Copula.clayton 2 θ hθ).cdf ![b, d]

A positive rectangle's density integral approximates the upper-corner CDF to within the sum of its two lower-edge cutoffs.

theorem Papers.AnsariRockel2024.clayton_density_formula_cutoff_rectangle_tendsto_cdf (θ : ℝ) (hθ : 0 < θ) (b d : ↑unitInterval) (r : ℕ → ↑unitInterval) (hr : ∀ (n : ℕ), 0 < ↑(r n) ∧ r n ≤ b ∧ r n ≤ d) (h0 : Filter.Tendsto (fun (n : ℕ) => ↑(r n)) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ) in ↑(r n)..↑b, ∫ (y : ℝ) in ↑(r n)..↑d, (1 + θ) * x ^ (-θ - 1) * y ^ (-θ - 1) * Papers.AnsariRockel2024.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ)) Filter.atTop (nhds ((ProbabilityTheory.Copula.clayton 2 θ hθ).cdf ![b, d]))

Integrating the candidate density from a vanishing positive cutoff to any fixed positive upper corner converges to that Clayton CDF value.