← Mathematical handbook

theorem Verification.patchworkRow_independence {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (i : Fin m) (v : ↑unitInterval) : patchworkRow A (fun (x : Fin m) (x_1 : Fin n) => ProbabilityTheory.Copula.independence 2) i v =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => checkerboardRow A i v

theorem Verification.checkerboard_conditional_energy {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (v : ↑unitInterval) : ∫ (u : ↑unitInterval), A.checkerboard.conditionalCDF u v ^ 2 = ∑ i : Fin m, P.width i * checkerboardRow A i v ^ 2

noncomputable def Verification.conditionalEnergy (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : ℝ

Equations

• Verification.conditionalEnergy C v = ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2

theorem Verification.conditionalEnergy_measurable (C : ProbabilityTheory.Copula 2) : Measurable (conditionalEnergy C)

theorem Verification.conditionalEnergy_mem (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : conditionalEnergy C v ∈ Set.Icc 0 1

theorem Verification.conditionalEnergy_integrable_comp (C : ProbabilityTheory.Copula 2) {f : ↑unitInterval → ↑unitInterval} (hf : Measurable f) : MeasureTheory.Integrable (fun (v : ↑unitInterval) => conditionalEnergy C (f v)) MeasureTheory.volume