← Mathematical handbook

noncomputable def Verification.empiricalCDFRadius (n : ℕ) : ℝ

Equations

• Verification.empiricalCDFRadius n = √(8 * Real.log (↑n + 2) / (↑n + 1))

theorem Verification.empiricalCDFRadius_nonneg (n : ℕ) : 0 ≤ empiricalCDFRadius n

theorem Verification.empiricalCDFRadius_exp (n : ℕ) : (↑n + 2) ^ 2 * 2 * Real.exp (-(↑n + 1) * empiricalCDFRadius n ^ 2 / 2) = 2 / (↑n + 2) ^ 2

theorem Verification.empiricalCDFRadius_summable : Summable fun (n : ℕ) => 2 / (↑n + 2) ^ 2

theorem Verification.empiricalCopulaCDF_ae_rate {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (C : ProbabilityTheory.Copula 2) (X : ℕ → Ω → Fin 2 → ↑unitInterval) (hX : ∀ (i : ℕ), Measurable (X i)) (hI : ProbabilityTheory.iIndepFun X μ) (hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (X i) μ = C.toMeasure) : ∀ᵐ (ω : Ω) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (u v : ↑unitInterval), |empiricalCopulaCDF X (n + 1) ω ![u, v] - C.cdf ![u, v]| ≤ empiricalCDFRadius n + 2 / (↑n + 1)

Uniform empirical CDF control almost surely, obtained from a growing finite grid, Hoeffding's inequality and Borel-Cantelli. No empirical convergence is assumed.