Documentation

Lean 4 Proof

theorem phieff_exceeds_phi0 {phi_0 beta_auto : ℝ}
    (hphi : 0 < phi_0) (hbeta : 0 < beta_auto)
    (hprod : beta_auto * phi_0 < 1) :
    phi_0 < effectiveTrainingProductivity phi_0 beta_auto := by
  unfold effectiveTrainingProductivity
  have hdenom_pos : 0 < 1 - beta_auto * phi_0 := by linarith
  rw [lt_div_iff₀ hdenom_pos]
  have : 0 < beta_auto * phi_0 := mul_pos hbeta hphi
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:54

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file