---

Step * 1 1 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
6. 0 < ||map(λi.(X i s);upto(k))||
7. Σ0 ≤ i < k. X i s ∈ ℤ
8. b : ℕ
9. y : ℕk
10. (y ∈ upto(k))
11. b = (X y s) ∈ ℕ
⊢ b ≤ Σ0 ≤ i < k. X i s
BY
{ xxx(((HypSubst (-1) 0) THENA Auto) THEN InstLemma `summand-qle-sum` [⌜0⌝;⌜k⌝;⌜λ2i.X i s⌝;⌜y⌝]⋅ 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 ∈ ℤ
8. b : ℕ
9. y : ℕk
10. (y ∈ upto(k))
11. b = (X y s) ∈ ℕ
12. (X y s) ≤ Σ0 ≤ j < k. X j s
⊢ (X y s) ≤ Σ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
6.  0  <  ||map(\mlambda{}i.(X  i  s);upto(k))||
7.  \mSigma{}0  \mleq{}  i  <  k.  X  i  s  \mmember{}  \mBbbZ{}
8.  b  :  \mBbbN{}
9.  y  :  \mBbbN{}k
10.  (y  \mmember{}  upto(k))
11.  b  =  (X  y  s)
\mvdash{}  b  \mleq{}  \mSigma{}0  \mleq{}  i  <  k.  X  i  s


By

---

Latex:
xxx(((HypSubst  (-1)  0)  THENA  Auto)
        THEN  InstLemma  `summand-qle-sum`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.X  i  s\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
        THEN  Auto)xxx

---

Home Index