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@i
6. 0 < ||map(λi.(X i s);upto(k))||
7. Σ0 ≤ i < k. X i s ∈ ℤ
8. b : ℕ@i
9. y : ℕk@i
10. (y ∈ upto(k))@i
11. b = (X y s) ∈ ℕ@i
⊢ b ≤ Σ0 ≤ i < k. X i s
BY
{ (((HypSubst (-1) 0) THENA Auto) THEN InstLemma `summand-qle-sum` [⌈0⌉;⌈k⌉;⌈λ2i.X i s⌉;⌈y⌉]⋅ THEN Auto) }
1
1. p : FinProbSpace
2. n : ℕ
3. k : ℕ+
4. X : ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ
5. s : ℕn ─→ Outcome@i
6. 0 < ||map(λi.(X i s);upto(k))||
7. Σ0 ≤ i < k. X i s ∈ ℤ
8. b : ℕ@i
9. y : ℕk@i
10. (y ∈ upto(k))@i
11. b = (X y s) ∈ ℕ@i
12. (X y s) ≤ Σ0 ≤ j < k. X j s
⊢ (X y s) ≤ Σ0 ≤ i < k. X i s
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@i
6. 0 < ||map(\mlambda{}i.(X i s);upto(k))||
7. \mSigma{}0 \mleq{} i < k. X i s \mmember{} \mBbbZ{}
8. b : \mBbbN{}@i
9. y : \mBbbN{}k@i
10. (y \mmember{} upto(k))@i
11. b = (X y s)@i
\mvdash{} b \mleq{} \mSigma{}0 \mleq{} i < k. X i s
By
(((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)
Home
Index