Documentation

Lean 4 Proof

theorem acr_gains_gt_one {lam ρ : ℝ}
    (hlam : 0 < lam) (hlam1 : lam < 1) (hρ : 0 < ρ) (hρ1 : ρ < 1) :
    1 < acrGainsFromTrade lam ρ := by
  simp only [acrGainsFromTrade]
  have hexp_neg : -(1 / ρ - 1) < 0 := by
    rw [neg_lt_zero, sub_pos, lt_div_iff₀ hρ, one_mul]
    exact hρ1
  calc (1 : ℝ) = lam ^ (0 : ℝ) := (rpow_zero lam).symm
    _ < lam ^ (-(1 / ρ - 1)) := by
        exact rpow_lt_rpow_of_exponent_gt hlam hlam1 hexp_neg

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:313

Module Section

Economics extensions for CES formalization:

In the same file