Documentation

Lean 4 Proof

theorem cramerRao_diverges_at_symmetry [NeZero J]
    {c : ℝ} (hc : 0 < c) (ρ : ℝ) (N : ℕ) (_hN : 0 < N) :
    cramerRaoBound N (fun _ : Fin J => c) ρ =
    1 / (↑N * 0) := by
  simp only [cramerRaoBound, fisherInfoRho,
             escort_fisher_zero_at_symmetry hc]

Dependency Graph

Location

thesis/CESProofs/Foundations/CESEstimation.lean:154

Module Section

CES Estimation Theory: Connecting Theory to Data

In the same file