---

Step * of Lemma open-expectation-monotone

∀[p:FinProbSpace]. ∀[n,m:ℕ].  ∀[C:p-open(p)]. (E(n;λs.(C <n, s>)) ≤ E(m;λs.(C <m, s>))) supposing n ≤ m
BY
{ (Auto
   THEN Try ((BLemma `open-random-variable`  THEN Auto))
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN NatInd (-1)
   THEN Auto) }

1
1. p : FinProbSpace
2. n : ℤ
3. m : ℕ@i
4. 0 ≤ m@i
5. C : p-open(p)@i
⊢ E(0;λs.(C <0, s>)) ≤ E(m;λs.(C <m, s>))

2
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
⊢ E(n;λs.(C <n, s>)) ≤ E(m;λs.(C <m, s>))

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[n,m:\mBbbN{}].    \mforall{}[C:p-open(p)].  (E(n;\mlambda{}s.(C  <n,  s>))  \mleq{}  E(m;\mlambda{}s.(C  <m,  s>)))  supposing  n  \000C\mleq{}  m


By

(Auto
  THEN  Try  ((BLemma  `open-random-variable`    THEN  Auto))
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  NatInd  (-1)
  THEN  Auto)

---

Home Index