Documentation

Lean 4 Proof

theorem welfare_loss_quadratic_approx (W_nn delta : ℝ) :
    -- The quadratic approximation of welfare loss
    -- V_n ≈ (1/2) * W_nn * delta^2
    (1 / 2 : ℝ) * W_nn * delta ^ 2 = W_nn * delta ^ 2 / 2 := by ring

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:168

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file