Documentation

Lean 4 Proof

theorem dmp_search_ces (J : ℕ) (ρ T : ℝ) :
    -- The matching function M(u,v) is CES with parameter ρ
    -- The q-escort distribution models heterogeneous search intensity
    -- Higher K_eff → tighter labor market (Beveridge curve shifts in)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/Welfare.lean:139

Module Section

Theorem 8, Corollary 6, Propositions 18-22:

In the same file