← Mathematical handbook

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

Equations

• Verification.patchworkRowEnergy A C i v = ∫ (u : ↑unitInterval), Verification.patchworkRow A C i v u ^ 2

theorem Verification.patchworkRowEnergy_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 (patchworkRowEnergy A C i)

theorem Verification.patchworkRowEnergy_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 : ↑unitInterval) : patchworkRowEnergy A C i v ∈ Set.Icc 0 1

theorem Verification.patchworkRowEnergy_integrable_comp {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) {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => patchworkRowEnergy A C i (f v)) MeasureTheory.volume

theorem Verification.patchworkRowEnergy_integral {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), patchworkRowEnergy A C i v = ∑ j : Fin n, Q.width j * ((cellPrefix A i j / P.width i) ^ 2 + cellPrefix A i j / P.width i * (A.mass i j / P.width i) + (A.mass i j / P.width i) ^ 2 * ((C i j).chatterjeeXi + 2) / 6)

theorem Verification.patchwork_xi_formula {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).chatterjeeXi = 6 * ∑ i : Fin m, P.width i * ∑ j : Fin n, Q.width j * ((cellPrefix A i j / P.width i) ^ 2 + cellPrefix A i j / P.width i * (A.mass i j / P.width i) + (A.mass i j / P.width i) ^ 2 * ((C i j).chatterjeeXi + 2) / 6) - 2

theorem Verification.patchwork_xi_correction {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).chatterjeeXi = A.checkerboard.chatterjeeXi + ∑ i : Fin m, ∑ j : Fin n, Q.width j / P.width i * A.mass i j ^ 2 * (C i j).chatterjeeXi