Documentation

Lean 4 Proof

theorem estimation_precision_bridge {J : ℕ} (hJ : 2 ≤ J)
    {ρ : ℝ} (_hρ : ρ < 1) (hρ0 : ρ ≠ 0) {c : ℝ} (hc : 0 < c) :
    -- K decomposes as bridge × geometry × Fisher
    curvatureK J ρ =
      bridgeRatio ρ * (↑J - 1) * c ^ 2 *
        escortFisherEigenvalue J ρ c :=
  curvatureK_eq_bridge_times_fisher hρ0 hc.ne'
    (Nat.cast_ne_zero.mpr (by omega))

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:318

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file