← Mathematical handbook

theorem Verification.uniform_coord_lower (m : ℕ) (i : Fin (m + 1)) (t : ↑unitInterval) (ht : ↑t ≤ 1 / (↑m + 1)) : ↑((ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯).coord i t) = if i = 0 then (↑m + 1) * ↑t else 0

theorem Verification.uniform_coord_upper (m : ℕ) (i : Fin (m + 1)) (t : ↑unitInterval) (ht : ↑t ≤ 1 / (↑m + 1)) : 1 - ↑((ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯).coord i (unitInterval.symm t)) = if i = Fin.last m then (↑m + 1) * ↑t else 0