EconCSLib.GameTheory.StrategicGame.ZeroSum.Learning.Cesaro #
The realised cumulative payoff along a matrix-game play sequence. The knowledge blueprint records the Cesàro convergence target and its proof route.
noncomputable def
MatrixGame.realisedCumPayoff
{I J : Type u}
(A : MatrixGame I J ℝ)
(iSeq : ℕ → I)
(jSeq : ℕ → J)
(n : ℕ)
:
Realised cumulative payoff along a play sequence on A.
Equations
- A.realisedCumPayoff iSeq jSeq n = ∑ p ∈ Finset.range n, A.g (iSeq p) (jSeq p)