Proof of Nuprl Lemma : slln-lemma3

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

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

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

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

 (B1 ≤ Σ0 ≤ k < m. if (k =_z 0) then 0 else (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s fi  s1))

BY
{ ((Assert ∀k:ℕ. (λs.Σ0 ≤ i < k. X i s ∈ (ℕ ⟶ Outcome) ⟶ ℚ) BY
(Auto THEN Try (Fold `random-variable` 0) THEN Try (Fold `p-outcome` 0) THEN Auto))

   THEN (Assert ∀k:ℕ⁺. ((x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s s1 ∈ ℚ) BY

               (Auto
                THEN RepUR ``rv-const rv-compose`` 0
                THEN Auto
                THEN (GenConcl ⌜(1/k1) = a ∈ ℚ⌝⋅ THENA Auto)
                THEN Auto
                THEN (Assert ¬(k1 = 0 ∈ ℤ) BY
                            Auto')
                THEN Auto
                THEN GenConclAtAddrType ⌜(ℕ ⟶ Outcome) ⟶ ℚ⌝ [2;1;2]⋅
                THEN Auto
                THEN RepUR ``rv-scale`` 0
                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. ∀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)|))))

19. B1 : ℚ
20. n : ℕ
21. ∀m:ℕ. ((n ≤ m) ⇒ (B1 ≤ Σ1 ≤ k < m. (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s s1))
22. ∀k:ℕ. (λs.Σ0 ≤ i < k. X i s ∈ (ℕ ⟶ Outcome) ⟶ ℚ)
23. ∀k:ℕ⁺. ((x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s s1 ∈ ℚ)
⊢ ∃n:ℕ
∀m:ℕ. ((n ≤ m) ⇒

 (B1 ≤ Σ0 ≤ k < m. if (k =_z 0) then 0 else (x.(x * x) * x * x) o (1/k)*λs.Σ0 ≤ i < k. X i s fi  s1))

Latex:

Latex:
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. 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 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)|)))) 19. B1 : \mBbbQ{} 20. n : \mBbbN{} 21. \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)) \mvdash{} \mexists{}n:\mBbbN{} \mforall{}m:\mBbbN{} ((n \mleq{} m) {}\mRightarrow{} (B1 \mleq{} \mSigma{}0 \mleq{} k < m. if (k =\msubz{} 0) then 0 else (x.(x * x) * x * x) o (1/k)*\mlambda{}s.\mSigma{}0 \mleq{} i < k. X i s fi s1)) By Latex: ((Assert \mforall{}k:\mBbbN{}. (\mlambda{}s.\mSigma{}0 \mleq{} i < k. X i s \mmember{} (\mBbbN{} {}\mrightarrow{} Outcome) {}\mrightarrow{} \mBbbQ{}) BY (Auto THEN Try (Fold `random-variable` 0) THEN Try (Fold `p-outcome` 0) THEN Auto)) THEN (Assert \mforall{}k:\mBbbN{}\msupplus{}. ((x.(x * x) * x * x) o (1/k)*\mlambda{}s.\mSigma{}0 \mleq{} i < k. X i s s1 \mmember{} \mBbbQ{}) BY (Auto THEN RepUR ``rv-const rv-compose`` 0 THEN Auto THEN (GenConcl \mkleeneopen{}(1/k1) = a\mkleeneclose{}\mcdot{} THENA Auto) THEN Auto THEN (Assert \mneg{}(k1 = 0) BY Auto') THEN Auto THEN GenConclAtAddrType \mkleeneopen{}(\mBbbN{} {}\mrightarrow{} Outcome) {}\mrightarrow{} \mBbbQ{}\mkleeneclose{} [2;1;2]\mcdot{} THEN Auto THEN RepUR ``rv-scale`` 0 THEN Auto)) ) Home Index