---

Step * of Lemma expectation-imax-list

∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[k:ℕ+]. ∀[X:ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ].
  (E(n;λs.imax-list(map(λi.(X i s);upto(k)))) ≤ Σ0 ≤ i < k. E(n;X i))
BY
{ (Auto THEN (RWW "length-map length_upto" 0 THEN Auto)⋅) }

1
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)

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n:\mBbbN{}].  \mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[X:\mBbbN{}k  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbN{}].
    (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

(Auto  THEN  (RWW  "length-map  length\_upto"  0  THEN  Auto)\mcdot{})

---

Home Index