← Mathematical handbook

theorem Verification.rectangular_checkerboard_lower_tail {m n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : A.checkerboard.HasLowerTailDependence 0

theorem Verification.rectangular_checkMin_lower_tail {m n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : A.checkMin.HasLowerTailDependence (A.mass 0 0 * min (↑m + 1) (↑n + 1))

theorem Verification.rectangular_checkW_lower_tail {m n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : A.checkW.HasLowerTailDependence 0

theorem Verification.rectangular_checkerboard_upper_tail {m n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : A.checkerboard.HasUpperTailDependence 0

theorem Verification.rectangular_checkMin_upper_tail {m n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : A.checkMin.HasUpperTailDependence (A.mass (Fin.last m) (Fin.last n) * min (↑m + 1) (↑n + 1))

theorem Verification.rectangular_checkW_upper_tail {m n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : A.checkW.HasUpperTailDependence 0