---

Step * of Lemma slln-lemma2

∀p:FinProbSpace. ∀f:ℕ ⟶ ℕ. ∀X:n:ℕ ⟶ RandomVariable(p;f[n]). ∀s,k:ℚ.
  ((∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n]))
     ⇒ (∃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))) 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
{ (Auto
   THEN (InstLemma `slln-lemma1` [⌜p⌝;⌜f⌝;⌜X⌝;⌜s⌝;⌜k⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (InstConcl [⌜2 * B⌝]⋅ THENA Auto)
   THEN Using [`p',⌜p⌝;`f',⌜f⌝] Auto⋅
   THEN Auto
   THEN (Assert ∀k:ℕn. (rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;f[n])) BY
               (Auto THEN (InstLemma `rv-partial-sum_wf` [⌜p⌝;⌜f⌝;⌜X⌝;⌜k1⌝]⋅ THENA Auto) THEN DoSubsume THEN Auto))) }

1
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. B : ℚ
10. 0 ≤ B
11. ∀n:ℕ. (E(f[n];(x.(x * x) * x * x) o rv-partial-sum(n;i.X[i])) ≤ (B * n * n))
12. n : ℕ
13. ∀k:ℕn. (rv-partial-sum(k;i.X[i]) ∈ RandomVariable(p;f[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 )) ≤ (2 * B)

---

Latex:

---

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{}  (\mexists{}B:\mBbbQ{}
                    \mforall{}n:\mBbbN{}
                        (E(f[n];rv-partial-sum(n;k.if  (k  =\msubz{}  0)
                        then  0
                        else  (x.(x  *  x)  *  x  *  x)  o  (1/k)*rv-partial-sum(k;i.X[i])
                        fi  ))  \mleq{}  B)))  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

---

Latex:
(Auto
  THEN  (InstLemma  `slln-lemma1`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstConcl  [\mkleeneopen{}2  *  B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Using  [`p',\mkleeneopen{}p\mkleeneclose{};`f',\mkleeneopen{}f\mkleeneclose{}]  Auto\mcdot{}
  THEN  Auto
  THEN  (Assert  \mforall{}k:\mBbbN{}n.  (rv-partial-sum(k;i.X[i])  \mmember{}  RandomVariable(p;f[n]))  BY
                          (Auto
                            THEN  (InstLemma  `rv-partial-sum\_wf`  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}k1\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  DoSubsume
                            THEN  Auto)))

---

Home Index