Documentation

Lean 4 Proof

theorem phieff_ge_one_condition {phi_0 beta_auto : ℝ}
    (_hphi : 0 < phi_0) (_hbeta : 0 < beta_auto)
    (hbeta_le : beta_auto ≤ 1)
    (hprod : beta_auto * phi_0 < 1)
    (hhalf : 1 / 2 ≤ beta_auto * phi_0) :
    1 ≤ effectiveTrainingProductivity phi_0 beta_auto := by
  unfold effectiveTrainingProductivity
  have hdenom_pos : 0 < 1 - beta_auto * phi_0 := by linarith
  rw [le_div_iff₀ hdenom_pos]
  nlinarith [mul_le_of_le_one_left (by linarith : 0 ≤ phi_0) hbeta_le]

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:70

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file