Documentation

Lean 4 Proof

def logCesHessianQF (J : ℕ) (ρ c : ℝ) (v : Fin J → ℝ) : ℝ :=
  (1 / c) * cesHessianQF J ρ c v - (1 / (↑J * c)) ^ 2 * (∑ j : Fin J, v j) ^ 2

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Appendix.lean:31

Module Section

Appendix Lemmas 1-3 (Paper 2, Appendix A)

In the same file