← Mathematical handbook

Lipschitz continuity of copula distribution functions

The difference between two lower orthants is contained in a union of coordinate strips. Uniform marginals bound the mass of each strip by its length. This gives the sharp Lipschitz bound for the sum of coordinate distances. With the default maximum metric on the cube, the resulting Lipschitz constant is d.

theorem ProbabilityTheory.Copula.cdf_sub_le_sum_abs {d : ℕ} (C : Copula d) (u v : Fin d → ↑unitInterval) : C.cdf u - C.cdf v ≤ ∑ i : Fin d, |↑(u i) - ↑(v i)|

A one-sided version of the Lipschitz estimate for the sum metric.

theorem ProbabilityTheory.Copula.abs_cdf_sub_le_sum_abs {d : ℕ} (C : Copula d) (u v : Fin d → ↑unitInterval) : |C.cdf u - C.cdf v| ≤ ∑ i : Fin d, |↑(u i) - ↑(v i)|

A copula CDF is 1-Lipschitz for the sum of coordinate distances.

theorem ProbabilityTheory.Copula.lipschitzWith_cdf {d : ℕ} (C : Copula d) : LipschitzWith (↑d) C.cdf

For Lean's default maximum metric on the cube, the Lipschitz constant is d.

theorem ProbabilityTheory.Copula.uniformContinuous_cdf {d : ℕ} (C : Copula d) : UniformContinuous C.cdf

Copula CDFs are uniformly continuous on the cube.

theorem ProbabilityTheory.Copula.continuous_cdf {d : ℕ} (C : Copula d) : Continuous C.cdf

Copula CDFs are continuous on the cube.