---

Step * 1 of Lemma expectation-imax-list


1. p : FinProbSpace
2. n : ℕ
3. k : ℕ+
4. X : ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ
⊢ E(n;λs.imax-list(map(λi.(X i s);upto(k)))) ≤ Σ0 ≤ i < k. E(n;X i)
BY
{ Assert ⌈E(n;λs.imax-list(map(λi.(X i s);upto(k)))) ≤ E(n;λs.Σ0 ≤ i < k. X i s)⌉⋅ }

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

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

---

Latex:



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


By

Assert  \mkleeneopen{}E(n;\mlambda{}s.imax-list(map(\mlambda{}i.(X  i  s);upto(k))))  \mleq{}  E(n;\mlambda{}s.\mSigma{}0  \mleq{}  i  <  k.  X  i  s)\mkleeneclose{}\mcdot{}

---

Home Index