← Mathematical handbook

noncomputable def Verification.patchworkRow {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) : ℝ

Equations

• Verification.patchworkRow A C i v u = ∑ j : Fin n, A.mass i j / P.width i * Verification.normalizedCDF (C i j) u (Q.coord j v)

noncomputable def Verification.patchworkKernel {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) (v u : ↑unitInterval) : ℝ

Equations

• Verification.patchworkKernel A C v u = ∑ i : Fin m, Verification.partitionPiece P i (Verification.patchworkRow A C i v) u

theorem Verification.patchworkRow_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) (v : ↑unitInterval) : Measurable (patchworkRow A C i v)

theorem Verification.patchworkRow_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 (patchworkRow A C i v) MeasureTheory.volume

theorem Verification.patchworkKernel_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) (v : ↑unitInterval) : MeasureTheory.Integrable (patchworkKernel A C v) MeasureTheory.volume

theorem Verification.patchworkKernel_nonneg {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) (v u : ↑unitInterval) : 0 ≤ patchworkKernel A C v u

theorem Verification.integral_patchworkRow_Iic {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 t : ↑unitInterval) : ∫ (u : ↑unitInterval) in Set.Iic t, patchworkRow A C i v u = ∑ j : Fin n, A.mass i j / P.width i * (C i j).cdf ![t, Q.coord j v]

theorem Verification.patchwork_conditionalCDF {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) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (A.patchwork C).conditionalCDF u v) =ᵐ[MeasureTheory.volume] patchworkKernel A C v