Documentation

Lean 4 Proof

theorem logit_is_ces_at_q_one (T : ℝ) (_hT : T ≠ 0) (ε : Fin J → ℝ) (j : Fin J) :
    logitProbability J T ε j =
    escortDistribution J 1 (fun k => Real.exp (ε k / T)) j := by
  simp only [logitProbability, escortDistribution, rpow_one]

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:1029

Module Section

Economics extensions for CES formalization:

In the same file