Documentation

Lean 4 Proof

def fisherInfo1 (J : ℕ) (m : EquicorrModel) : ℝ :=
  ↑J / (m.τ ^ 2 * (1 + m.r * (↑J - 1)))

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:85

Module Section

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

In the same file