← Mathematical handbook

The comonotonic copula

Pushing uniform volume forward along the diagonal gives a copula whose coordinates agree almost surely.

noncomputable def ProbabilityTheory.Copula.comonotonic (d : ℕ) : Copula d

The comonotonic copula, the law of a repeated uniform random variable.

Equations

• ProbabilityTheory.Copula.comonotonic d = ProbabilityTheory.Copula.ofMap ⟨MeasureTheory.volume, ProbabilityTheory.Copula.comonotonic._proof_1⟩ (fun (u : ↑unitInterval) (x : Fin d) => u) ⋯ ⋯

@[simp]

theorem ProbabilityTheory.Copula.toMeasure_comonotonic (d : ℕ) : (comonotonic d).toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) (x : Fin d) => u) MeasureTheory.volume

@[simp]

theorem ProbabilityTheory.Copula.cdf_comonotonic {d : ℕ} (u : Fin d → ↑unitInterval) : (comonotonic d).cdf u = ↑(⨅ (i : Fin d), u i)

The comonotonic CDF is the minimum coordinate, with empty infimum equal to one.