---

Step * of Lemma slln-lemma3

∀p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]). ∀s,k:ℚ.
  ((∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n]))
     ⇒ nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s)|)))))) supposing 
     ((∀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 ∈ ℚ))) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))
BY
{ (InstLemma `slln-lemma2` []
   THEN RepeatFor 5 ((ParallelLast THEN (Thin (-3))))
   THEN RepeatFor 2 (ParallelLast)
   THEN (D 0
         THENA (Auto
                THEN Try (((Assert f[i] < f[n] BY
                                  Auto)
                           THEN (Assert ||p|| ∈ ℕ BY
                                       (DVar`p' THEN Auto))
                           THEN DoSubsume
                           THEN Auto))
                )
         )
   THEN ThinTrivial) }

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. ∃B:ℚ
    ∀n:ℕ
      (E(f[n];rv-partial-sum(n;k.if (k =z 0) then 0 else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i]) fi )) ≤ B)
⊢ nullset(p;λs.∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X[i] s)|)))))

---

Latex:


\mforall{}p:FinProbSpace.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}X:n:\mBbbN{}  {}\mrightarrow{}  RandomVariable(p;f[n]).  \mforall{}s,k:\mBbbQ{}.
    ((\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    rv-disjoint(p;f[n];X[i];X[n]))
          {}\mRightarrow{}  nullset(p;\mlambda{}s.\mexists{}q:\mBbbQ{}
                                            (0  <  q
                                            \mwedge{}  (\mforall{}n:\mBbbN{}.  \mexists{}m:\mBbbN{}.  (n  <  m  \mwedge{}  (q  \mleq{}  |\mSigma{}0  \mleq{}  i  <  m.  (1/m)  *  (X[i]  s)|))))))  supposing 
          ((\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)))  and 
          (\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    f[i]  <  f[n]))


By

(InstLemma  `slln-lemma2`  []
  THEN  RepeatFor  5  ((ParallelLast  THEN  (Thin  (-3))))
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (D  0
              THENA  (Auto
                            THEN  Try  (((Assert  f[i]  <  f[n]  BY
                                                                Auto)
                                                  THEN  (Assert  ||p||  \mmember{}  \mBbbN{}  BY
                                                                          (DVar`p'  THEN  Auto))
                                                  THEN  DoSubsume
                                                  THEN  Auto))
                            )
              )
  THEN  ThinTrivial)

---

Home Index