← Mathematical handbook

theorem Verification.uniform_stripCut_coord (n : ℕ) (i : Fin (n + 1)) (u : ↑unitInterval) : stripCut (1 / (↑n + 1)) (↑↑i / (↑n + 1)) ↑u = 1 / (↑n + 1) * ↑((ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯).coord i u)

theorem Verification.permutationShuffle_eq_rankCheckMin (n : ℕ) (rx ry : Equiv.Perm (Fin (n + 1))) : PermutationShuffle.copula n ((Equiv.symm rx).trans ry) = (rankCellMass (n + 1) ⋯ rx ry).checkMin

theorem Verification.rankCheckMin_cdf_error (n : ℕ) (rx ry : Equiv.Perm (Fin (n + 1))) (u v : ↑unitInterval) : |(rankCellMass (n + 1) ⋯ rx ry).checkMin.cdf ![u, v] - (rankCopula (n + 1) ⋯ rx ry).cdf ![u, v]| ≤ 2 / (↑n + 1)

theorem Verification.exists_permutationShuffle_approximation (C : ProbabilityTheory.Copula 2) : ∃ (π : (n : ℕ) → Equiv.Perm (Fin (n + 1))), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (u v : ↑unitInterval), |(PermutationShuffle.copula n (π n)).cdf ![u, v] - C.cdf ![u, v]| ≤ 3 * empiricalCDFRadius n + 10 / (↑n + 1)

A quantitative uniform approximation by actual equal-width permutation shuffles.