Equicorr Model Γ

def proved Curvature Roles

Documentation

Lean 4 Proof

def EquicorrModel.γ (m : EquicorrModel) : ℝ := m.τ / m.c

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:33

Module Section

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

In the same file

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