Documentation

Lean 4 Proof

theorem escort_fisher_zero_at_symmetry [NeZero J]
    {c₀ : ℝ} (hc : 0 < c₀) (ρ : ℝ) :
    escortVariance (fun _ : Fin J => c₀) ρ
      (fun _ => Real.log c₀) = 0 :=
  escort_variance_const _ (fun _ => hc) ρ (Real.log c₀)

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/InformationGeometry.lean:990

Module Section

### Part F: The Dual Curvature Principle

In the same file