Sections / Section 3: Sextuple Role of Curvature K / EquicorrModel

Equicorr Model

structureprovedCurvature Roles

Documentation

Lean 4 Proof

structure EquicorrModel where
  c : ℝ  -- mean level (symmetric point)
  τ : ℝ  -- standard deviation
  r : ℝ  -- equicorrelation parameter
  hc : 0 < c
  hτ : 0 < τ
  hr_ge : 0 ≤ r
  hr_lt : r < 1

Dependency Graph

Used by

fisherInfo2 detectionThresholdRHS diversity_encoding fisherInfo1 EquicorrModel.idioVar SextupleRoleStatement EquicorrModel.γ detectionThresholdLHS quadratic_fisher_info_scales

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:23

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