Fisher Info 2

def proved Curvature Roles

Lean 4 Proof

def fisherInfo2 (J : ℕ) (m : EquicorrModel) : ℝ :=
  (↑J - 1) / (2 * m.c ^ 2)

Dependency Graph

Used by

quadratic_fisher_info_scales

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:88

Module Section

Correlation robustness of CES (Paper 1, Section 7):

In the same file

EquicorrModel EquicorrModel.γ EquicorrModel.idioVar diversity_encoding fisherInfo1 quadratic_channel_zero_at_linear quadratic_channel_present detectionThresholdLHS detectionThresholdRHS detection_achievable cesEigenvaluePerp_sq eigenvaluePerp_sq_proportional_to_K_sq quadratic_fisher_info_scales