Documentation

Lean 4 Proof

theorem critical_mass_above_has_benefit {T ρ c d_sq J : ℝ}
    (hc : 0 < c) (hd : 0 < d_sq) (hρ : ρ < 1) (hJ : 1 < J)
    (hJcrit : criticalMassJ T ρ c d_sq < J) (hT : 0 < T) :
    T < criticalFrictionReal J ρ c d_sq := by
  rw [criticalFrictionReal_eq J ρ c d_sq hJ (by linarith)]
  simp only [criticalMassJ] at hJcrit
  have hcd : 0 < 2 * c ^ 2 * d_sq := by positivity
  rw [lt_div_iff₀ (by linarith : (0:ℝ) < 1 - ρ)]
  have := (div_lt_iff₀ hcd).mp hJcrit
  nlinarith

Dependency Graph

Location

thesis/CESProofs/EntryExit/Equilibria.lean:227

Module Section

Paper 1c, Section 3: The Participation Game

In the same file