← Mathematical handbook

noncomputable def Verification.lowerCubeIndicator (t : Fin 2 → ↑unitInterval) : (Fin 2 → ↑unitInterval) → ℝ

Equations

• Verification.lowerCubeIndicator t = (Set.Iic t).indicator fun (x : Fin 2 → ↑unitInterval) => 1

theorem Verification.lowerCubeIndicator_measurable (t : Fin 2 → ↑unitInterval) : Measurable (lowerCubeIndicator t)

theorem Verification.lowerCubeIndicator_mem (t x : Fin 2 → ↑unitInterval) : lowerCubeIndicator t x ∈ Set.Icc 0 1

theorem Verification.lowerCubeIndicator_mono {s t : Fin 2 → ↑unitInterval} (hst : s ≤ t) (x : Fin 2 → ↑unitInterval) : lowerCubeIndicator s x ≤ lowerCubeIndicator t x

noncomputable def Verification.empiricalCopulaCDF {Ω : Type u_1} (X : ℕ → Ω → Fin 2 → ↑unitInterval) (n : ℕ) (ω : Ω) (t : Fin 2 → ↑unitInterval) : ℝ

Equations

• Verification.empiricalCopulaCDF X n ω t = Verification.empiricalMean (fun (i : ℕ) (ω : Ω) => Verification.lowerCubeIndicator t (X i ω)) n ω

theorem Verification.empiricalCopulaCDF_mono {Ω : Type u_1} (X : ℕ → Ω → Fin 2 → ↑unitInterval) (n : ℕ) (ω : Ω) : Monotone (empiricalCopulaCDF X n ω)

theorem Verification.lowerCubeIndicator_mean {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (C : ProbabilityTheory.Copula 2) (X : Ω → Fin 2 → ↑unitInterval) (hX : Measurable X) (hlaw : MeasureTheory.Measure.map X μ = C.toMeasure) (t : Fin 2 → ↑unitInterval) : ∫ (ω : Ω), lowerCubeIndicator t (X ω) ∂μ = C.cdf t

theorem Verification.empiricalCopulaCDF_grid_deviation {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] (μ : 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) (grid : ι → Fin 2 → ↑unitInterval) (n : ℕ) (hn : 0 < n) (ε : ℝ) (hε : 0 ≤ ε) : μ.real {ω : Ω | ∃ (t : ι), ε ≤ |empiricalCopulaCDF X n ω (grid t) - C.cdf (grid t)|} ≤ ↑(Fintype.card ι) * 2 * Real.exp (-↑n * ε ^ 2 / 2)

theorem Verification.cdf_grid_error_bound {m n : ℕ} (C : ProbabilityTheory.Copula 2) (F : (Fin 2 → ↑unitInterval) → ℝ) (hF : Monotone F) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (ε dx dy : ℝ) (hx : ∀ (i : Fin m), P.width i ≤ dx) (hy : ∀ (j : Fin n), Q.width j ≤ dy) (hgrid : ∀ (i : Fin (m + 1)) (j : Fin (n + 1)), |F ![P.point i, Q.point j] - C.cdf ![P.point i, Q.point j]| ≤ ε) (u v : ↑unitInterval) : |F ![u, v] - C.cdf ![u, v]| ≤ ε + dx + dy

Monotonicity extends a finite-grid CDF error bound to the whole square.