---

Step * 1 1 of Lemma expectation-imax-list

.....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)
BY
{ (BLemma `expectation-monotone`
   THEN Auto
   THEN Try (Complete ((All (Unfold `random-variable`)
                        THEN All (Fold `p-outcome`)
                        THEN Auto'
                        THEN RWW "length-map length_upto" 0
                        THEN Auto)⋅)))⋅ }

1
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

---

Latex:


.....assertion..... 
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{}  E(n;\mlambda{}s.\mSigma{}0  \mleq{}  i  <  k.  X  i  s)


By

(BLemma  `expectation-monotone`
  THEN  Auto
  THEN  Try  (Complete  ((All  (Unfold  `random-variable`)
                                            THEN  All  (Fold  `p-outcome`)
                                            THEN  Auto'
                                            THEN  RWW  "length-map  length\_upto"  0
                                            THEN  Auto)\mcdot{})))\mcdot{}

---

Home Index