Documentation

Lean 4 Proof

theorem qExp_logit_identity (T : ℝ) (ε : Fin J → ℝ) :
    qExpAllocation J 1 T ε = fun j =>
    Real.exp (ε j / T) / ∑ k : Fin J, Real.exp (ε k / T) :=
  qExpAllocation_at_one T ε

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:338

Module Section

Ten Views of a Single Object:

In the same file