---

Step * 1 1 1 1 of Lemma open-expectation-monotone


1. p : FinProbSpace
2. n : ℤ
3. m : ℕ@i
4. 0 ≤ m@i
5. C : p-open(p)@i
6. s : ℕm ─→ Outcome@i
⊢ (C <0, null>) ≤ (C <m, s>)
BY
{ ((Subst' (C <0, null>) = (C <0, s>) ∈ ℤ 0 THEN Auto) THEN (DVar `C' THEN Unhide THEN Auto)⋅) }

1
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ@i
4. 0 ≤ m@i
5. C : (n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2@i
6. ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))@i
7. s : ℕm ─→ Outcome@i
⊢ (C <0, null>) = (C <0, s>) ∈ ℤ

2
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ@i
4. 0 ≤ m@i
5. C : (n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2@i
6. ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))@i
7. s : ℕm ─→ Outcome@i
⊢ (C <0, s>) ≤ (C <m, s>)

---

Latex:



1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbN{}@i
4.  0  \mleq{}  m@i
5.  C  :  p-open(p)@i
6.  s  :  \mBbbN{}m  {}\mrightarrow{}  Outcome@i
\mvdash{}  (C  ɘ,  null>)  \mleq{}  (C  <m,  s>)


By

((Subst'  (C  ɘ,  null>)  =  (C  ɘ,  s>)  0  THEN  Auto)  THEN  (DVar  `C'  THEN  Unhide  THEN  Auto)\mcdot{})

---

Home Index