---

Step * 2 1 of Lemma slln-lemma1

.....assertion..... 
1. p : FinProbSpace
2. f : ℕ ⟶ ℕ
3. X : n:ℕ ⟶ RandomVariable(p;f[n])
4. s : ℚ
5. k : ℚ
6. ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]
7. ∀n:ℕ. ((E(f[n];X[n]) = 0 ∈ ℚ) ∧ (E(f[n];(x.x * x) o X[n]) = s ∈ ℚ) ∧ (E(f[n];(x.(x * x) * x * x) o X[n]) = k ∈ ℚ))
8. ∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n])
9. 0 ≤ s
⊢ ∃B:ℚ. ((k ≤ B) ∧ (s ≤ B))
BY
{ (Decide s ≤ k THEN Auto THEN (InstConcl [⌜s⌝]⋅ THEN Auto THEN FLemma `qle_complement_qorder` [-1] THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:
.....assertion..... 
1.  p  :  FinProbSpace
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
3.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])
4.  s  :  \mBbbQ{}
5.  k  :  \mBbbQ{}
6.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]
7.  \mforall{}n:\mBbbN{}
          ((E(f[n];X[n])  =  0)
          \mwedge{}  (E(f[n];(x.x  *  x)  o  X[n])  =  s)
          \mwedge{}  (E(f[n];(x.(x  *  x)  *  x  *  x)  o  X[n])  =  k))
8.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    rv-disjoint(p;f[n];X[i];X[n])
9.  0  \mleq{}  s
\mvdash{}  \mexists{}B:\mBbbQ{}.  ((k  \mleq{}  B)  \mwedge{}  (s  \mleq{}  B))


By

---

Latex:
(Decide  s  \mleq{}  k
  THEN  Auto
  THEN  (InstConcl  [\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  FLemma  `qle\_complement\_qorder`  [-1]  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index