Step * 2 1 1 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. : ℕ@i
6. n ≤ m@i
7. p-open(p)@i
8. ¬(n 0 ∈ ℤ)
9. ¬(m 0 ∈ ℤ)
10. : ℕ||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)
BY
(RepUR ``rv-shift`` THEN (InstHyp [⌈1⌉;⌈λp.(C <(fst(p)) 1, cons-seq(x;snd(p))>)⌉4⋅ THENA Auto)) }

1
.....wf..... 
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. : ℕ@i
6. n ≤ m@i
7. p-open(p)@i
8. ¬(n 0 ∈ ℤ)
9. ¬(m 0 ∈ ℤ)
10. : ℕ||p||@i
⊢ λp.(C <(fst(p)) 1, cons-seq(x;snd(p))>) ∈ p-open(p)

2
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. : ℕ@i
6. n ≤ m@i
7. p-open(p)@i
8. ¬(n 0 ∈ ℤ)
9. ¬(m 0 ∈ ℤ)
10. : ℕ||p||@i
11. E(n 1;λs.((λp.(C <(fst(p)) 1, cons-seq(x;snd(p))>)) <1, s>)) ≤ E(m 1;λs.((λp.(C <(fst(p)) 1, cons-seq(x;\000Csnd(p))>)) <1, s>))
⊢ E(n 1;λs.(C <n, cons-seq(x;s)>)) ≤ E(m 1;λs.(C <m, cons-seq(x;s)>))


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


By

(RepUR  ``rv-shift``  0
  THEN  (InstHyp  [\mkleeneopen{}m  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}p.(C  <(fst(p))  +  1,  cons-seq(x;snd(p))>)\mkleeneclose{}]  4\mcdot{}  THENA  Auto)
  )




Home Index