Documentation

Lean 4 Proof

theorem piketty_r_gt_g {r g s_K s δ : ℝ}
    (hδ : 0 < δ) (hs : 0 < s)
    (h_solow : s_K = r * s / δ) :
    r > g ↔ s_K > g * s / δ := by
  subst h_solow
  constructor
  · intro h
    exact div_lt_div_of_pos_right (mul_lt_mul_of_pos_right h hs) hδ
  · intro h
    rw [gt_iff_lt] at h ⊢
    by_contra h_neg
    push_neg at h_neg
    have : r * s ≤ g * s := mul_le_mul_of_nonneg_right h_neg (le_of_lt hs)
    have : r * s / δ ≤ g * s / δ := div_le_div_of_nonneg_right this (le_of_lt hδ)
    linarith

Dependency Graph

Location

thesis/CESProofs/Applications/Inequality.lean:161

Module Section

CES Inequality Decomposition

In the same file