Documentation

Lean 4 Proof

theorem eigenvaluePerp_sq_proportional_to_K_sq (hJ : 2 ≤ J) (ρ c : ℝ) :
    cesEigenvaluePerp J ρ c ^ 2 =
      curvatureK J ρ ^ 2 / ((↑J - 1) ^ 2 * c ^ 2) := by
  simp only [cesEigenvaluePerp, curvatureK]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  have hJm1_ne : (↑J : ℝ) - 1 ≠ 0 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
    linarith
  field_simp

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/CorrelationRobust.lean:162

Module Section

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

In the same file