← Mathematical handbook

noncomputable def Verification.LTDExample.thirdMatrix (p : ℝ) (hp : p ∈ Set.Icc 0 1) : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯)

Equations

• Verification.LTDExample.thirdMatrix p hp = { mass := !![1 / 3, 0, 0; 0, p / 3, (1 - p) / 3; 0, (1 - p) / 3, p / 3], nonneg := ⋯, row_sum := ⋯, col_sum := ⋯ }

theorem Verification.LTDExample.thirdMatrix_xi (p : ℝ) (hp : p ∈ Set.Icc 0 1) : (thirdMatrix p hp).checkerboard.chatterjeeXi = 4 / 9 + 2 / 9 * (1 - 2 * p) ^ 2

theorem Verification.LTDExample.thirdMatrix_diagonal_grid (p : ℝ) (hp : p ∈ Set.Icc 0 1) : (thirdMatrix p hp).checkerboard.cdf ![(ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).point 2, (ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).point 2] = (1 + p) / 3

theorem Verification.LTDExample.printedMatrix_not_ltd : ¬(thirdMatrix (1 / 4) ⋯).checkerboard.IsLTD

The matrix printed in Remark 2.6(d) fails even positive quadrant dependence.

theorem Verification.LTDExample.uniform_three_coord (i : Fin 3) (u : ↑unitInterval) : ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).coord i u) = ![3 * min (↑u) (1 / 3), 3 * (min (↑u) (2 / 3) - min (↑u) (1 / 3)), 3 * (↑u - min (↑u) (2 / 3))] i

theorem Verification.LTDExample.correctedMatrix_cdf (u v : ↑unitInterval) : (thirdMatrix (1 / 3) ⋯).checkerboard.cdf ![u, v] = ↑u * (2 * ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).coord 1 v) + ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).coord 2 v)) / 3 + min (↑u) (1 / 3) * (↑((ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).coord 0 v) - ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).coord 1 v)) + (2 * min (↑u) (1 / 3) - min (↑u) (2 / 3)) * (↑((ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).coord 1 v) - ↑((ProbabilityTheory.Copula.IntervalPartition.uniform 3 ⋯).coord 2 v)) / 3

theorem Verification.LTDExample.coord_index_antitone {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (u : ↑unitInterval) (i j : Fin n) (hij : i ≤ j) : P.coord j u ≤ P.coord i u

theorem Verification.LTDExample.correctedMatrix_ltd : (thirdMatrix (1 / 3) ⋯).checkerboard.IsLTD

A corrected matrix proving the intended strict LTD counterexample.