← Mathematical handbook

theorem Verification.rowMeanEnergy_continuous {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ProbabilityTheory.Copula 2) : Continuous (rowMeanEnergy P C)

theorem Verification.rowMeanEnergy_mem {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) : rowMeanEnergy P C v ∈ Set.Icc 0 1

theorem Verification.rowMeanEnergy_integrable {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ProbabilityTheory.Copula 2) : MeasureTheory.Integrable (rowMeanEnergy P C) MeasureTheory.volume

noncomputable def Verification.rowMeanXi {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ProbabilityTheory.Copula 2) : ℝ

Predictor-bin averaging gives a lower approximation to xi, with no response binning.

Equations

• Verification.rowMeanXi P C = (6 * ∫ (v : ↑unitInterval), Verification.rowMeanEnergy P C v) - 2

theorem Verification.rowMeanXi_le {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ProbabilityTheory.Copula 2) : rowMeanXi P C ≤ C.chatterjeeXi

theorem Verification.rowMeanXi_tendsto (C : ProbabilityTheory.Copula 2) : Filter.Tendsto (fun (k : ℕ) => rowMeanXi (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯) C) Filter.atTop (nhds C.chatterjeeXi)

theorem Verification.rowMeanXi_tendsto_of_cdf {m : ℕ} (P : ProbabilityTheory.Copula.IntervalPartition m) (C : ℕ → ProbabilityTheory.Copula 2) (D : ProbabilityTheory.Copula 2) (hC : ∀ (u v : ↑unitInterval), Filter.Tendsto (fun (k : ℕ) => (C k).cdf ![u, v]) Filter.atTop (nhds (D.cdf ![u, v]))) : Filter.Tendsto (fun (k : ℕ) => rowMeanXi P (C k)) Filter.atTop (nhds (rowMeanXi P D))

A fixed predictor-bin energy is continuous under pointwise copula-CDF convergence.

theorem Verification.xi_le_limit_of_cdf (C : ℕ → ProbabilityTheory.Copula 2) (D : ProbabilityTheory.Copula 2) (x : ℝ) (hC : ∀ (u v : ↑unitInterval), Filter.Tendsto (fun (k : ℕ) => (C k).cdf ![u, v]) Filter.atTop (nhds (D.cdf ![u, v]))) (hx : Filter.Tendsto (fun (k : ℕ) => (C k).chatterjeeXi) Filter.atTop (nhds x)) : D.chatterjeeXi ≤ x

Xi cannot jump upward at a pointwise CDF limit. Singular copulas are included.