Documentation

Lean 4 Proof

theorem baumol_bounded_below {beta_Z g_C g_Z : ℝ}
    (_hbeta : 0 ≤ beta_Z) (_hbeta1 : beta_Z ≤ 1) (hgZ_le : g_Z ≤ g_C) :
    g_Z ≤ baumolGrowthRate beta_Z g_C g_Z := by
  unfold baumolGrowthRate; nlinarith

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:140

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file