← Mathematical handbook

noncomputable def Verification.patchworkLaw {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) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

The patchwork is a weighted sum of affine images of the actual local copula laws.

Equations

• Verification.patchworkLaw A C = ∑ i : Fin m, ∑ j : Fin n, ENNReal.ofReal (A.mass i j) • Verification.partitionCellLaw P Q i j (C i j)

instance Verification.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalHSMulENNRealMeasureOfRealMassPartitionCellLaw {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) : MeasureTheory.IsFiniteMeasure (ENNReal.ofReal (A.mass i j) • partitionCellLaw P Q i j (C i j))

instance Verification.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalPatchworkLaw {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) : MeasureTheory.IsFiniteMeasure (patchworkLaw A C)

instance Verification.instIsProbabilityMeasureForallFinOfNatNatElemRealUnitIntervalPatchworkLaw {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) : MeasureTheory.IsProbabilityMeasure (patchworkLaw A C)

theorem Verification.patchworkLaw_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) (u : Fin 2 → ↑unitInterval) : (patchworkLaw A C) (Set.Iic u) = ENNReal.ofReal ((A.patchwork C).cdf u)

theorem Verification.toMeasure_patchworkLaw {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) : (A.patchwork C).toMeasure = patchworkLaw A C

theorem Verification.integral_patchwork {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) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(A.patchwork C).toMeasure = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * ∫ (x : Fin 2 → ↑unitInterval), f (partitionCellMap P Q i j x) ∂(C i j).toMeasure