← Copula mathematical handbook

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

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

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

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

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

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rowMeanXi P C = (6 * ∫ (v : ↑unitInterval), ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rowMeanEnergy P C v) - 2

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

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rowMeanXi_tendsto_of_cdf {m : ℕ} (P : IntervalPartition m) (C : ℕ → Copula 2) (D : 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 ProbabilityTheory.Copula.RankRegion.XiBlest.Support.xi_le_limit_of_cdf (C : ℕ → Copula 2) (D : 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.