Baumol Growth Rate

def proved Curvature Roles

Documentation

Lean 4 Proof

def baumolGrowthRate (beta_Z g_C g_Z : ℝ) : ℝ :=
  (1 - beta_Z) * g_C + beta_Z * g_Z

Dependency Graph

Used by

baumol_limit baumol_bounded_below

Location

thesis/CESProofs/Applications/AITransition.lean:129

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file

effectiveTrainingProductivity phieff_exceeds_phi0 phieff_ge_one_condition gcFunction gc_trivial_solution adoptionR0 adoption_threshold baumol_limit baumol_bounded_below singularityTime singularity_time_pos two_period_overinvestment saturation_escape_rate effectiveAlpha_monotone_J collapse_at_J1 crossing_threshold_reexport