← Mathematical handbook

Regularity derived from the classical copula conditions

Rectangle increments split additively along each coordinate. Positivity then gives monotonicity and the Lipschitz estimate; continuity is a consequence of the classical conditions, rather than an extra hypothesis.

theorem ProbabilityTheory.Copula.partialIncrement_congr_lower {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (a a' b : Fin d → ↑unitInterval) (s : Finset (Fin d)) (ha : ∀ i ∈ s, a i = a' i) : partialIncrement F a b s = partialIncrement F a' b s

theorem ProbabilityTheory.Copula.rectangleIncrement_split {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (a b : Fin d → ↑unitInterval) (i : Fin d) (t : ↑unitInterval) : rectangleIncrement F a b = rectangleIncrement F a (Function.update b i t) + rectangleIncrement F (Function.update a i t) b

Finite additivity under a cut, including cuts at the endpoints.

theorem ProbabilityTheory.Copula.rectangleIncrement_eq_zero_of_eq {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (a b : Fin d → ↑unitInterval) (i : Fin d) (hi : a i = b i) : rectangleIncrement F a b = 0

theorem ProbabilityTheory.Copula.IsClassical.partialIncrement_zero_lower {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (a b : Fin d → ↑unitInterval) (s : Finset (Fin d)) (ha : ∀ i ∈ s, a i = 0) : partialIncrement F a b s = F b

theorem ProbabilityTheory.Copula.IsClassical.rectangleIncrement_zero_lower {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (b : Fin d → ↑unitInterval) : rectangleIncrement F (fun (x : Fin d) => 0) b = F b

theorem ProbabilityTheory.Copula.IsClassical.rectangleIncrement_slab {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (b : Fin d → ↑unitInterval) (i : Fin d) (t : ↑unitInterval) : rectangleIncrement F (Function.update (fun (x : Fin d) => 0) i t) b = F b - F (Function.update b i t)

theorem ProbabilityTheory.Copula.IsClassical.rectangleIncrement_mono_upper {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (a b c : Fin d → ↑unitInterval) (hab : a ≤ b) (hbc : b ≤ c) : rectangleIncrement F a b ≤ rectangleIncrement F a c

Rectangle mass increases when its upper endpoint increases.

theorem ProbabilityTheory.Copula.IsClassical.monotone {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) : Monotone F

Coordinatewise monotonicity follows from the rectangle condition.

theorem ProbabilityTheory.Copula.IsClassical.update_sub_le {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (u : Fin d → ↑unitInterval) (i : Fin d) (t : ↑unitInterval) (ht : u i ≤ t) : F (Function.update u i t) - F u ≤ ↑t - ↑(u i)

theorem ProbabilityTheory.Copula.IsClassical.sub_le_sum_of_le {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (a b : Fin d → ↑unitInterval) (hab : a ≤ b) : F b - F a ≤ ∑ i : Fin d, (↑(b i) - ↑(a i))

theorem ProbabilityTheory.Copula.IsClassical.sub_le_sum_abs {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (a b : Fin d → ↑unitInterval) : F a - F b ≤ ∑ i : Fin d, |↑(a i) - ↑(b i)|

theorem ProbabilityTheory.Copula.IsClassical.abs_sub_le_sum_abs {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) (a b : Fin d → ↑unitInterval) : |F a - F b| ≤ ∑ i : Fin d, |↑(a i) - ↑(b i)|

The sharp Lipschitz estimate in the sum of coordinate distances.

theorem ProbabilityTheory.Copula.IsClassical.lipschitzWith {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) : LipschitzWith (↑d) F

theorem ProbabilityTheory.Copula.IsClassical.continuous {d : ℕ} {F : (Fin d → ↑unitInterval) → ℝ} (hF : IsClassical F) : Continuous F