Documentation

Lean 4 Proof

theorem diversity_premium_monotone_J {rho : ℝ} {J1 J2 : ℕ}
    (hrho : rho < 1) (_hrho_pos : 0 < rho)
    (_hJ1 : 1 ≤ J1) (_hJ2 : 1 ≤ J2) (hJ : J1 ≤ J2) :
    (1 - rho) * ((↑J1 - 1) / ↑J1) ≤
    (1 - rho) * ((↑J2 - 1) / ↑J2) := by
  apply mul_le_mul_of_nonneg_left _ (by linarith)
  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/KnowledgeCommons.lean:63

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file