← Copula mathematical handbook

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

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

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

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

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

The analytic mixed derivative is exactly the explicit Clayton density formula at every strictly positive coordinate.

theorem ProbabilityTheory.Copula.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) * ProbabilityTheory.Copula.claytonBaseReal✝ θ u y ^ (-2 - 1 / θ) = u ^ (-θ - 1) * ProbabilityTheory.Copula.claytonBaseReal✝ θ u b ^ (-1 / θ - 1) - u ^ (-θ - 1) * ProbabilityTheory.Copula.claytonBaseReal✝ θ u a ^ (-1 / θ - 1)

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

theorem ProbabilityTheory.Copula.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) * ProbabilityTheory.Copula.claytonBaseReal✝ θ x v ^ (-1 / θ - 1) = ProbabilityTheory.Copula.claytonBaseReal✝ θ b v ^ (-1 / θ) - ProbabilityTheory.Copula.claytonBaseReal✝ θ a v ^ (-1 / θ)

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

theorem ProbabilityTheory.Copula.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) * ProbabilityTheory.Copula.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) = ProbabilityTheory.Copula.claytonBaseReal✝ θ b d ^ (-1 / θ) - ProbabilityTheory.Copula.claytonBaseReal✝ θ a d ^ (-1 / θ) - ProbabilityTheory.Copula.claytonBaseReal✝ θ b c ^ (-1 / θ) + ProbabilityTheory.Copula.claytonBaseReal✝ θ a c ^ (-1 / θ)

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

theorem ProbabilityTheory.Copula.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) * ProbabilityTheory.Copula.claytonBaseReal✝ θ x y ^ (-2 - 1 / θ) = (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 ProbabilityTheory.Copula.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), claytonDensityFormula θ x = (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 ProbabilityTheory.Copula.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 (claytonDensityFormula θ x)) (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i)) = (clayton 2 θ hθ).toMeasure (Set.univ.pi fun (i : Fin 2) => Set.Ioc (![a, c] i) (![b, d] i))

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

theorem ProbabilityTheory.Copula.clayton_withDensity_axis_zero (θ : ℝ) (i : Fin 2) : (MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (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 ProbabilityTheory.Copula.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 (claytonDensityFormula θ x)) (Set.univ.pi fun (i : Fin 2) => Set.Ioc 0 (![u, v] i)) = (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 ProbabilityTheory.Copula.clayton_withDensity_lowerOrthant_eq_measure (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (claytonDensityFormula θ x)) (Set.Iic ![u, v]) = (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 ProbabilityTheory.Copula.clayton_toMeasure_eq_withDensity_positive (θ : ℝ) (hθ : 0 < θ) : (clayton 2 θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (claytonDensityFormula θ x)

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

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

Positive Clayton has an actual nonnegative MTP2 density, given by the the explicit formula above.

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

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

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

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