Documentation

Lean 4 Proof

theorem geometricMean_symmetric {J : ℕ} (hJ : 0 < J) {c : ℝ} (hc : 0 < c) :
    geometricMean J (symmetricPoint J c) = c := by
  simp only [geometricMean, symmetricPoint, Finset.prod_const, Finset.card_univ, Fintype.card_fin]
  rw [← rpow_natCast c J, ← rpow_mul (le_of_lt hc)]
  simp [Nat.cast_ne_zero.mpr (by omega : J ≠ 0)]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:787

Module Section

Economics extensions for CES formalization:

In the same file