Documentation

Lean 4 Proof

theorem complementarity_paradox_barrier {T c d_sq ρ₁ ρ₂ : ℝ}
    (hc : 0 < c) (hd : 0 < d_sq) (hT : 0 < T)
    (hρ₁ : ρ₁ < 1) (hρ₂ : ρ₂ < 1) (hρ : ρ₂ < ρ₁) :
    -- Lower rho (more complementary) -> higher J_crit
    criticalMassJ T ρ₁ c d_sq < criticalMassJ T ρ₂ c d_sq :=
  criticalMassJ_increasing_in_complementarity hc hd hT hρ₂ hρ₁ (by linarith)

Dependency Graph

Location

thesis/CESProofs/EntryExit/Welfare.lean:96

Module Section

Paper 1c, Section 4: Welfare and Coordination Failure

In the same file