← Copula mathematical handbook

Finite patchworks with uniform marginals

Nonnegative weighted local copulas remain two-increasing after monotone coordinate changes. The two weighted marginal identities are exactly what is needed to obtain a copula. This is shared by finite ordinal sums, checkerboards, check-min copulas and shuffles.

structure ProbabilityTheory.Copula.PatchworkData (ι : Type u_2) [Fintype ι] : Type u_2

Finite local copulas with monotone coordinates and uniform weighted marginals.

• weight : ι → ℝ
• nonneg (i : ι) : 0 ≤ self.weight i
• first : ι → ↑unitInterval → ↑unitInterval
• second : ι → ↑unitInterval → ↑unitInterval
• first_mono (i : ι) : Monotone (self.first i)
• second_mono (i : ι) : Monotone (self.second i)
• first_zero (i : ι) : self.first i 0 = 0
• second_zero (i : ι) : self.second i 0 = 0
• first_one (i : ι) : self.first i 1 = 1
• second_one (i : ι) : self.second i 1 = 1
• first_margin (u : ↑unitInterval) : ∑ i : ι, self.weight i * ↑(self.first i u) = ↑u
• second_margin (v : ↑unitInterval) : ∑ i : ι, self.weight i * ↑(self.second i v) = ↑v

noncomputable def ProbabilityTheory.Copula.PatchworkData.cdf {ι : Type u_1} [Fintype ι] (P : PatchworkData ι) (C : ι → Copula 2) (u v : ↑unitInterval) : ℝ

Weighted CDF of the local copulas.

Equations

• P.cdf C u v = ∑ i : ι, P.weight i * (C i).cdf ![P.first i u, P.second i v]

theorem ProbabilityTheory.Copula.PatchworkData.isClassical {ι : Type u_1} [Fintype ι] (P : PatchworkData ι) (C : ι → Copula 2) : IsClassical fun (u : Fin 2 → ↑unitInterval) => P.cdf C (u 0) (u 1)

noncomputable def ProbabilityTheory.Copula.PatchworkData.copula {ι : Type u_1} [Fintype ι] (P : PatchworkData ι) (C : ι → Copula 2) : Copula 2

Assemble a finite patchwork as a probability-measure copula.

Equations

• P.copula C = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => P.cdf C (u 0) (u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.PatchworkData.cdf_copula {ι : Type u_1} [Fintype ι] (P : PatchworkData ι) (C : ι → Copula 2) (u : Fin 2 → ↑unitInterval) : (P.copula C).cdf u = P.cdf C (u 0) (u 1)

theorem ProbabilityTheory.Copula.PatchworkData.cdf_mono {ι : Type u_1} [Fintype ι] (P : PatchworkData ι) (C D : ι → Copula 2) (h : ∀ (i : ι) (u : Fin 2 → ↑unitInterval), (C i).cdf u ≤ (D i).cdf u) (u v : ↑unitInterval) : P.cdf C u v ≤ P.cdf D u v

Pointwise order of the local copulas passes to the patchwork.