Quadratic Channel Zero At Linear

theorem proved Curvature Roles

Documentation

Lean 4 Proof

theorem quadratic_channel_zero_at_linear (hJ : 2 ≤ J) :
    curvatureK J 1 = 0 := curvatureK_eq_zero_of_rho_one

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:92

Module Section

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

In the same file

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