← Copula mathematical handbook

Gluing copulas side by side

The gluing construction of Siburg and Stoimenov (Gluing copulas, Communications in Statistics – Theory and Methods 37 (2008)), in its n-fold form along the first coordinate. For an interval partition 0 = a₀ < a₁ < ⋯ < aₙ = 1 of [0,1] with cell widths pᵢ = aᵢ - aᵢ₋₁ and copulas C₁, …, Cₙ, the glued copula is

C(u,v) = aᵢ₋₁ v + pᵢ Cᵢ((u - aᵢ₋₁) / pᵢ, v) for aᵢ₋₁ ≤ u ≤ aᵢ

(cdf_gluing_of_mem). It is realized as the patchwork ∑ᵢ pᵢ Cᵢ(coordᵢ(u), v) with the clipped local coordinates of the partition (cdf_gluing). On the i-th strip its deviation from independence is the rescaled deviation pᵢ (Cᵢ - Π)(coordᵢ(u), v) (cdf_gluing_sub_mul_of_mem), and inside the strip its partial derivative in u is the rescaled partial derivative of Cᵢ (deriv_cdfSection_gluing_of_mem).

We also record some general partition calculus (maximal width, splitting ∫₀¹ along the cells, the affine change of variables on a cell) and the Lipschitz regularity of CDF sections.

Partitions: index positivity, the maximal width, and integration over cells

theorem ProbabilityTheory.Copula.IntervalPartition.pos {n : ℕ} (P : IntervalPartition n) : 0 < n

theorem ProbabilityTheory.Copula.IntervalPartition.univ_nonempty {n : ℕ} (P : IntervalPartition n) : Finset.univ.Nonempty

noncomputable def ProbabilityTheory.Copula.IntervalPartition.maxWidth {n : ℕ} (P : IntervalPartition n) : ℝ

The largest cell width max_i p_i of a partition.

Equations

• P.maxWidth = Finset.univ.sup' ⋯ P.width

theorem ProbabilityTheory.Copula.IntervalPartition.width_le_maxWidth {n : ℕ} (P : IntervalPartition n) (i : Fin n) : P.width i ≤ P.maxWidth

theorem ProbabilityTheory.Copula.IntervalPartition.exists_width_eq_maxWidth {n : ℕ} (P : IntervalPartition n) : ∃ (i : Fin n), P.width i = P.maxWidth

theorem ProbabilityTheory.Copula.IntervalPartition.maxWidth_pos {n : ℕ} (P : IntervalPartition n) : 0 < P.maxWidth

theorem ProbabilityTheory.Copula.IntervalPartition.maxWidth_le_one {n : ℕ} (P : IntervalPartition n) : P.maxWidth ≤ 1

theorem ProbabilityTheory.Copula.IntervalPartition.sum_pow_le_one {n : ℕ} (P : IntervalPartition n) (e : ℕ) (he : 1 ≤ e) : ∑ i : Fin n, P.width i ^ e ≤ 1

theorem ProbabilityTheory.Copula.IntervalPartition.sum_pow_pos {n : ℕ} (P : IntervalPartition n) (e : ℕ) : 0 < ∑ i : Fin n, P.width i ^ e

noncomputable def ProbabilityTheory.Copula.IntervalPartition.pt {n : ℕ} (P : IntervalPartition n) (k : ℕ) : ℝ

The points of a partition, indexed by natural numbers (constantly 1 beyond n).

Equations

• P.pt k = if h : k < n + 1 then ↑(P.point ⟨k, h⟩) else 1

theorem ProbabilityTheory.Copula.IntervalPartition.pt_zero {n : ℕ} (P : IntervalPartition n) : P.pt 0 = 0

theorem ProbabilityTheory.Copula.IntervalPartition.pt_n {n : ℕ} (P : IntervalPartition n) : P.pt n = 1

theorem ProbabilityTheory.Copula.IntervalPartition.pt_castSucc {n : ℕ} (P : IntervalPartition n) (i : Fin n) : P.pt ↑i = ↑(P.point i.castSucc)

theorem ProbabilityTheory.Copula.IntervalPartition.pt_succ {n : ℕ} (P : IntervalPartition n) (i : Fin n) : P.pt (↑i + 1) = ↑(P.point i.succ)

theorem ProbabilityTheory.Copula.IntervalPartition.cell_le {n : ℕ} (P : IntervalPartition n) (i : Fin n) : ↑(P.point i.castSucc) ≤ ↑(P.point i.succ)

theorem ProbabilityTheory.Copula.IntervalPartition.integral_eq_sum_cells {n : ℕ} (P : IntervalPartition n) (f : ℝ → ℝ) (hf : ∀ (i : Fin n), IntervalIntegrable f MeasureTheory.volume ↑(P.point i.castSucc) ↑(P.point i.succ)) : ∫ (t : ℝ) in 0..1, f t = ∑ i : Fin n, ∫ (t : ℝ) in ↑(P.point i.castSucc)..↑(P.point i.succ), f t

Splitting ∫₀¹ along the cells of a partition.

theorem ProbabilityTheory.Copula.IntervalPartition.integral_cell_comp {n : ℕ} (P : IntervalPartition n) (i : Fin n) (g : ℝ → ℝ) : ∫ (t : ℝ) in ↑(P.point i.castSucc)..↑(P.point i.succ), g ((t - ↑(P.point i.castSucc)) / P.width i) = P.width i * ∫ (s : ℝ) in 0..1, g s

The affine change of variables on one cell.

theorem ProbabilityTheory.Copula.IntervalPartition.coord_of_lt {n : ℕ} (P : IntervalPartition n) {i j : Fin n} (hji : j < i) (u : ↑unitInterval) (hl : P.point i.castSucc ≤ u) : P.coord j u = 1

theorem ProbabilityTheory.Copula.IntervalPartition.coord_of_gt {n : ℕ} (P : IntervalPartition n) {i j : Fin n} (hij : i < j) (u : ↑unitInterval) (hr : u ≤ P.point i.succ) : P.coord j u = 0

The glued copula

noncomputable def ProbabilityTheory.Copula.gluingData {n : ℕ} (P : IntervalPartition n) : PatchworkData (Fin n)

Patchwork data for gluing n scaled copulas side by side in the first coordinate: weights pᵢ = width i, first coordinates the clipped cell coordinates, second coordinates untouched.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.gluing {n : ℕ} (P : IntervalPartition n) (C : Fin n → Copula 2) : Copula 2

The gluing of the copulas C i, scaled to the cells of P, along the first coordinate (Siburg–Stoimenov).

Equations

• ProbabilityTheory.Copula.gluing P C = (ProbabilityTheory.Copula.gluingData P).copula C

theorem ProbabilityTheory.Copula.cdf_gluing {n : ℕ} (P : IntervalPartition n) (C : Fin n → Copula 2) (u v : ↑unitInterval) : (gluing P C).cdf ![u, v] = ∑ i : Fin n, P.width i * (C i).cdf ![P.coord i u, v]

theorem ProbabilityTheory.Copula.cdf_gluing_sub_mul {n : ℕ} (P : IntervalPartition n) (C : Fin n → Copula 2) (u v : ↑unitInterval) : (gluing P C).cdf ![u, v] - ↑u * ↑v = ∑ i : Fin n, P.width i * ((C i).cdf ![P.coord i u, v] - ↑(P.coord i u) * ↑v)

The deviation of the glued copula from independence, as a weighted sum.

theorem ProbabilityTheory.Copula.cdf_gluing_sub_mul_of_mem {n : ℕ} (P : IntervalPartition n) (C : Fin n → Copula 2) (i : Fin n) (u v : ↑unitInterval) (hl : P.point i.castSucc ≤ u) (hr : u ≤ P.point i.succ) : (gluing P C).cdf ![u, v] - ↑u * ↑v = P.width i * ((C i).cdf ![P.coord i u, v] - ↑(P.coord i u) * ↑v)

On the i-th strip only the i-th copula deviates from independence.

theorem ProbabilityTheory.Copula.cdf_gluing_of_mem {n : ℕ} (P : IntervalPartition n) (C : Fin n → Copula 2) (i : Fin n) (u v : ↑unitInterval) (hl : P.point i.castSucc ≤ u) (hr : u ≤ P.point i.succ) : (gluing P C).cdf ![u, v] = ↑(P.point i.castSucc) * ↑v + P.width i * (C i).cdf ![P.coord i u, v]

The Siburg–Stoimenov formula: on the strip aᵢ₋₁ ≤ u ≤ aᵢ, C(u,v) = aᵢ₋₁ v + pᵢ Cᵢ((u - aᵢ₋₁)/pᵢ, v).

@[simp]

theorem ProbabilityTheory.Copula.gluing_independence {n : ℕ} (P : IntervalPartition n) : (gluing P fun (x : Fin n) => independence 2) = independence 2

Gluing copies of the independence copula gives the independence copula.

Regularity of CDF sections

theorem ProbabilityTheory.Copula.lipschitzWith_cdfSection (D : Copula 2) (v : ↑unitInterval) : LipschitzWith 1 (D.cdfSection v)

theorem ProbabilityTheory.Copula.abs_deriv_cdfSection_le_one (D : Copula 2) (v : ↑unitInterval) (t : ℝ) : |deriv (D.cdfSection v) t| ≤ 1

theorem ProbabilityTheory.Copula.intervalIntegrable_deriv_cdfSection_sq (D : Copula 2) (v : ↑unitInterval) (a b : ℝ) : IntervalIntegrable (fun (t : ℝ) => deriv (D.cdfSection v) t ^ 2) MeasureTheory.volume a b

Sections of the glued copula

theorem ProbabilityTheory.Copula.cdfSection_gluing_of_mem {n : ℕ} (P : IntervalPartition n) (C : Fin n → Copula 2) (i : Fin n) (v : ↑unitInterval) {t : ℝ} (hl : ↑(P.point i.castSucc) ≤ t) (hr : t ≤ ↑(P.point i.succ)) : (gluing P C).cdfSection v t = P.width i * (C i).cdfSection v ((P.width i)⁻¹ * (t - ↑(P.point i.castSucc))) + ↑(P.point i.castSucc) * ↑v

On the closed i-th strip, the CDF section of the glued copula is an affine reparametrization of the CDF section of C i plus aᵢ₋₁ v.

theorem ProbabilityTheory.Copula.deriv_cdfSection_gluing_of_mem {n : ℕ} (P : IntervalPartition n) (C : Fin n → Copula 2) (i : Fin n) (v : ↑unitInterval) {t : ℝ} (hl : ↑(P.point i.castSucc) < t) (hr : t < ↑(P.point i.succ)) : deriv ((gluing P C).cdfSection v) t = deriv ((C i).cdfSection v) ((t - ↑(P.point i.castSucc)) / P.width i)

Inside the i-th strip, ∂₁C(t, v) = ∂₁Cᵢ((t - aᵢ₋₁)/pᵢ, v) for the glued copula.