Documentation

Lean 4 Proof

theorem deviationGain_eq_K (hJ : 2 ≤ J) (ρ c : ℝ)
    (hc : c ≠ 0) :
    deviationGain J ρ c =
      curvatureK J ρ / (2 * (↑J - 1) * c) := by
  simp only [deviationGain, 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/GameTheory.lean:267

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file