Detection Threshold RHS

def proved Curvature Roles

Lean 4 Proof

def detectionThresholdRHS (J : ℕ) (m : EquicorrModel) : ℝ :=
  Real.sqrt (2 * (1 + m.r * (↑J - 1)) / ↑J)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:116

Module Section

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

In the same file

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