← Mathematical handbook

theorem Verification.normalizedCDF_affine_energy (C : ProbabilityTheory.Copula 2) (a b : ℝ) : ∫ (v : ↑unitInterval) (u : ↑unitInterval), (a + b * normalizedCDF C u v) ^ 2 = a ^ 2 + a * b + b ^ 2 * (C.chatterjeeXi + 2) / 6

theorem Verification.conditional_energy_lt_of_local_deriv (C : ProbabilityTheory.Copula 2) (v q : ↑unitInterval) (g : ↑unitInterval → ℝ) (hg : ContinuousAt g q) (hd : ∀ᶠ (u : ↑unitInterval) in nhds q, HasDerivAt (C.cdfSection v) (g u) ↑u) (h0 : 0 < g q) (h1 : g q < 1) : ∫ (u : ↑unitInterval), C.conditionalCDF u v ^ 2 < ↑v

A locally continuous conditional probability strictly between zero and one prevents maximal conditional energy at this threshold.