Documentation

Lean 4 Proof

theorem production_cost_tradeoff
    {K_F K_C invariant : ℝ}
    (h_conservation : K_F * K_C = invariant)
    (h_KF : 0 < K_F) (h_KC : 0 < K_C)
    {ΔK_F : ℝ} (h_increase : 0 < ΔK_F)
    (h_new_conservation : (K_F + ΔK_F) * (K_C - ΔK_F) = invariant - ΔK_F ^ 2) :
    -- K_C decreases when K_F increases (conservation law)
    -- At first order (ΔK_F small): ΔK_C ≈ -ΔK_F
    K_C - ΔK_F < K_C := by
  linarith

Dependency Graph

Location

thesis/CESProofs/Potential/PrimalDual.lean:66

Module Section

## Policy Tradeoff Theorems (Gap 8)

In the same file