Documentation

Lean 4 Proof

theorem gainsFromVariety_eq_scaling_ratio (hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {c : ℝ} (hc : 0 < c) :
    unnormCES J ρ (symmetricPoint J c) / (↑J * c) = gainsFromVariety J ρ := by
  rw [network_scaling hJ hρ hc]
  simp only [gainsFromVariety]
  have hJpos : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hcne : c ≠ 0 := ne_of_gt hc
  rw [mul_div_mul_right _ _ hcne]
  -- Goal: (↑J)^(1/ρ) / ↑J = (↑J)^(1/ρ - 1)
  rw [rpow_sub hJpos, rpow_one]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:241

Module Section

Economics extensions for CES formalization:

In the same file