---

Step * 2 1 of Lemma open-expectation-monotone

.....falsecase..... 
1. p : FinProbSpace
2. n : ℤ
3. 0 < n
4. ∀m:ℕ. (((n - 1) ≤ m) ⇒ (∀C:p-open(p). (E(n - 1;λs.(C <n - 1, s>)) ≤ E(m;λs.(C <m, s>)))))
5. m : ℕ@i
6. n ≤ m@i
7. C : p-open(p)@i
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>))))
BY
{ (BLemma `ws-monotone`
   THEN Auto
   THEN Try ((Try ((DVar `C' THEN Reduce 0))
              THEN Try (Unfold `random-variable` 0)
              THEN All (Fold `p-outcome`)⋅
              THEN Auto
              THEN (DVar `p' THEN Auto THEN (Unhide THEN Auto) THEN RWO "l_all_iff" 3 THEN Complete (Auto))⋅)⋅)) }

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

---

Latex:


.....falsecase..... 
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{}@i
6.  n  \mleq{}  m@i
7.  C  :  p-open(p)@i
8.  \mneg{}(n  =  0)
9.  \mneg{}(m  =  0)
\mvdash{}  weighted-sum(p;\mlambda{}x.E(n 
                                        -  1;rv-shift(x;\mlambda{}s.(C  <n,  s>))))  \mleq{}  weighted-sum(p;\mlambda{}x.E(m 
                                                                                                                                            -  1;rv-shift(x;\mlambda{}s.(C  <m,  s>)))\000C)


By

(BLemma  `ws-monotone`
  THEN  Auto
  THEN  Try  ((Try  ((DVar  `C'  THEN  Reduce  0))
                        THEN  Try  (Unfold  `random-variable`  0)
                        THEN  All  (Fold  `p-outcome`)\mcdot{}
                        THEN  Auto
                        THEN  (DVar  `p'
                                    THEN  Auto
                                    THEN  (Unhide  THEN  Auto)
                                    THEN  RWO  "l\_all\_iff"  3
                                    THEN  Complete  (Auto))\mcdot{})\mcdot{}))

---

Home Index