Documentation

Lean 4 Proof

theorem optimal_scope_foc (K_eff T mg mh : ℝ) (_hK : 0 < K_eff) (hT : 0 < T)
    (hmg : 0 < mg) (_hmh : 0 < mh) :
    -- At the optimum, the ratio of marginal benefits to marginal costs
    -- determines the scope: K_eff/T = h'(n*)/g'(n*)
    K_eff * mg = T * mh ↔ K_eff / T = mh / mg := by
  constructor
  · intro h
    rw [div_eq_div_iff (ne_of_gt hT) (ne_of_gt hmg)]
    linarith
  · intro h
    rw [div_eq_div_iff (ne_of_gt hT) (ne_of_gt hmg)] at h
    linarith

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:50

Module Section

Propositions 12-17 and Corollary 5:

In the same file