Documentation

Lean 4 Proof

theorem curvatureK_from_hessLogF {J : ℕ} (ρ c : ℝ)
    (hc : c ≠ 0) (hJ : (↑J : ℝ) ≠ 0) :
    curvatureK J ρ = -(↑J - 1) * c ^ 2 * hessLogFEigenvalue J ρ c := by
  simp only [curvatureK, hessLogFEigenvalue]
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:282

Module Section

Information Geometry of CES:

In the same file