theorem escortDistribution_is_shareFunction (q : ℝ)
    (x : Fin J → ℝ) (j : Fin J) :
    escortDistribution J q x j = shareFunction (fun k => (x k) ^ q) j :=
  rfl

theorem factorShare_is_shareFunction (a : Fin J → ℝ) (ρ : ℝ)
    (x : Fin J → ℝ) (j : Fin J) :
    factorShare J a ρ x j = shareFunction (fun k => a k * (x k) ^ ρ) j :=
  rfl

theorem contestShare_is_shareFunction (a x : Fin J → ℝ)
    (ρ : ℝ) (j : Fin J) :
    contestShare a x ρ j =
    shareFunction (fun k => a k * x k ^ ρ) j :=
  rfl

theorem logitProbability_is_shareFunction (T : ℝ)
    (ε : Fin J → ℝ) (j : Fin J) :
    logitProbability J T ε j =
    shareFunction (fun k => Real.exp (ε k / T)) j :=
  rfl

theorem gibbsProb_is_shareFunction (ε x : Fin J → ℝ)
    (T h : ℝ) (j : Fin J) :
    gibbsProb ε x T h j =
    shareFunction (fun k => gibbsWeight ε x T h k) j := by
  simp only [gibbsProb, gibbsZ, shareFunction]