Documentation

Lean 4 Proof

def logitProbability (J : ℕ) (T : ℝ) (ε : Fin J → ℝ) (j : Fin J) : ℝ :=
  Real.exp (ε j / T) / ∑ k : Fin J, Real.exp (ε k / T)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:1014

Module Section

Economics extensions for CES formalization:

In the same file