Documentation

Lean 4 Proof

theorem quadratic_fisher_info_scales (hJ : 2 ≤ J) (m : EquicorrModel) :
    fisherInfo2 J m * (2 * m.c ^ 2) = ↑J - 1 := by
  simp only [fisherInfo2]
  have hcne : m.c ≠ 0 := ne_of_gt m.hc
  field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:177

Module Section

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

In the same file