Documentation

Lean 4 Proof

theorem gainsFromVariety_gt_one (hJ : 2 ≤ J) {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1) :
    1 < gainsFromVariety J ρ := by
  simp only [gainsFromVariety]
  have hJpos : (1 : ℝ) < ↑J := by exact_mod_cast (by omega : 1 < J)
  have hexp : 0 < 1 / ρ - 1 := by
    rw [sub_pos, lt_div_iff₀ hρ, one_mul]
    exact hρ1
  calc (1 : ℝ) = 1 ^ (1 / ρ - 1) := (one_rpow _).symm
    _ < (↑J : ℝ) ^ (1 / ρ - 1) := by
        exact rpow_lt_rpow zero_le_one hJpos hexp

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:255

Module Section

Economics extensions for CES formalization:

In the same file