Documentation

Lean 4 Proof

theorem critical_mass_below_no_benefit {T ρ c d_sq J : ℝ}
    (hc : 0 < c) (hd : 0 < d_sq) (hρ : ρ < 1) (hJ : 1 < J)
    (hJcrit : J < criticalMassJ T ρ c d_sq) (hT : 0 < T) :
    -- Below J_crit, T > T*(J), so K_eff = 0
    criticalFrictionReal J ρ c d_sq < T := 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 [div_lt_iff₀ (by linarith : (0:ℝ) < 1 - ρ)]
  have := (lt_div_iff₀ hcd).mp hJcrit
  nlinarith

Dependency Graph

Location

thesis/CESProofs/EntryExit/Equilibria.lean:214

Module Section

Paper 1c, Section 3: The Participation Game

In the same file