Sections / Section 17: Welfare, Trade, Applications / gcFunction

Gc Function

defprovedCurvature Roles

Documentation

Lean 4 Proof

def gcFunction (gamma : ℝ) (phi : ℝ) : ℝ :=
  phi * (1 - Real.exp (-gamma * phi))

Dependency Graph

Used by

gc_trivial_solution

Location

thesis/CESProofs/Applications/AITransition.lean:88

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file

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