Documentation

Lean 4 Proof

theorem effectiveAlpha_monotone_J {rho : ℝ} {J1 J2 : ℕ}
    (hrho_pos : 0 < rho) (hrho_lt : rho < 1)
    (_hJ1 : 1 ≤ J1) (_hJ2 : 1 ≤ J2) (hJ : J1 ≤ J2) :
    (1 - rho) / rho * ((↑J1 - 1) / ↑J1) ≤
    (1 - rho) / rho * ((↑J2 - 1) / ↑J2) := by
  apply mul_le_mul_of_nonneg_left _ (div_nonneg (by linarith) (le_of_lt hrho_pos))
  have hJ1_pos : (0 : ℝ) < ↑J1 := by positivity
  have hJ2_pos : (0 : ℝ) < ↑J2 := by positivity
  rw [div_le_div_iff₀ hJ1_pos hJ2_pos]
  have hJ_cast : (↑J1 : ℝ) ≤ ↑J2 := Nat.cast_le.mpr hJ
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Applications/AITransition.lean:211

Module Section

Paper 6: Endogenous Decentralization and the AI Transition

In the same file