Equicorr Model Idio VAR

def proved Curvature Roles

Documentation

Lean 4 Proof

def EquicorrModel.idioVar (m : EquicorrModel) : ℝ := m.τ ^ 2 * (1 - m.r)

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:36

Module Section

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

In the same file

EquicorrModel EquicorrModel.γ 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