Documentation

Lean 4 Proof

theorem welfare_gap_lower_bound {J_high J_low ρ c : ℝ}
    (hJl : 1 < J_low) (hJh : J_low < J_high)
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c) :
    0 < (valueFunction J_high ρ c - valueFunction J_low ρ c) * J_low := by
  apply mul_pos
  · linarith [pareto_ranking_strengthened hJl hJh hρ0 hρ1 hc]
  · linarith

Dependency Graph

Used by

Location

thesis/CESProofs/EntryExit/Calculus.lean:362

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)

In the same file