CES Eigenvalue Perp Sq

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem cesEigenvaluePerp_sq (J : ℕ) (ρ c : ℝ) :
    cesEigenvaluePerp J ρ c ^ 2 = (1 - ρ) ^ 2 / ((↑J) ^ 2 * c ^ 2) := by
  simp only [cesEigenvaluePerp]; ring

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:153

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 detectionThresholdRHS detection_achievable eigenvaluePerp_sq_proportional_to_K_sq quadratic_fisher_info_scales