← Mathematical handbook

noncomputable def Verification.checkerboardDensity {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.checkerboardDensity_measurable {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) : Measurable (checkerboardDensity A)

theorem Verification.checkerboardDensity_nonneg {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (x : Fin 2 → ↑unitInterval) : 0 ≤ checkerboardDensity A x

theorem Verification.checkerboardDensity_term_integrable {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (i : Fin m) (j : Fin n) : MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => A.mass i j / (P.width i * Q.width j) * (partitionPiece P i (fun (x : ↑unitInterval) => 1) (x 0) * partitionPiece Q j (fun (x : ↑unitInterval) => 1) (x 1))) MeasureTheory.volume

theorem Verification.checkerboardDensity_integrable {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) : MeasureTheory.Integrable (checkerboardDensity A) MeasureTheory.volume

theorem Verification.checkerboardDensity_integral_Iic {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (u : Fin 2 → ↑unitInterval) : ∫ (x : Fin 2 → ↑unitInterval) in Set.Iic u, checkerboardDensity A x = A.checkerboard.cdf u

theorem Verification.checkerboard_toMeasure_density {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) : A.checkerboard.toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (checkerboardDensity A x)