---

Step * 1 1 1 of Lemma expectation-imax-list


1. p : FinProbSpace
2. n : ℕ
3. k : ℕ+
4. X : ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ
⊢ λs.imax-list(map(λi.(X i s);upto(k))) ≤ λs.Σ0 ≤ i < k. X i s
BY
{ (RepUR ``rv-le`` 0 THEN Auto)⋅ }

1
1. p : FinProbSpace
2. n : ℕ
3. k : ℕ+
4. X : ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ
5. s : ℕn ─→ Outcome@i
⊢ imax-list(map(λi.(X i s);upto(k))) ≤ Σ0 ≤ i < k. X i s

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbN{}
3.  k  :  \mBbbN{}\msupplus{}
4.  X  :  \mBbbN{}k  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \mlambda{}s.imax-list(map(\mlambda{}i.(X  i  s);upto(k)))  \mleq{}  \mlambda{}s.\mSigma{}0  \mleq{}  i  <  k.  X  i  s


By

(RepUR  ``rv-le``  0  THEN  Auto)\mcdot{}

---

Home Index