Proof of Nuprl Lemma : slln-lemma3

Step * 1 2 2 2 3 2 1 1 of Lemma slln-lemma3

.....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
9. B : ℚ
10. ∀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)

11. ∀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 )

       ∈ RandomVariable(p;f[n]))
12. 0 ≤ B
13. B < B + 1
14. ∀n:ℕ. ∀i:ℕn.
      rv-partial-sum(i;k.if (k =_z 0)
      then 0
      else (x.(x * x) * x * x) o (1/k)*rv-partial-sum(k;i.X[i])

      fi ) ≤ 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 )

15. ∀s:ℕ ─→ Outcome. ∀n:ℕ⁺. (Σ0 ≤ i < n. (1/n) * (X i s) ∈ ℚ)
16. ∀p:FinProbSpace. ∀[P,Q:(ℕ ─→ Outcome) ─→ ℙ]. ((∀s:ℕ ─→ Outcome. (Q[s] ⇒ P[s])) ⇒ {nullset(p;P) ⇒ nullset(p;Q)})
17. s1 : ℕ ─→ Outcome@i

18. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s1)|))))@i

19. B1 : ℚ@i
⊢ ∃n:ℕ. ∀m:ℕ. ((n ≤ m) ⇒ (B1 ≤ Σ1 ≤ k < m. (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s s1))
BY

{ (InstLemma `q-not-limit-zero-diverges-2` [⌈λ₂m.(λx.((x * x) * x * x)) |Σ0 ≤ i < m. (1/m) * (X i s1)|⌉;⌈B1⌉]⋅

   THENA (Auto THEN Try ((Reduce 0 THEN BLemma `q-square-non-neg` THEN Auto)))
   ) }

1
.....antecedent.....
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 : ℚ
10. ∀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)

11. ∀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 )

      fi ) ≤ 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 )

18. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s1)|))))@i

19. B1 : ℚ@i

⊢ ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ ((λx.((x * x) * x * x)) |Σ0 ≤ i < m. (1/m) * (X i s1)|)))))

2
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 : ℚ
10. ∀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)

11. ∀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 )

      fi ) ≤ 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 )

18. ∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ |Σ0 ≤ i < m. (1/m) * (X i s1)|))))@i

19. B1 : ℚ@i

20. ∃n:ℕ. (B1 ≤ Σ1 ≤ i < n. (λx.((x * x) * x * x)) |Σ0 ≤ i@0 < i. (1/i) * (X i@0 s1)|)

⊢ ∃n:ℕ. ∀m:ℕ. ((n ≤ m) ⇒ (B1 ≤ Σ1 ≤ k < m. (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s s1))

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 9. B : \mBbbQ{} 10. \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) 11. \mforall{}n:\mBbbN{} (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 ) \mmember{} RandomVariable(p;f[n])) 12. 0 \mleq{} B 13. B < B + 1 14. \mforall{}n:\mBbbN{}. \mforall{}i:\mBbbN{}n. rv-partial-sum(i;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{} 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 ) 15. \mforall{}s:\mBbbN{} {}\mrightarrow{} Outcome. \mforall{}n:\mBbbN{}\msupplus{}. (\mSigma{}0 \mleq{} i < n. (1/n) * (X i s) \mmember{} \mBbbQ{}) 16. \mforall{}p:FinProbSpace \mforall{}[P,Q:(\mBbbN{} {}\mrightarrow{} Outcome) {}\mrightarrow{} \mBbbP{}]. ((\mforall{}s:\mBbbN{} {}\mrightarrow{} Outcome. (Q[s] {}\mRightarrow{} P[s])) {}\mRightarrow{} \{nullset(p;P) {}\mRightarrow{} nullset(p;Q)\}) 17. s1 : \mBbbN{} {}\mrightarrow{} Outcome@i 18. \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 s1)|))))@i 19. B1 : \mBbbQ{}@i \mvdash{} \mexists{}n:\mBbbN{}. \mforall{}m:\mBbbN{}. ((n \mleq{} m) {}\mRightarrow{} (B1 \mleq{} \mSigma{}1 \mleq{} k < m. (x.(x * x) * x * x) o (1/k)*\mlambda{}s.\mSigma{}0 \mleq{} i < k. X i s s1)) By (InstLemma `q-not-limit-zero-diverges-2` [ \mkleeneopen{}\mlambda{}\msubtwo{}m.(\mlambda{}x.((x * x) * x * x)) |\mSigma{}0 \mleq{} i < m. (1/m) * (X i s1)|\mkleeneclose{};\mkleeneopen{}B1\mkleeneclose{}]\mcdot{} THENA (Auto THEN Try ((Reduce 0 THEN BLemma `q-square-non-neg` THEN Auto))) ) Home Index