Sections / Section 4: Ten Views -- Universal Share Function / luceChoice_is_shareFunction

Luce Choice Is Share Function

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem luceChoice_is_shareFunction (v : Fin J → ℝ) (j : Fin J) :
    luceChoice v j = shareFunction v j :=
  rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:250

Module Section

Ten Views of a Single Object:

In the same file

shareFunction shareFunction_sum_one shareFunction_nonneg shareFunction_iia shareFunction_scale_invariant shareFunction_le_one powerMeanWeight luceChoice factorShare_is_shareFunction escortDistribution_is_shareFunction escortProbability_is_shareFunction logitProbability_is_shareFunction gibbsProb_is_shareFunction contestShare_is_shareFunction qExpAllocation_is_shareFunction powerMeanWeight_is_shareFunction equilibriumShare_is_shareFunction factorShare_escort_identity contest_factorShare_identity logit_escort_identity