Lean declarations

abbrev wsum EconCSLib @ cef01c7, EconCSLib.Math.Simplex

abbrev wsum (x : stdSimplex 𝕜 I) (f : I → 𝕜) : 𝕜 :=
  x ⬝ᵥ f

theorem wsum_const EconCSLib @ cef01c7, EconCSLib.Math.Simplex
Weighted sum of a constant equals the constant.
```
theorem wsum_const (x : stdSimplex 𝕜 I) (c : 𝕜) :
    wsum x (fun _ => c) = c
```
theorem wsum_le_wsum EconCSLib @ cef01c7, EconCSLib.Math.Simplex
Weighted sum is monotone: pointwise `≤` implies `wsum ≤`.
```
theorem wsum_le_wsum (x : stdSimplex 𝕜 I) {f g : I → 𝕜}
    (h : ∀ i, f i ≤ g i) : wsum x f ≤ wsum x g
```
theorem wsum_nonneg EconCSLib @ cef01c7, EconCSLib.Math.Simplex
Weighted sum of non-negative values is non-negative.
```
theorem wsum_nonneg (x : stdSimplex 𝕜 I) {f : I → 𝕜}
    (h : ∀ i, 0 ≤ f i) : 0 ≤ wsum x f
```

theorem wsum_pos EconCSLib @ cef01c7, EconCSLib.Math.Simplex

theorem wsum_pos (x : stdSimplex 𝕜 I) {f : I → 𝕜}
    (hf : ∀ i, 0 < f i) : 0 < wsum x f

theorem wsum_ge_wsum EconCSLib @ cef01c7, EconCSLib.Math.Simplex

Weighted sum respects `≥`.

theorem wsum_ge_wsum (x : stdSimplex 𝕜 I) {f g : I → 𝕜}
    (h : ∀ i, f i ≥ g i) : wsum x f ≥ wsum x g

theorem wsum_add EconCSLib @ cef01c7, EconCSLib.Math.Simplex

Weighted sum is linear over addition.

theorem wsum_add (x : stdSimplex 𝕜 I) (f g : I → 𝕜) :
    wsum x (f + g) = wsum x f + wsum x g

theorem wsum_smul EconCSLib @ cef01c7, EconCSLib.Math.Simplex
Weighted sum commutes with scalar multiplication.
```
theorem wsum_smul (x : stdSimplex 𝕜 I) (c : 𝕜) (f : I → 𝕜) :
    wsum x (c • f) = c * wsum x f
```

Modules: EconCSLib.Math.Simplex

Weighted Sum over the Standard Simplex

For a finite index I, a strictly ordered field 𝕜, an element x ∈ stdSimplex 𝕜 I, and a function f : I → 𝕜, the weighted sum is $$ \operatorname{wsum} x \, f \;=\; \sum_{i \in I} x_i \cdot f(i). $$

This is the operator that turns a mixed strategy into an expected payoff and a lottery into an expected utility. It is definitionally equal to Mathlib's finite dot product x ⬝ᵥ f, but receives a dedicated name because the simplex-specific algebraic lemmas below depend on the constraints $\sum_i x_i = 1$ and $x_i \ge 0$ and have no generic dotProduct analogue.

The core algebra:

wsum_const -- wsum x (fun _ => c) = c
wsum_le_wsum -- pointwise f ≤ g implies wsum x f ≤ wsum x g
wsum_nonneg -- pointwise 0 ≤ f implies 0 ≤ wsum x f
wsum_ge_wsum -- the symmetric ≥ version of monotonicity
wsum_add -- wsum x (f + g) = wsum x f + wsum x g
wsum_smul -- wsum x (c • f) = c · wsum x f

References

[MFoGT, Chapter 1] Laraki, Renault, and Sorin, Mathematical Foundations of Game Theory. Mixed-strategy weighted sums.

Provenance

Adapted from GameTheory/Simplex.lean in math-xmum/gametheory.

Weighted Sum over the Standard Simplex

References

Provenance

Used by

Also in