Documentation

Lean 4 Proof

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

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:274

Module Section

Information Geometry of CES:

In the same file