← Copula mathematical handbook

Sobolev energy and the Siburg–Stoimenov dependence coefficient

The squared modified Sobolev norm is the sum of the two directional conditional CDF energies. The derivative representation is proved without a density assumption. Siburg–Stoimenov's coefficient is sqrt (3 * energy - 2); its square equals the average of the two directional Chatterjee coefficients.

noncomputable def ProbabilityTheory.Copula.sobolevNormSq (C : Copula 2) : ℝ

Squared modified Sobolev norm: the integrated squares of both first partials.

Equations

• C.sobolevNormSq = (∫ (v : ↑unitInterval) (u : ↑unitInterval), C.conditionalCDF u v ^ 2) + ∫ (v : ↑unitInterval) (u : ↑unitInterval), C.transpose.conditionalCDF u v ^ 2

noncomputable def ProbabilityTheory.Copula.sobolevNorm (C : Copula 2) : ℝ

The modified Sobolev norm of a bivariate copula.

Equations

• C.sobolevNorm = √C.sobolevNormSq

noncomputable def ProbabilityTheory.Copula.sobolevDistanceSq (C D : Copula 2) : ℝ

Squared Sobolev distance, using both directional conditional distributions.

Equations

• C.sobolevDistanceSq D = C.conditionalCDFDistanceSq D + C.transpose.conditionalCDFDistanceSq D.transpose

noncomputable def ProbabilityTheory.Copula.sobolevDependenceSq (C : Copula 2) : ℝ

Squared Siburg–Stoimenov dependence coefficient.

Equations

• C.sobolevDependenceSq = 3 * C.sobolevNormSq - 2

noncomputable def ProbabilityTheory.Copula.sobolevDependence (C : Copula 2) : ℝ

Siburg–Stoimenov's normalized Sobolev dependence coefficient ω.

Equations

• C.sobolevDependence = √C.sobolevDependenceSq

theorem ProbabilityTheory.Copula.sobolevNormSq_eq_integral_deriv (C : Copula 2) : C.sobolevNormSq = (∫ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.cdfSection v) ↑u ^ 2) + ∫ (v : ↑unitInterval) (u : ↑unitInterval), deriv (C.transpose.cdfSection v) ↑u ^ 2

theorem ProbabilityTheory.Copula.sobolevDependenceSq_eq_chatterjeeXi (C : Copula 2) : C.sobolevDependenceSq = (C.chatterjeeXi + C.transpose.chatterjeeXi) / 2

theorem ProbabilityTheory.Copula.sobolevDependenceSq_mem_Icc (C : Copula 2) : C.sobolevDependenceSq ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.sobolevNormSq_mem_Icc (C : Copula 2) : C.sobolevNormSq ∈ Set.Icc (2 / 3) 1

theorem ProbabilityTheory.Copula.sobolevDependence_mem_Icc (C : Copula 2) : C.sobolevDependence ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.sobolevNorm_sq (C : Copula 2) : C.sobolevNorm ^ 2 = C.sobolevNormSq

theorem ProbabilityTheory.Copula.sobolevDependence_sq (C : Copula 2) : C.sobolevDependence ^ 2 = C.sobolevDependenceSq

@[simp]

theorem ProbabilityTheory.Copula.sobolevNormSq_transpose (C : Copula 2) : C.transpose.sobolevNormSq = C.sobolevNormSq

@[simp]

theorem ProbabilityTheory.Copula.sobolevDependence_transpose (C : Copula 2) : C.transpose.sobolevDependence = C.sobolevDependence

theorem ProbabilityTheory.Copula.sobolevDistanceSq_nonneg (C D : Copula 2) : 0 ≤ C.sobolevDistanceSq D

theorem ProbabilityTheory.Copula.sobolevDistanceSq_comm (C D : Copula 2) : C.sobolevDistanceSq D = D.sobolevDistanceSq C

@[simp]

theorem ProbabilityTheory.Copula.sobolevDistanceSq_self (C : Copula 2) : C.sobolevDistanceSq C = 0

theorem ProbabilityTheory.Copula.sobolevDistanceSq_eq_zero_iff (C D : Copula 2) : C.sobolevDistanceSq D = 0 ↔ C = D

theorem ProbabilityTheory.Copula.sobolevDependenceSq_eq_distance_independence (C : Copula 2) : C.sobolevDependenceSq = 3 * C.sobolevDistanceSq (independence 2)

theorem ProbabilityTheory.Copula.sobolevDependence_eq_zero_iff (C : Copula 2) : C.sobolevDependence = 0 ↔ C = independence 2

theorem ProbabilityTheory.Copula.sobolevDependence_eq_one_iff (C : Copula 2) : C.sobolevDependence = 1 ↔ C.chatterjeeXi = 1 ∧ C.transpose.chatterjeeXi = 1

theorem ProbabilityTheory.Copula.IsMutuallyCompletelyDependent.sobolevDependence_eq_one {C : Copula 2} (h : C.IsMutuallyCompletelyDependent) : C.sobolevDependence = 1

@[simp]

theorem ProbabilityTheory.Copula.sobolevDependence_independence : (independence 2).sobolevDependence = 0

@[simp]

theorem ProbabilityTheory.Copula.sobolevDependence_comonotonic : (comonotonic 2).sobolevDependence = 1

@[simp]

theorem ProbabilityTheory.Copula.sobolevDependence_countermonotonic : countermonotonic.sobolevDependence = 1

theorem ProbabilityTheory.Copula.sobolevDependenceSq_mix_independence (C : Copula 2) (a : ↑unitInterval) : (C.mix (independence 2) a).sobolevDependenceSq = ↑a ^ 2 * C.sobolevDependenceSq

theorem ProbabilityTheory.Copula.sobolevDependence_mix_independence (C : Copula 2) (a : ↑unitInterval) : (C.mix (independence 2) a).sobolevDependence = ↑a * C.sobolevDependence

theorem ProbabilityTheory.Copula.sobolevDependenceSq_fgm (θ : ℝ) (hθ : |θ| ≤ 1) : (fgm θ hθ).sobolevDependenceSq = θ ^ 2 / 15