Documentation

Lean 4 Proof

theorem fisherInfoRho_zero_at_symmetry [NeZero J]
    {c : ℝ} (hc : 0 < c) (ρ : ℝ) :
    fisherInfoRho (fun _ : Fin J => c) ρ = 0 :=
  escort_fisher_zero_at_symmetry hc ρ

Dependency Graph

Used by

Location

thesis/CESProofs/Foundations/CESEstimation.lean:143

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file