← Mathematical handbook

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

Equations

• Verification.rowMeanEnergy P C v = ∑ i : Fin n, P.width i * Verification.copulaRowMean P C i v ^ 2

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

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

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