Documentation

Lean 4 Proof

def inclusiveValue (J : ℕ) (T : ℝ) (ε : Fin J → ℝ) : ℝ :=
  T * Real.log (∑ k : Fin J, Real.exp (ε k / T))

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:1022

Module Section

Economics extensions for CES formalization:

In the same file