← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.quadratic_unit_lipschitz (s t : ↑unitInterval) : |↑s - ↑s ^ 2 - (↑t - ↑t ^ 2)| ≤ |↑s - ↑t|

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.pieceValue_lipschitz {n v w : ℝ} (hn : 0 ≤ n) (hv : 0 ≤ v) (_hw : 0 ≤ w) (i : Fin 4) (s t : ↑unitInterval) : |pieceValue n v w i ↑s - pieceValue n v w i ↑t| ≤ v * |piecePoint n v w i ↑s - piecePoint n v w i ↑t|

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.basePotential_piece_lipschitz {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (i : Fin 4) (x : ℝ) (hx : x ∈ Set.Icc (piecePoint n v w i 0) (piecePoint n v w i 1)) (y : ℝ) (hy : y ∈ Set.Icc (piecePoint n v w i 0) (piecePoint n v w i 1)) : |basePotential n v w x - basePotential n v w y| ≤ v * |x - y|

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.basePotential_lipschitz {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (x : ℝ) (hx : x ∈ Set.Icc 0 (period n v w)) (y : ℝ) (hy : y ∈ Set.Icc 0 (period n v w)) : |basePotential n v w x - basePotential n v w y| ≤ v * |x - y|

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential_lipschitz {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hp : 0 < period n v w) : LipschitzWith ⟨v, hv⟩ (potential n v w hp)

The periodic extension preserves the sharp Lipschitz constant, including across its seams.