---

Step * 1 of Lemma slln-lemma1

.....assertion..... 
1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
3. X : n:ℕ ─→ RandomVariable(p;f[n])@i
4. s : ℚ@i
5. k : ℚ@i
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])@i
⊢ 0 ≤ s
BY
{ ((Assert E(f[1];(x.x * x) o X[1]) = s ∈ ℚ BY
          Auto)
   THEN (RevHypSubst' -1 0 THENA Auto)
   THEN (Subst' 0 = E(f[1];0) ∈ ℚ 0 THENA Auto)
   THEN Try ((BLemma `expectation-monotone` THEN Auto))
   THEN Try ((RWO "expectation-rv-const" 0 THEN Complete (Auto)))) }

1
1. p : FinProbSpace@i
2. f : ℕ ─→ ℕ@i
3. X : n:ℕ ─→ RandomVariable(p;f[n])@i
4. s : ℚ@i
5. k : ℚ@i
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])@i
9. E(f[1];(x.x * x) o X[1]) = s ∈ ℚ
⊢ 0 ≤ (x.x * x) o X[1]

---

Latex:


.....assertion..... 
1.  p  :  FinProbSpace@i
2.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
3.  X  :  n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n])@i
4.  s  :  \mBbbQ{}@i
5.  k  :  \mBbbQ{}@i
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])@i
\mvdash{}  0  \mleq{}  s


By

((Assert  E(f[1];(x.x  *  x)  o  X[1])  =  s  BY
                Auto)
  THEN  (RevHypSubst'  -1  0  THENA  Auto)
  THEN  (Subst'  0  =  E(f[1];0)  0  THENA  Auto)
  THEN  Try  ((BLemma  `expectation-monotone`  THEN  Auto))
  THEN  Try  ((RWO  "expectation-rv-const"  0  THEN  Complete  (Auto))))

---

Home Index