Documentation

Lean 4 Proof

theorem two_period_overinvestment {V c : ℝ} {N : ℕ}
    (hV : 0 < V) (_hc : 0 < c) (_hN : 2 ≤ N) :
    c / ↑N < V / ↑N → c / ↑N < V := by
  intro h
  have hN_ge1 : (1 : ℝ) ≤ ↑N := by exact_mod_cast (by omega : 1 ≤ N)
  calc c / ↑N < V / ↑N := h
    _ ≤ V := div_le_self (le_of_lt hV) hN_ge1

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:176

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file