Documentation

Lean 4 Proof

theorem frontLoaded_worse_than_linear {R_0 γ φ : ℝ}
    (hR : 0 < R_0) (hγ : 0 < γ) (_hφ0 : 0 < φ) (hφ1 : φ < 1) :
    frontLoadedRevenue R_0 γ φ < R_0 * (1 - φ) := by
  unfold frontLoadedRevenue
  have h1mφ : 0 < 1 - φ := by linarith
  have key : (1 - φ) ^ γ < 1 := rpow_lt_one h1mφ.le (by linarith) hγ
  have decomp : (1 - φ) ^ (1 + γ) = (1 - φ) * (1 - φ) ^ γ := by
    rw [rpow_add h1mφ, rpow_one]
  rw [decomp]
  have : (1 - φ) * (1 - φ) ^ γ < 1 - φ := by
    calc (1 - φ) * (1 - φ) ^ γ
        < (1 - φ) * 1 := mul_lt_mul_of_pos_left key h1mφ
      _ = 1 - φ := mul_one _
  linarith [mul_lt_mul_of_pos_left this hR]

Dependency Graph

Location

thesis/CESProofs/Applications/KnowledgeCommons.lean:222

Module Section

Paper 10: The Knowledge Commons Paradox:

In the same file