← Mathematical handbook

theorem Verification.uniform_coord_lower_eq (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 (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯).coord 0 t else 0

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

theorem Verification.uniform_patchwork_lower_corner {m n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) (C : Fin (m + 1) → Fin (n + 1) → ProbabilityTheory.Copula 2) (t : ↑unitInterval) (hm : ↑t ≤ 1 / (↑m + 1)) (hn : ↑t ≤ 1 / (↑n + 1)) : (A.patchwork C).diagonal t = A.mass 0 0 * (C 0 0).cdf ![(ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯).coord 0 t, (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯).coord 0 t]

theorem Verification.survival_two_one_left (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : C.survival ![1, v] = 0

theorem Verification.survival_two_one_right (C : ProbabilityTheory.Copula 2) (u : ↑unitInterval) : C.survival ![u, 1] = 0

theorem Verification.uniform_patchwork_upper_corner {m n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) (C : Fin (m + 1) → Fin (n + 1) → ProbabilityTheory.Copula 2) (t : ↑unitInterval) (hm : ↑t ≤ 1 / (↑m + 1)) (hn : ↑t ≤ 1 / (↑n + 1)) : (A.patchwork C).survival ![unitInterval.symm t, unitInterval.symm t] = A.mass (Fin.last m) (Fin.last n) * (C (Fin.last m) (Fin.last n)).survival ![(ProbabilityTheory.Copula.IntervalPartition.uniform (m + 1) ⋯).coord (Fin.last m) (unitInterval.symm t), (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯).coord (Fin.last n) (unitInterval.symm t)]