Documentation

Lean 4 Proof

theorem amplification_diverges {M : ℝ} (hM : 0 < M) :
    ∃ ρ : ℝ, 1 < ρ ∧ M < amplificationExponent ρ := by
  use 1 + 1 / (M + 1)
  constructor
  · linarith [div_pos one_pos (by linarith : (0:ℝ) < M + 1)]
  · unfold amplificationExponent
    rw [show 1 + 1 / (M + 1) - 1 = 1 / (M + 1) from by ring]
    rw [one_div, one_div, inv_inv]
    linarith

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:358

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file