Documentation

Lean 4 Proof

theorem amplification_pos {ρ : ℝ} (hρ : 1 < ρ) :
    0 < amplificationExponent ρ :=
  div_pos one_pos (by linarith)

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/GameTheory.lean:348

Module Section

Multi-Agent CES Game Theory (Gap #14)

In the same file