← Copula mathematical handbook

Finite ordinal sums on arbitrary interval partitions

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

Ordered diagonal blocks associated with a finite interval partition.

Equations

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

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

A finite ordinal sum with arbitrary positive block lengths and local copulas.

Equations

• ProbabilityTheory.Copula.finiteOrdinalSum P C = P.ordinalData.copula C

@[simp]

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

noncomputable def ProbabilityTheory.Copula.ordinalSumPi {n : ℕ} (P : IntervalPartition n) : Copula 2

Finite ordinal sum of copies of the independence copula Π.

Equations

• ProbabilityTheory.Copula.ordinalSumPi P = ProbabilityTheory.Copula.finiteOrdinalSum P fun (x : Fin n) => ProbabilityTheory.Copula.independence 2

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

@[simp]

theorem ProbabilityTheory.Copula.finiteOrdinalSum_comonotonic {n : ℕ} (P : IntervalPartition n) : (finiteOrdinalSum P fun (x : Fin n) => comonotonic 2) = comonotonic 2

Any finite ordinal sum of copies of M is M.

def ProbabilityTheory.Copula.IntervalPartition.binary (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : IntervalPartition 2

A two-cell partition at an interior split.

Equations

• ProbabilityTheory.Copula.IntervalPartition.binary a ha0 ha1 = { point := ![0, a, 1], strictMono := ⋯, zero := ⋯, one := ⋯ }

theorem ProbabilityTheory.Copula.finiteOrdinalSum_binary (C D : Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : finiteOrdinalSum (IntervalPartition.binary a ha0 ha1) ![C, D] = C.ordinalSum D a

The finite construction agrees with the existing binary ordinal-sum API.