---

Step * 1 2 of Lemma expectation-imax-list


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)
BY
{ (NthHypEq  (-1) THEN (EqCD THEN Auto) THEN (RWW "length-map length_upto expectation-qsum" 0 THEN Auto)⋅) }

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbN{}
3.  k  :  \mBbbN{}\msupplus{}
4.  X  :  \mBbbN{}k  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbN{}
5.  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)
\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

(NthHypEq    (-1)
  THEN  (EqCD  THEN  Auto)
  THEN  (RWW  "length-map  length\_upto  expectation-qsum"  0  THEN  Auto)\mcdot{})

---

Home Index