Share Function

def proved Foundations

Documentation

Lean 4 Proof

def shareFunction (w : Fin J → ℝ) (j : Fin J) : ℝ :=
  w j / ∑ k : Fin J, w k

Dependency Graph

Used by

shareFunction_scale_invariant equilibriumShare_is_shareFunction shareFunction_uniform_at_symmetry shareFunction_nonneg gibbsProb_is_shareFunction factorShare_is_shareFunction ten_views_one_object qExpAllocation_is_shareFunction logitProbability_is_shareFunction escortProbability_is_shareFunction contestShare_is_shareFunction luceChoice_is_shareFunction shareFunction_sum_one shareFunction_le_one escortDistribution_is_shareFunction shareFunction_coordinate_invariance shareFunction_iia powerMeanWeight_is_shareFunction shareFunction_maximum_dominates

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:55

Module Section

Ten Views of a Single Object: