← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rowMeanEnergy {n : ℕ} (P : IntervalPartition n) (C : Copula 2) (v : ↑unitInterval) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rowMeanEnergy P C v = ∑ i : Fin n, P.width i * ProbabilityTheory.Copula.RankRegion.XiBlest.Support.copulaRowMean P C i v ^ 2

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.copulaRowMean_mem {n : ℕ} (P : IntervalPartition n) (C : Copula 2) (i : Fin n) (v : ↑unitInterval) : copulaRowMean P C i v ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rowMeanEnergy_error {n : ℕ} (P : IntervalPartition n) (C : Copula 2) (v : ↑unitInterval) : conditionalEnergy C v - rowMeanEnergy P C v ≤ 2 * partitionAverageError P fun (u : ↑unitInterval) => C.conditionalCDF u v

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.rowMeanEnergy_tendsto (C : Copula 2) (v : ↑unitInterval) : Filter.Tendsto (fun (k : ℕ) => rowMeanEnergy (IntervalPartition.uniform (k + 1) ⋯) C v) Filter.atTop (nhds (conditionalEnergy C v))