← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow_joint_measurable {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => patchworkRow A C i p.1 p.2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow_mem {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (v u : ↑unitInterval) : patchworkRow A C i v u ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow_sq_integrable {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (v : ↑unitInterval) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => patchworkRow A C i v u ^ 2) MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellPrefix {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (i : Fin m) (j : Fin n) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.cellPrefix A i j = ∑ s : Fin n, if s < j then A.mass i s else 0

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow_embed {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (j : Fin n) (v u : ↑unitInterval) : patchworkRow A C i (partitionEmbed Q j v) u = cellPrefix A i j / P.width i + A.mass i j / P.width i * normalizedCDF (C i j) u v