---

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


1. p : FinProbSpace
2. n : ℕ
3. k : ℕ+
4. X : ℕk ⟶ (ℕn ⟶ Outcome) ⟶ ℕ
5. s : ℕn ⟶ Outcome
⊢ imax-list(map(λi.(X i s);upto(k))) ≤ Σ0 ≤ i < k. X i s
BY
{ xxx((Assert 0 < ||map(λi.(X i s);upto(k))|| BY
             ((RWO "length-map" 0 THEN Auto) THEN RWO "length_upto" 0 THEN Auto))
      THEN (Assert Σ0 ≤ i < k. X i s ∈ ℤ BY
                  (BLemma `qsum-int` THEN Auto))
      THEN (RWO "qle-int" 0 THEN Auto)
      THEN BLemma `imax-list-lb`
      THEN Auto)xxx }

1
1. p : FinProbSpace
2. n : ℕ
3. k : ℕ+
4. X : ℕk ⟶ (ℕn ⟶ Outcome) ⟶ ℕ
5. s : ℕn ⟶ Outcome
6. 0 < ||map(λi.(X i s);upto(k))||
7. Σ0 ≤ i < k. X i s ∈ ℤ
⊢ (∀b∈map(λi.(X i s);upto(k)).b ≤ Σ0 ≤ i < k. X i s)

---

Latex:

---

Latex:

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


By

---

Latex:
xxx((Assert  0  <  ||map(\mlambda{}i.(X  i  s);upto(k))||  BY
                      ((RWO  "length-map"  0  THEN  Auto)  THEN  RWO  "length\_upto"  0  THEN  Auto))
        THEN  (Assert  \mSigma{}0  \mleq{}  i  <  k.  X  i  s  \mmember{}  \mBbbZ{}  BY
                                (BLemma  `qsum-int`  THEN  Auto))
        THEN  (RWO  "qle-int"  0  THEN  Auto)
        THEN  BLemma  `imax-list-lb`
        THEN  Auto)xxx

---

Home Index