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

Luce Choice

defprovedFoundations

Documentation

Lean 4 Proof

def luceChoice (v : Fin J → ℝ) (j : Fin J) : ℝ :=
  v j / ∑ k : Fin J, v k

Dependency Graph

Used by

ten_views_one_object luceChoice_is_shareFunction

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:140

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 factorShare_is_shareFunction escortDistribution_is_shareFunction escortProbability_is_shareFunction logitProbability_is_shareFunction gibbsProb_is_shareFunction contestShare_is_shareFunction qExpAllocation_is_shareFunction powerMeanWeight_is_shareFunction luceChoice_is_shareFunction equilibriumShare_is_shareFunction factorShare_escort_identity contest_factorShare_identity logit_escort_identity