Critical Mass Zero Friction

theorem proved Microeconomics

Documentation

Lean 4 Proof

theorem critical_mass_zero_friction {ρ c d_sq : ℝ} :
    criticalMassJ 0 ρ c d_sq = 0 := by
  simp [criticalMassJ]

Dependency Graph

Location

thesis/CESProofs/EntryExit/Equilibria.lean:239

Module Section

Paper 1c, Section 3: The Participation Game

In the same file

strategic_complementarity strategic_complementarity_full marginal_curvature_bounded multiple_equilibria_sign_below_peak multiple_equilibria_lower_root multiple_equilibria_upper_root multiple_equilibria_fold trivial_equilibrium_exists critical_mass_below_no_benefit critical_mass_above_has_benefit