Documentation

Lean 4 Proof

def geometricMean (J : ℕ) (x : Fin J → ℝ) : ℝ :=
  (∏ j : Fin J, x j) ^ (1 / (↑J : ℝ))

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:782

Module Section

Economics extensions for CES formalization:

In the same file