Documentation

Lean 4 Proof

theorem fifth_role_of_K (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1) (hρ0 : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c) :
    -- K is positive (economic curvature exists)
    0 < curvatureK J ρ ∧
    -- K decomposes as bridge × geometry × Fisher
    curvatureK J ρ =
      bridgeRatio ρ * (↑J - 1) * c ^ 2 * escortFisherEigenvalue J ρ c ∧
    -- The bridge theorem holds
    -hessLogFEigenvalue J ρ c =
      bridgeRatio ρ * escortFisherEigenvalue J ρ c :=
  ⟨curvatureK_pos hJ hρ,
   curvatureK_eq_bridge_times_fisher hρ0 hc.ne' (Nat.cast_ne_zero.mpr (by omega)),
   bridge_theorem hρ0 hc.ne' (Nat.cast_ne_zero.mpr (by omega))⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:319

Module Section

Information Geometry of CES:

In the same file