Step * 2 of Lemma open-expectation-monotone


1. FinProbSpace
2. : ℤ
3. 0 < n
4. ∀m:ℕ(((n 1) ≤ m)  (∀C:p-open(p). (E(n 1;λs.(C <1, s>)) ≤ E(m;λs.(C <m, s>)))))
5. : ℕ
6. n ≤ m
7. p-open(p)
⊢ E(n;λs.(C <n, s>)) ≤ E(m;λs.(C <m, s>))
BY
(RecUnfold `expectation` THEN RepeatFor ((SplitOnConclITE THEN Auto'))) }

1
.....falsecase..... 
1. FinProbSpace
2. : ℤ
3. 0 < n
4. ∀m:ℕ(((n 1) ≤ m)  (∀C:p-open(p). (E(n 1;λs.(C <1, s>)) ≤ E(m;λs.(C <m, s>)))))
5. : ℕ
6. n ≤ m
7. p-open(p)
8. ¬(n 0 ∈ ℤ)
9. ¬(m 0 ∈ ℤ)
⊢ weighted-sum(p;λx.E(n 1;rv-shift(x;λs.(C <n, s>)))) ≤ weighted-sum(p;λx.E(m 1;rv-shift(x;λs.(C <m, s>))))


Latex:


Latex:

1.  p  :  FinProbSpace
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}m:\mBbbN{}.  (((n  -  1)  \mleq{}  m)  {}\mRightarrow{}  (\mforall{}C:p-open(p).  (E(n  -  1;\mlambda{}s.(C  <n  -  1,  s>))  \mleq{}  E(m;\mlambda{}s.(C  <m,  s>)))))
5.  m  :  \mBbbN{}
6.  n  \mleq{}  m
7.  C  :  p-open(p)
\mvdash{}  E(n;\mlambda{}s.(C  <n,  s>))  \mleq{}  E(m;\mlambda{}s.(C  <m,  s>))


By


Latex:
(RecUnfold  `expectation`  0  THEN  RepeatFor  2  ((SplitOnConclITE  THEN  Auto')))




Home Index