← Mathematical handbook

Continuous tests of partition-averaged conditional distributions

theorem Verification.continuous_unit_affine_modulus (φ : ℝ → ℝ) (hc : Continuous φ) {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, |φ x - φ y| ≤ ε + K * |x - y|

A continuous test on the unit interval has an affine error modulus with arbitrarily small constant term.

theorem Verification.conditionalCDF_embed_comp_integrable {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (i : Fin n) (v : ↑unitInterval) (φ : ℝ → ℝ) (hc : Continuous φ) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => φ (C.conditionalCDF (partitionEmbed P i u) v)) MeasureTheory.volume

noncomputable def Verification.rowMeanTest {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (φ : ℝ → ℝ) : ℝ

Equations

• Verification.rowMeanTest P C v φ = ∑ i : Fin n, P.width i * φ (Verification.copulaRowMean P C i v)

theorem Verification.rowMeanTest_error {n : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition n) (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (φ : ℝ → ℝ) (hc : Continuous φ) (ε K : ℝ) (hm : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, |φ x - φ y| ≤ ε + K * |x - y|) : |rowMeanTest P C v φ - ∫ (u : ↑unitInterval), φ (C.conditionalCDF u v)| ≤ ε + K * partitionAverageError P fun (u : ↑unitInterval) => C.conditionalCDF u v

theorem Verification.rowMeanTest_tendsto (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) (φ : ℝ → ℝ) (hc : Continuous φ) : Filter.Tendsto (fun (k : ℕ) => rowMeanTest (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯) C v φ) Filter.atTop (nhds (∫ (u : ↑unitInterval), φ (C.conditionalCDF u v)))