← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRowEnergy {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) (v : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRowEnergy A C i v = ∫ (u : ↑unitInterval), ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRow A C i v u ^ 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRowEnergy_measurable {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (i : Fin m) : Measurable (patchworkRowEnergy A C i)

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRowEnergy_integrable_comp {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchworkRowEnergy_integral {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchwork_xi_formula {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.patchwork_xi_correction {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → 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