---

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


1. p : FinProbSpace
2. n : ℤ
3. m : ℕ
4. 0 ≤ m
5. C : (n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2
6. ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))
7. s : ℕm ⟶ Outcome
⊢ (C <0, s>) ≤ (C <m, s>)
BY
{ xxx(Subst' s = (λn.if n <z m then s n else 0 fi ) ∈ (ℕm ⟶ Outcome) 0 THEN Auto)xxx }

1
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ
4. 0 ≤ m
5. C : (n:ℕ × (ℕn ⟶ Outcome)) ⟶ ℕ2
6. ∀s:ℕ ⟶ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))
7. s : ℕm ⟶ Outcome
⊢ (C <0, λn.if n <z m then s n else 0 fi >) ≤ (C <m, λn.if n <z m then s n else 0 fi >)

---

Latex:

---

Latex:

1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbN{}
4.  0  \mleq{}  m
5.  C  :  (n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  Outcome))  {}\mrightarrow{}  \mBbbN{}2
6.  \mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    ((C  <i,  s>)  \mleq{}  (C  <j,  s>))
7.  s  :  \mBbbN{}m  {}\mrightarrow{}  Outcome
\mvdash{}  (C  ɘ,  s>)  \mleq{}  (C  <m,  s>)


By

---

Latex:
xxx(Subst'  s  =  (\mlambda{}n.if  n  <z  m  then  s  n  else  0  fi  )  0  THEN  Auto)xxx

---

Home Index