← Copula mathematical handbook

Finite interval partitions and clipped local coordinates

structure ProbabilityTheory.Copula.IntervalPartition (n : ℕ) : Type

A strictly increasing finite partition of the whole unit interval. Positive cell lengths exclude division by zero; a partition with no cells cannot satisfy the two endpoint requirements.

• point : Fin (n + 1) → ↑unitInterval
• strictMono : StrictMono self.point
• zero : self.point 0 = 0
• one : self.point (Fin.last n) = 1

def ProbabilityTheory.Copula.IntervalPartition.width {n : ℕ} (P : IntervalPartition n) (i : Fin n) : ℝ

Length of a partition cell.

Equations

• P.width i = ↑(P.point i.succ) - ↑(P.point i.castSucc)

theorem ProbabilityTheory.Copula.IntervalPartition.width_pos {n : ℕ} (P : IntervalPartition n) (i : Fin n) : 0 < P.width i

noncomputable def ProbabilityTheory.Copula.IntervalPartition.coord {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) : ↑unitInterval

Inverse affine coordinate in a cell, clipped to the unit interval.

Equations

• P.coord i u = Set.projIcc 0 1 ProbabilityTheory.Copula.IntervalPartition.coord._proof_1 ((↑u - ↑(P.point i.castSucc)) / P.width i)

theorem ProbabilityTheory.Copula.IntervalPartition.coord_mono {n : ℕ} (P : IntervalPartition n) (i : Fin n) : Monotone (P.coord i)

theorem ProbabilityTheory.Copula.IntervalPartition.coord_of_le {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) (hu : u ≤ P.point i.castSucc) : P.coord i u = 0

theorem ProbabilityTheory.Copula.IntervalPartition.coord_of_ge {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) (hu : P.point i.succ ≤ u) : P.coord i u = 1

@[simp]

theorem ProbabilityTheory.Copula.IntervalPartition.coord_zero {n : ℕ} (P : IntervalPartition n) (i : Fin n) : P.coord i 0 = 0

@[simp]

theorem ProbabilityTheory.Copula.IntervalPartition.coord_one {n : ℕ} (P : IntervalPartition n) (i : Fin n) : P.coord i 1 = 1

theorem ProbabilityTheory.Copula.IntervalPartition.coe_coord_of_mem {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) (hl : P.point i.castSucc ≤ u) (hr : u ≤ P.point i.succ) : ↑(P.coord i u) = (↑u - ↑(P.point i.castSucc)) / P.width i

theorem ProbabilityTheory.Copula.IntervalPartition.width_mul_coord {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) : P.width i * ↑(P.coord i u) = min ↑u ↑(P.point i.succ) - min ↑u ↑(P.point i.castSucc)

theorem ProbabilityTheory.Copula.IntervalPartition.sum_differences {n : ℕ} (f : Fin (n + 1) → ℝ) : ∑ i : Fin n, (f i.succ - f i.castSucc) = f (Fin.last n) - f 0

Telescoping over consecutive endpoints, including the empty sum.

theorem ProbabilityTheory.Copula.IntervalPartition.sum_width_mul_coord {n : ℕ} (P : IntervalPartition n) (u : ↑unitInterval) : ∑ i : Fin n, P.width i * ↑(P.coord i u) = ↑u

@[simp]

theorem ProbabilityTheory.Copula.IntervalPartition.sum_width {n : ℕ} (P : IntervalPartition n) : ∑ i : Fin n, P.width i = 1

noncomputable def ProbabilityTheory.Copula.IntervalPartition.uniform (n : ℕ) (hn : 0 < n) : IntervalPartition n

The equally spaced partition into n cells, for n > 0.

Equations

• ProbabilityTheory.Copula.IntervalPartition.uniform n hn = { point := fun (i : Fin (n + 1)) => ⟨↑↑i / ↑n, ⋯⟩, strictMono := ⋯, zero := ⋯, one := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.IntervalPartition.width_uniform (n : ℕ) (hn : 0 < n) (i : Fin n) : (uniform n hn).width i = 1 / ↑n