Documentation

Lean 4 Proof

theorem diversity_encoding (hJ : 2 ≤ J) {ρ : ℝ} (hρ : ρ < 1)
    (m : EquicorrModel) :
    -- The second-order correction to E[F(X)] is:
    -- -(K/(2c)) · τ²(1-r) = cesEigenvaluePerp J ρ c · (J-1)/J · τ²(1-r) / 2
    let correction := -(curvatureK J ρ) / (2 * m.c) * m.idioVar
    -- This equals the trace of H · Σ restricted to 1⊥, divided by 2
    correction = cesEigenvaluePerp J ρ m.c * (↑J - 1) * m.idioVar / 2 := by
  simp only [curvatureK, cesEigenvaluePerp, EquicorrModel.idioVar]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hcne : m.c ≠ 0 := ne_of_gt m.hc
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:62

Module Section

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

In the same file