← Mathematical handbook

Explicit counterexamples in Section 4.1

theorem Papers.Rockel2025Approximation.example43 : Verification.ApproximationExamples.lowerMatrix.checkerboard.IsSI ∧ Verification.ApproximationExamples.lowerMatrix.checkerboard.chatterjeeXi = 1 / 16 ∧ (Verification.ApproximationExamples.lowerMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkerboard.chatterjeeXi = 1 / 8 ∧ Verification.ApproximationExamples.lowerMatrix.checkerboard.chatterjeeXi < (Verification.ApproximationExamples.lowerMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkerboard.chatterjeeXi

theorem Papers.Rockel2025Approximation.example44 : Verification.ApproximationExamples.upperMatrix.checkerboard.HasMTP2Density ∧ Verification.ApproximationExamples.upperMatrix.checkerboard.chatterjeeXi = 5 / 8 ∧ (Verification.ApproximationExamples.upperMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkMin.chatterjeeXi = 7 / 16 ∧ (Verification.ApproximationExamples.upperMatrix.checkerboard.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkMin.chatterjeeXi < Verification.ApproximationExamples.upperMatrix.checkerboard.chatterjeeXi

theorem Papers.Rockel2025Approximation.permutation_counterexample : Verification.ApproximationExamples.shuffleMatrix.checkMin.chatterjeeXi = 1 ∧ (Verification.ApproximationExamples.shuffleMatrix.checkMin.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform 2 ⋯)).checkMin.chatterjeeXi = 1 / 4