← Mathematical handbook

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

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

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

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

Equations

• Verification.cellPrefix A i j = ∑ s : Fin n, if s < j then A.mass i s else 0

theorem Verification.patchworkRow_embed {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (C : Fin m → Fin n → ProbabilityTheory.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