WIP: Add finite-dimensional copulas and Sklar's theorem

LeanPool/Copula.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Marcus Rockel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marcus Rockel, Gaëtan Serré, Rémy Degenne
+-/
+
+module
+
+public import LeanPool.Copula.Classical.Characterization
+public import LeanPool.Copula.Sklar.General
+public import LeanPool.Copula.CDF.Bounds
+
+/-!
+# Finite-dimensional copulas and Sklar's theorem
+
+Source: url:https://github.com/Corrram/copula/tree/fe53ea2f3e6af41da8541e7d0aa2edc38ed0dcc8
+Authors: Marcus Rockel, Gaëtan Serré, Rémy Degenne
+Status: verified
+Main declarations: `ProbabilityTheory.Copula.exists_sklarCopula`
+Tags: copulas, sklar-theorem, probability-measures, disintegration, quantiles
+MSC: 60E05, 60B05
+-/
+
+/-!
+## Mathematical scope
+
+The completed core of Marcus Rockel's copula library, from
+https://github.com/Corrram/copula/tree/fe53ea2f3e6af41da8541e7d0aa2edc38ed0dcc8.
+It includes arbitrary real marginals, continuous-marginal uniqueness, the classical
+CDF characterization in every finite dimension, and reusable randomized lifting.
+-/

LeanPool/Copula/Basic.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2026 Marcus Rockel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marcus Rockel
+-/
+module
+
+public import Mathlib.MeasureTheory.Constructions.UnitInterval
+public import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
+
+/-!
+# Copulas as probability measures
+
+A copula is a probability measure on a finite power of the unit interval with
+uniform coordinate marginals. Dimension zero is allowed. The usual copula
+distribution function is derived in `Copula.CDF`.
+-/
+
+public section
+
+open MeasureTheory
+open scoped unitInterval
+
+namespace ProbabilityTheory
+
+/-- A `d`-dimensional copula, represented by a probability measure on `[0, 1]^d`
+whose coordinate marginals are the canonical uniform probability measure. -/
+structure Copula (d : ℕ) where
+  /-- The probability measure underlying the copula. -/
+  measure : ProbabilityMeasure (Fin d → I)
+  /-- Every coordinate has the uniform distribution on the unit interval. -/
+  marginal_eq (i : Fin d) : measure.toMeasure.map (fun x => x i) = volume
+
+namespace Copula
+
+variable {d : ℕ}
+
+/-- The underlying measure, for use with mathlib's measure-theoretic API. -/
+@[expose]
+def toMeasure (C : Copula d) : Measure (Fin d → I) := C.measure.toMeasure
+
+instance (C : Copula d) : IsProbabilityMeasure C.toMeasure :=
+  inferInstanceAs (IsProbabilityMeasure C.measure.toMeasure)
+
+@[ext]
+theorem ext {C D : Copula d} (h : C.toMeasure = D.toMeasure) : C = D := by
+  have hmeasure : C.measure = D.measure := ProbabilityMeasure.toMeasure_injective h
+  cases C
+  cases D
+  cases hmeasure
+  rfl
+
+theorem toMeasure_injective : Function.Injective (toMeasure (d := d)) :=
+  fun _ _ h => ext h
+
+@[simp]
+theorem map_eval (C : Copula d) (i : Fin d) :
+    C.toMeasure.map (fun x => x i) = volume :=
+  C.marginal_eq i
+
+/-- Coordinate projections preserve the uniform measure. -/
+theorem measurePreserving_eval (C : Copula d) (i : Fin d) :
+    MeasurePreserving (fun x => x i) C.toMeasure volume :=
+  ⟨measurable_pi_apply i, C.map_eval i⟩
+
+/-- The probability of a measurable coordinate event is its uniform volume. -/
+theorem measure_preimage_eval (C : Copula d) (i : Fin d) {s : Set I}
+    (hs : MeasurableSet s) : C.toMeasure ((fun x => x i) ⁻¹' s) = volume s := by
+  rw [← Measure.map_apply (measurable_pi_apply i) hs, C.map_eval]
+
+@[simp]
+theorem measure_eval_le (C : Copula d) (i : Fin d) (u : I) :
+    C.toMeasure {x | x i ≤ u} = ENNReal.ofReal (u : ℝ) := by
+  exact (C.measure_preimage_eval i measurableSet_Iic).trans (unitInterval.volume_Iic u)
+
+@[simp]
+theorem measureReal_eval_le (C : Copula d) (i : Fin d) (u : I) :
+    C.toMeasure.real {x | x i ≤ u} = (u : ℝ) := by
+  simp [Measure.real, C.measure_eval_le, u.property.1]
+
+/-- Construct a copula from a random vector with uniform coordinate laws. -/
+@[expose]
+noncomputable def ofMap {Ω : Type*} [MeasurableSpace Ω]
+    (μ : ProbabilityMeasure Ω) (X : Ω → Fin d → I) (hX : Measurable X)
+    (hmarg : ∀ i, μ.toMeasure.map (fun ω => X ω i) = volume) : Copula d where
+  measure := μ.map X
+  marginal_eq i := by
+    rw [ProbabilityMeasure.toMeasure_map, Measure.map_map (measurable_pi_apply i) hX]
+    exact hmarg i
+
+@[simp]
+theorem toMeasure_ofMap {Ω : Type*} [MeasurableSpace Ω]
+    (μ : ProbabilityMeasure Ω) (X : Ω → Fin d → I) (hX : Measurable X)
+    (hmarg : ∀ i, μ.toMeasure.map (fun ω => X ω i) = volume) :
+    (ofMap μ X hX hmarg).toMeasure = μ.toMeasure.map X := rfl
+
+end Copula
+end ProbabilityTheory

LeanPool/Copula/CDF.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2026 Marcus Rockel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marcus Rockel
+-/
+module
+
+public import LeanPool.Copula.Basic
+
+/-!
+# The distribution function of a copula
+
+The CDF is the real-valued mass of a lower orthant. The pointwise order on the
+cube lets us use `Set.Iic` directly. Groundedness requires a coordinate; in
+dimension zero the CDF is identically one.
+-/
+
+public section
+
+open MeasureTheory Set
+open scoped unitInterval
+
+namespace ProbabilityTheory.Copula
+
+variable {d : ℕ}
+
+/-- The distribution function of a copula on the unit cube. -/
+@[expose]
+noncomputable def cdf (C : Copula d) (u : Fin d → I) : ℝ :=
+  C.toMeasure.real (Iic u)
+
+theorem cdf_nonneg (C : Copula d) (u : Fin d → I) : 0 ≤ C.cdf u :=
+  measureReal_nonneg
+
+theorem cdf_le_one (C : Copula d) (u : Fin d → I) : C.cdf u ≤ 1 :=
+  measureReal_le_one
+
+/-- The copula CDF is monotone in the pointwise order. -/
+theorem monotone_cdf (C : Copula d) : Monotone C.cdf := by
+  intro u v huv
+  exact measureReal_mono (Iic_subset_Iic.mpr huv)
+
+@[simp]
+theorem cdf_one (C : Copula d) : C.cdf (fun _ => 1) = 1 := by
+  have h : Iic (fun _ : Fin d => (1 : I)) = univ := by
+    ext x
+    simp [mem_Iic, Pi.le_def, unitInterval.le_one']
+  simp [cdf, h]
+
+/-- Every coordinate is an upper bound for the CDF. -/
+theorem cdf_le_coord (C : Copula d) (u : Fin d → I) (i : Fin d) :
+    C.cdf u ≤ (u i : ℝ) := by
+  calc
+    C.cdf u ≤ C.toMeasure.real {x | x i ≤ u i} :=
+      measureReal_mono (fun _ hx => hx i)
+    _ = (u i : ℝ) := C.measureReal_eval_le i (u i)
+
+/-- A lower orthant with a zero coordinate has zero mass. -/
+theorem cdf_eq_zero_of_coord_eq_zero (C : Copula d) (u : Fin d → I)
+    (i : Fin d) (hi : u i = 0) : C.cdf u = 0 := by
+  apply le_antisymm _ (C.cdf_nonneg u)
+  simpa [hi] using C.cdf_le_coord u i
+
+@[simp]
+theorem cdf_zero (C : Copula d) [NeZero d] : C.cdf (fun _ => 0) = 0 :=
+  C.cdf_eq_zero_of_coord_eq_zero _ ⟨0, Nat.pos_of_ne_zero (NeZero.ne d)⟩ rfl
+
+/-- With all other coordinates equal to one, the CDF is the remaining coordinate. -/
+@[simp]
+theorem cdf_update_one (C : Copula d) (i : Fin d) (u : I) :
+    C.cdf (Function.update (fun _ => 1) i u) = (u : ℝ) := by
+  have h : Iic (Function.update (fun _ : Fin d => (1 : I)) i u) =
+      {x | x i ≤ u} := by
+    ext x
+    constructor
+    · intro hx
+      simpa using hx i
+    · intro hx j
+      by_cases hji : j = i
+      · subst j
+        simpa using hx
+      · simpa [Function.update_of_ne hji] using (unitInterval.le_one' (t := x j))
+  rw [cdf, h, C.measureReal_eval_le]
+
+/-- The empty lower orthant is the whole zero-dimensional cube. -/
+@[simp]
+theorem cdf_dim_zero (C : Copula 0) (u : Fin 0 → I) : C.cdf u = 1 := by
+  have h : u = fun _ => 1 := Subsingleton.elim _ _
+  rw [h, C.cdf_one]
+
+end ProbabilityTheory.Copula

LeanPool/Copula/CDF/Bounds.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 Marcus Rockel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marcus Rockel
+-/
+module
+
+public import LeanPool.Copula.CDF
+
+/-!
+# Fréchet–Hoeffding bounds
+
+Every copula lies between the lower bound `max 0 (∑ i, u i - d + 1)` and the
+minimum coordinate. The upper bound uses an infimum in the unit interval, so
+its value in dimension zero is one. These are bounds on the CDF; the lower
+bound does not in general define a copula in dimensions greater than two.
+-/
+
+public section
+
+open MeasureTheory Set
+open scoped unitInterval BigOperators
+
+namespace ProbabilityTheory.Copula
+
+variable {d : ℕ}
+
+/-- The untruncated lower Fréchet–Hoeffding bound, obtained from the union bound. -/
+theorem sum_sub_dim_add_one_le_cdf (C : Copula d) (u : Fin d → I) :
+    (∑ i, (u i : ℝ)) - d + 1 ≤ C.cdf u := by
+  have hcomp : (Iic u)ᶜ = ⋃ i, {x | u i < x i} := by
+    ext x
+    simp [mem_Iic, Pi.le_def, not_forall, not_le]
+  have hcoord (i : Fin d) : C.toMeasure.real {x | u i < x i} = 1 - (u i : ℝ) := by
+    change (C.toMeasure ((fun x => x i) ⁻¹' Ioi (u i))).toReal = _
+    rw [C.measure_preimage_eval i measurableSet_Ioi, unitInterval.volume_Ioi,
+      ENNReal.toReal_ofReal (sub_nonneg.mpr (u i).property.2)]
+  have hunion := measureReal_iUnion_fintype_le (μ := C.toMeasure)
+    (fun i : Fin d => {x | u i < x i})
+  rw [← hcomp, measureReal_compl measurableSet_Iic, probReal_univ] at hunion
+  simp_rw [hcoord] at hunion
+  have h : 1 - C.cdf u ≤ (d : ℝ) - ∑ i, (u i : ℝ) := by
+    simpa [cdf, Finset.sum_sub_distrib] using hunion
+  linarith
+
+/-- The lower Fréchet–Hoeffding bound, including dimension zero. -/
+theorem frechet_lower_le_cdf (C : Copula d) (u : Fin d → I) :
+    max 0 ((∑ i, (u i : ℝ)) - d + 1) ≤ C.cdf u :=
+  max_le (C.cdf_nonneg u) (C.sum_sub_dim_add_one_le_cdf u)
+
+/-- The upper Fréchet–Hoeffding bound, with the empty infimum equal to one. -/
+theorem cdf_le_frechet_upper (C : Copula d) (u : Fin d → I) :
+    C.cdf u ≤ ((⨅ i, u i : I) : ℝ) := by
+  have h : (⟨C.cdf u, C.cdf_nonneg u, C.cdf_le_one u⟩ : I) ≤ ⨅ i, u i :=
+    le_iInf fun i => C.cdf_le_coord u i
+  exact h
+
+end ProbabilityTheory.Copula

LeanPool/Copula/CDF/Continuity.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2026 Marcus Rockel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Marcus Rockel
+-/
+module
+
+public import LeanPool.Copula.CDF
+
+/-!
+# 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`.
+-/
+
+public section
+
+open MeasureTheory Set
+open scoped unitInterval BigOperators NNReal
+
+namespace ProbabilityTheory.Copula
+
+variable {d : ℕ}
+
+/-- A one-sided version of the Lipschitz estimate for the sum metric. -/
+theorem cdf_sub_le_sum_abs (C : Copula d) (u v : Fin d → I) :
+    C.cdf u - C.cdf v ≤ ∑ i, |(u i : ℝ) - (v i : ℝ)| := by
+  let strip (i : Fin d) : Set (Fin d → I) :=
+    (fun x => x i) ⁻¹' uIoc (v i) (u i)
+  have hsub : Iic u \ Iic v ⊆ ⋃ i, strip i := by
+    intro x hx
+    obtain ⟨i, hi⟩ := not_forall.mp hx.2
+    refine mem_iUnion.mpr ⟨i, ?_⟩
+    exact mem_uIoc.mpr (Or.inl ⟨lt_of_not_ge hi, hx.1 i⟩)
+  have hstrip (i : Fin d) : C.toMeasure.real (strip i) = |(u i : ℝ) - (v i : ℝ)| := by
+    change (C.toMeasure ((fun x => x i) ⁻¹' uIoc (v i) (u i))).toReal = _
+    rw [C.measure_preimage_eval i measurableSet_uIoc, unitInterval.volume_uIoc,
+      edist_dist, ENNReal.toReal_ofReal dist_nonneg, Subtype.dist_eq, Real.dist_eq]
+  calc
+    C.cdf u - C.cdf v ≤ C.toMeasure.real (Iic u \ Iic v) := le_measureReal_sdiff
+    _ ≤ C.toMeasure.real (⋃ i, strip i) := measureReal_mono hsub
+    _ ≤ ∑ i, C.toMeasure.real (strip i) := measureReal_iUnion_fintype_le strip
+    _ = ∑ i, |(u i : ℝ) - (v i : ℝ)| := Finset.sum_congr rfl (fun i _ => hstrip i)
+
+/-- A copula CDF is 1-Lipschitz for the sum of coordinate distances. -/
+theorem abs_cdf_sub_le_sum_abs (C : Copula d) (u v : Fin d → I) :
+    |C.cdf u - C.cdf v| ≤ ∑ i, |(u i : ℝ) - (v i : ℝ)| := by
+  refine abs_le.mpr ⟨?_, C.cdf_sub_le_sum_abs u v⟩
+  have h : C.cdf v - C.cdf u ≤ ∑ i, |(u i : ℝ) - (v i : ℝ)| := by
+    simpa only [abs_sub_comm] using C.cdf_sub_le_sum_abs v u
+  linarith
+
+/-- For Lean's default maximum metric on the cube, the Lipschitz constant is `d`. -/
+theorem lipschitzWith_cdf (C : Copula d) : LipschitzWith (d : ℝ≥0) C.cdf := by
+  apply LipschitzWith.of_dist_le_mul
+  intro u v
+  calc
+    dist (C.cdf u) (C.cdf v) = |C.cdf u - C.cdf v| := Real.dist_eq _ _
+    _ ≤ ∑ i, |(u i : ℝ) - (v i : ℝ)| := C.abs_cdf_sub_le_sum_abs u v
+    _ ≤ ∑ _ : Fin d, dist u v := Finset.sum_le_sum fun i _ => by
+      simpa [Subtype.dist_eq, Real.dist_eq] using dist_le_pi_dist u v i
+    _ = (d : ℝ≥0) * dist u v := by simp
+
+/-- Copula CDFs are uniformly continuous on the cube. -/
+theorem uniformContinuous_cdf (C : Copula d) : UniformContinuous C.cdf :=
+  C.lipschitzWith_cdf.uniformContinuous
+
+/-- Copula CDFs are continuous on the cube. -/
+@[fun_prop]
+theorem continuous_cdf (C : Copula d) : Continuous C.cdf :=
+  C.lipschitzWith_cdf.continuous
+
+end ProbabilityTheory.Copula