← Mathematical handbook

noncomputable def Verification.finiteSampleCDF {n : ℕ} (x : Fin n → Fin 2 → ↑unitInterval) (t : Fin 2 → ↑unitInterval) : ℝ

Equations

• Verification.finiteSampleCDF x t = 1 / ↑n * ∑ k : Fin n, Verification.lowerCubeIndicator t (x k)

theorem Verification.finiteSampleCDF_eq_empirical {Ω : Type u_1} (X : ℕ → Ω → Fin 2 → ↑unitInterval) (n : ℕ) (ω : Ω) (t : Fin 2 → ↑unitInterval) : finiteSampleCDF (fun (k : Fin n) => X (↑k) ω) t = empiricalCopulaCDF X n ω t

theorem Verification.lowerCubeIndicator_two (x : Fin 2 → ↑unitInterval) (u v : ↑unitInterval) : lowerCubeIndicator ![u, v] x = if x 0 ≤ u ∧ x 1 ≤ v then 1 else 0

theorem Verification.rankCopula_cdf_grid (n : ℕ) (hn : 0 < n) (rx ry : Equiv.Perm (Fin n)) (x : Fin n → Fin 2 → ↑unitInterval) (i j : Fin (n + 1)) (u v : ↑unitInterval) (hx : ∀ (k : Fin n), x k 0 ≤ u ↔ ↑(rx k) < ↑i) (hy : ∀ (k : Fin n), x k 1 ≤ v ↔ ↑(ry k) < ↑j) : (rankCopula n hn rx ry).cdf ![(ProbabilityTheory.Copula.IntervalPartition.uniform n hn).point i, (ProbabilityTheory.Copula.IntervalPartition.uniform n hn).point j] = finiteSampleCDF x ![u, v]

Exact link between rank-grid CDF values and empirical order-statistic thresholds.

theorem Verification.rankCopula_cdf_error (n : ℕ) (hn : 0 < n) (rx ry : Equiv.Perm (Fin n)) (x : Fin n → Fin 2 → ↑unitInterval) (hx : ∀ (k l : Fin n), x k 0 ≤ x l 0 ↔ rx k ≤ rx l) (hy : ∀ (k l : Fin n), x k 1 ≤ x l 1 ↔ ry k ≤ ry l) (C : ProbabilityTheory.Copula 2) (δ : ℝ) (hδ : 0 ≤ δ) (hCDF : ∀ (u v : ↑unitInterval), |finiteSampleCDF x ![u, v] - C.cdf ![u, v]| ≤ δ) (u v : ↑unitInterval) : |(rankCopula n hn rx ry).cdf ![u, v] - C.cdf ![u, v]| ≤ 3 * δ + 2 / ↑n

Rank transformation preserves uniform CDF approximation, up to the fine-grid mesh.