← Copula mathematical handbook

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.

noncomputable def ProbabilityTheory.Copula.cdf {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : ℝ

The distribution function of a copula on the unit cube.

Equations

• C.cdf u = C.toMeasure.real (Set.Iic u)

theorem ProbabilityTheory.Copula.cdf_nonneg {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : 0 ≤ C.cdf u

theorem ProbabilityTheory.Copula.cdf_le_one {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : C.cdf u ≤ 1

theorem ProbabilityTheory.Copula.monotone_cdf {d : ℕ} (C : Copula d) : Monotone C.cdf

The copula CDF is monotone in the pointwise order.

@[simp]

theorem ProbabilityTheory.Copula.cdf_one {d : ℕ} (C : Copula d) : (C.cdf fun (x : Fin d) => 1) = 1

theorem ProbabilityTheory.Copula.cdf_le_coord {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) (i : Fin d) : C.cdf u ≤ ↑(u i)

Every coordinate is an upper bound for the CDF.

theorem ProbabilityTheory.Copula.cdf_eq_zero_of_coord_eq_zero {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) (i : Fin d) (hi : u i = 0) : C.cdf u = 0

A lower orthant with a zero coordinate has zero mass.

@[simp]

theorem ProbabilityTheory.Copula.cdf_zero {d : ℕ} (C : Copula d) [NeZero d] : (C.cdf fun (x : Fin d) => 0) = 0

@[simp]

theorem ProbabilityTheory.Copula.cdf_update_one {d : ℕ} (C : Copula d) (i : Fin d) (u : ↑unitInterval) : C.cdf (Function.update (fun (x : Fin d) => 1) i u) = ↑u

With all other coordinates equal to one, the CDF is the remaining coordinate.

@[simp]

theorem ProbabilityTheory.Copula.cdf_dim_zero (C : Copula 0) (u : Fin 0 → ↑unitInterval) : C.cdf u = 1

The empty lower orthant is the whole zero-dimensional cube.