Documentation

Lean 4 Proof

theorem logit_escort_identity (T : ℝ) (hT : T ≠ 0)
    (ε : Fin J → ℝ) (j : Fin J) :
    logitProbability J T ε j =
    escortDistribution J 1 (fun k => Real.exp (ε k / T)) j :=
  logit_is_ces_at_q_one T hT ε j

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:304

Module Section

Ten Views of a Single Object:

In the same file