Documentation

Lean 4 Proof

theorem ten_views_one_object :
    -- View 1: CES factor shares = shareFunction
    (∀ (a : Fin J → ℝ) (ρ : ℝ) (x : Fin J → ℝ) (j : Fin J),
      factorShare J a ρ x j =
      shareFunction (fun k => a k * (x k) ^ ρ) j) ∧
    -- View 2: Escort distribution = shareFunction
    (∀ (q : ℝ) (x : Fin J → ℝ) (j : Fin J),
      escortDistribution J q x j =
      shareFunction (fun k => (x k) ^ q) j) ∧
    -- View 3: Escort probability = shareFunction
    (∀ (x : Fin J → ℝ) (ρ : ℝ) (j : Fin J),
      escortProbability x ρ j =
      shareFunction (fun k => (x k) ^ ρ) j) ∧
    -- View 4: Logit / Softmax = shareFunction
    (∀ (T : ℝ) (ε : Fin J → ℝ) (j : Fin J),
      logitProbability J T ε j =
      shareFunction (fun k => Real.exp (ε k / T)) j) ∧
    -- View 5: Gibbs-Boltzmann = shareFunction
    (∀ (ε x : Fin J → ℝ) (T h : ℝ) (j : Fin J),
      gibbsProb ε x T h j =
      shareFunction (fun k => gibbsWeight ε x T h k) j) ∧
    -- View 6: Tullock contest = shareFunction
    (∀ (a x : Fin J → ℝ) (ρ : ℝ) (j : Fin J),
      contestShare a x ρ j =
      shareFunction (fun k => a k * x k ^ ρ) j) ∧
    -- View 7: q-exponential = shareFunction
    (∀ (q T : ℝ) (ε : Fin J → ℝ) (j : Fin J),
      qExpAllocation J q T ε j =
      shareFunction (fun k => qExp q (ε k / T)) j) ∧
    -- View 8: Power mean weight = shareFunction
    (∀ (x : Fin J → ℝ) (ρ : ℝ) (j : Fin J),
      powerMeanWeight x ρ j =
      shareFunction (fun k => (x k) ^ ρ) j) ∧
    -- View 9: Luce choice = shareFunction
    (∀ (v : Fin J → ℝ) (j : Fin J),
      luceChoice v j = shareFunction v j) ∧
    -- View 10: Equilibrium share = shareFunction
    (∀ (a cost : Fin J → ℝ) (ρ : ℝ) (j : Fin J),
      equilibriumShare a cost ρ j =
      shareFunction (fun k => agentFitness a cost ρ k) j) :=
  ⟨fun _ _ _ _ => rfl,                                            -- 1: factor shares
   fun _ _ _ => rfl,                                               -- 2: escort
   fun x ρ j => by simp only [escortProbability, escortPartitionZ, -- 3: escort prob
                               shareFunction],
   fun _ _ _ => rfl,                                               -- 4: logit
   fun ε x T h j => by simp only [gibbsProb, gibbsZ,              -- 5: Gibbs
                                   shareFunction],
   fun _ _ _ _ => rfl,                                             -- 6: contest
   fun q T ε j => by simp only [qExpAllocation, shareFunction],    -- 7: q-exp
   fun _ _ _ => rfl,                                               -- 8: power mean
   fun _ _ => rfl,                                                 -- 9: Luce
   fun a cost ρ j => by simp only [equilibriumShare,               -- 10: equilibrium
                                    shareFunction]⟩

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:436

Module Section

Ten Views of a Single Object:

In the same file