Lemma: free-from-atom-rational
[a:Atom1]. ∀[q:ℚ].  a#q:ℚ

Definition: finite-prob-space
FinProbSpace ==  {p:ℚ List| 0 ≤ i < ||p||. p[i] 1 ∈ ℚ) ∧ (∀q∈p.0 ≤ q)} 

Lemma: finite-prob-space_wf
FinProbSpace ∈ Type

Lemma: fps-not-null
[p:FinProbSpace]. (null(p) ff)

Definition: unit-fps
*1* ==  [1]

Lemma: unit-fps_wf
*1* ∈ FinProbSpace

Definition: binary-fps
*50/50* ==  [(1/2); (1/2)]

Lemma: binary-fps_wf
*50/50* ∈ FinProbSpace

Definition: ternary-fps
*1/3* ==  [(1/3); (1/3); (1/3)]

Lemma: ternary-fps_wf
*1/3* ∈ FinProbSpace

Definition: uniform-fps
uniform-fps(n) ==  map(λx.(1/n);upto(n))

Lemma: uniform-fps_wf
[n:ℕ+]. (uniform-fps(n) ∈ FinProbSpace)

Definition: p-outcome
Outcome ==  ℕ||p||

Lemma: p-outcome_wf
[p:FinProbSpace]. (Outcome ∈ Type)

Lemma: natural_number_wf_p-outcome
[p:FinProbSpace]. (0 ∈ Outcome)

Lemma: decidable__p-outcome
p:FinProbSpace. Dec(Outcome)

Definition: weighted-sum
weighted-sum(p;F) ==  Σ0 ≤ i < ||p||. (F i) p[i]

Lemma: weighted-sum_wf
[p:ℚ List]. ∀[F:ℕ||p|| ─→ ℚ].  (weighted-sum(p;F) ∈ ℚ)

Lemma: ws_nil_lemma
F:Top. (weighted-sum([];F) 0)

Lemma: ws_single_lemma
F,p:Top.  (weighted-sum([p];F) ((F 0) p))

Lemma: weighted-sum-nil
[F:Top]. (weighted-sum([];F) 0)

Lemma: weighted-sum-split
[p,q:ℚ List]. ∀[F:ℕ||p q|| ─→ ℚ].
  (weighted-sum(p q;F) (weighted-sum(p;F) weighted-sum(q;λi.(F (i ||p||)))) ∈ ℚ)

Lemma: weighted-sum-linear
[a,b:ℚ]. ∀[p:ℚ List]. ∀[F,G:ℕ||p|| ─→ ℚ].
  (weighted-sum(p;λx.((a (F x)) (b (G x)))) ((a weighted-sum(p;F)) (b weighted-sum(p;G))) ∈ ℚ)

Lemma: ws-monotone
[p:ℚ List]. ∀[F,G:ℕ||p|| ─→ ℚ].
  (weighted-sum(p;F) ≤ weighted-sum(p;G)) supposing ((∀x:ℕ||p||. ((F x) ≤ (G x))) and (∀q:ℚ((q ∈ p)  (0 ≤ q))))

Lemma: weighted-sum_wf2
[p:FinProbSpace]. ∀[F:Outcome ─→ ℚ].  (weighted-sum(p;F) ∈ ℚ)

Lemma: ws-linear
[a,b:ℚ]. ∀[p:FinProbSpace]. ∀[F,G:Outcome ─→ ℚ].
  (weighted-sum(p;λx.((a (F x)) (b (G x)))) ((a weighted-sum(p;F)) (b weighted-sum(p;G))) ∈ ℚ)

Lemma: ws-constant
[a:ℚ]. ∀[p:FinProbSpace]. ∀[F:Outcome ─→ ℚ].  weighted-sum(p;F) a ∈ ℚ supposing ∀x:Outcome. ((F x) a ∈ ℚ)

Lemma: ws-lower-bound
[p:FinProbSpace]. ∀[F:Outcome ─→ ℚ]. ∀[q:ℚ].  q ≤ weighted-sum(p;F) supposing ∀x:Outcome. (q ≤ (F x))

Definition: null-seq
null ==  λx.⋅

Lemma: null-seq_wf
[T:Type]. (null ∈ ℕ0 ─→ T)

Definition: cons-seq
cons-seq(x;s) ==  λn.if (n =z 0) then else (n 1) fi 

Lemma: cons-seq_wf
[T:Type]. ∀[k:ℕ]. ∀[x:T]. ∀[s:ℕk ─→ T].  (cons-seq(x;s) ∈ ℕ1 ─→ T)

Definition: random-variable
RandomVariable(p;n) ==  (ℕn ─→ ℕ||p||) ─→ ℚ

Lemma: random-variable_wf
[k:FinProbSpace]. ∀[n:ℕ].  (RandomVariable(k;n) ∈ Type)

Lemma: subtype_rel-random-variable
[k:FinProbSpace]. ∀[n,m:ℕ].  RandomVariable(k;n) ⊆RandomVariable(k;m) supposing n ≤ m

Definition: rv-add
==  λs.((X s) (Y s))

Lemma: rv-add_wf
[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)].  (X Y ∈ RandomVariable(k;n))

Definition: rv-scale
q*X ==  λs.(q (X s))

Lemma: rv-scale_wf
[k:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(k;n)]. ∀[q:ℚ].  (q*X ∈ RandomVariable(k;n))

Definition: rv-mul
==  λs.((X s) (Y s))

Lemma: rv-mul_wf
[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)].  (X Y ∈ RandomVariable(k;n))

Definition: rv-shift
rv-shift(x;X) ==  λs.(X cons-seq(x;s))

Lemma: rv-shift_wf
[p:FinProbSpace]. ∀[n:ℕ+]. ∀[X:RandomVariable(p;n)]. ∀[x:Outcome].  (rv-shift(x;X) ∈ RandomVariable(p;n 1))

Lemma: rv-shift-linear
[k:FinProbSpace]. ∀[x:Outcome]. ∀[n:ℕ+]. ∀[X,Y:RandomVariable(k;n)]. ∀[a,b:ℚ].
  (rv-shift(x;a*X b*Y) a*rv-shift(x;X) b*rv-shift(x;Y) ∈ RandomVariable(k;n 1))

Definition: rv-sample
X@i ==  λs.(X (s i))

Lemma: rv-sample_wf
[k:FinProbSpace]. ∀[n:ℕ]. ∀[i:ℕn]. ∀[X:Outcome ─→ ℚ].  (X@i ∈ RandomVariable(k;n))

Definition: rv-qle
A ≤ ==  λs.if q_le(A s;B s) then else fi 

Lemma: rv-qle_wf
[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)].  (X ≤ Y ∈ RandomVariable(k;n))

Definition: rv-const
==  λs.a

Lemma: rv-const_wf
[p:FinProbSpace]. ∀[a:ℚ]. ∀[n:ℕ].  (a ∈ RandomVariable(p;n))

Definition: expectation
E(n;F) ==  expectation,n,F. if (n =z 0) then null else weighted-sum(p;λx.(expectation (n 1) rv-shift(x;F))) fi )\000C F

Lemma: expectation_wf
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)].  (E(n;X) ∈ ℚ)

Lemma: expectation-linear
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)]. ∀[a,b:ℚ].  (E(n;a*X b*Y) ((a E(n;X)) (b E(n;Y))) ∈ ℚ)

Lemma: expectation-constant
[p:FinProbSpace]. ∀[a:ℚ]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)].  E(n;X) a ∈ ℚ supposing ∀s:ℕn ─→ Outcome. ((X s) a ∈ ℚ)

Lemma: expectation-rv-const
[p:FinProbSpace]. ∀[a:ℚ]. ∀[n:ℕ].  (E(n;a) a ∈ ℚ)

Lemma: expectation-rv-add
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  (E(n;X Y) (E(n;X) E(n;Y)) ∈ ℚ)

Lemma: expectation-rv-scale
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)]. ∀[q:ℚ].  (E(n;q*X) (q E(n;X)) ∈ ℚ)

Lemma: expectation-qsum
[k:ℕ]. ∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:ℕk ─→ RandomVariable(p;n)].
  (E(n;λs.Σ0 ≤ i < k. s) = Σ0 ≤ i < k. E(n;X i) ∈ ℚ)

Lemma: expectation-rv-sample
[p:FinProbSpace]. ∀[n:ℕ]. ∀[i:ℕn]. ∀[X:Outcome ─→ ℚ].  (E(n;X@i) weighted-sum(p;X) ∈ ℚ)

Definition: rv-disjoint
rv-disjoint(p;n;X;Y) ==
  ∀i:ℕn
    ((∀s1,s2:ℕn ─→ Outcome.  ((∀j:ℕn. ((¬(j i ∈ ℤ))  ((s1 j) (s2 j) ∈ Outcome)))  ((X s1) (X s2) ∈ ℚ)))
    ∨ (∀s1,s2:ℕn ─→ Outcome.  ((∀j:ℕn. ((¬(j i ∈ ℤ))  ((s1 j) (s2 j) ∈ Outcome)))  ((Y s1) (Y s2) ∈ ℚ))))

Lemma: rv-disjoint_wf
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  (rv-disjoint(p;n;X;Y) ∈ ℙ)

Lemma: rv-disjoint-rv-shift
p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).
  (rv-disjoint(p;n;X;Y)
   (∀x,y:Outcome.  (rv-shift(x;X) rv-shift(y;X) ∈ RandomVariable(p;n 1)))
     ∨ (∀x,y:Outcome.  (rv-shift(x;Y) rv-shift(y;Y) ∈ RandomVariable(p;n 1))) 
     supposing 0 < n)

Lemma: rv-disjoint-rv-add
p:FinProbSpace. ∀n:ℕ. ∀X,Y,Z:RandomVariable(p;n).
  (rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;X;Z)  rv-disjoint(p;n;X;Y Z))

Lemma: rv-disjoint-symmetry
p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).  (rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;Y;X))

Lemma: rv-disjoint-rv-add2
p:FinProbSpace. ∀n:ℕ. ∀X,Y,Z:RandomVariable(p;n).
  (rv-disjoint(p;n;Y;X)  rv-disjoint(p;n;Z;X)  rv-disjoint(p;n;Y Z;X))

Lemma: rv-disjoint-rv-mul
p:FinProbSpace. ∀n:ℕ. ∀X,Y,Z:RandomVariable(p;n).
  (rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;X;Z)  rv-disjoint(p;n;X;Y Z))

Lemma: rv-disjoint-rv-mul2
p:FinProbSpace. ∀n:ℕ. ∀X,Y,Z:RandomVariable(p;n).
  (rv-disjoint(p;n;Y;X)  rv-disjoint(p;n;Z;X)  rv-disjoint(p;n;Y Z;X))

Lemma: rv-disjoint-const
p:FinProbSpace. ∀n:ℕ. ∀X:RandomVariable(p;n). ∀a:ℚ.  rv-disjoint(p;n;a;X)

Lemma: rv-disjoint-monotone-in-first
p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).  (rv-disjoint(p;n;X;Y)  (∀m:ℕrv-disjoint(p;m;X;Y) supposing n ≤ m))

Definition: rv-compose
(x.F[x]) ==  λs.F[X s]

Lemma: rv-compose_wf
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)]. ∀[F:ℚ ─→ ℚ].  ((X.F[X]) X ∈ RandomVariable(p;n))

Lemma: rv-disjoint-compose
F,G:ℚ ─→ ℚ. ∀p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n).
  (rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;(X.F[X]) X;(Y.G[Y]) Y))

Lemma: rv-disjoint-rv-scale
p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n). ∀a:ℚ.  (rv-disjoint(p;n;X;Y)  rv-disjoint(p;n;X;a*Y))

Lemma: rv-disjoint-shift
p:FinProbSpace. ∀n:ℕ. ∀X,Y:RandomVariable(p;n). ∀x:Outcome.
  rv-disjoint(p;n;X;Y)  rv-disjoint(p;n 1;rv-shift(x;X);rv-shift(x;Y)) supposing 0 < n

Lemma: expectation-rv-disjoint
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
  E(n;X Y) (E(n;X) E(n;Y)) ∈ ℚ supposing rv-disjoint(p;n;X;Y)

Lemma: expectation-rv-add-squared
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
  (E(n;(x.x x) Y) ((E(n;(x.x x) X) (2 E(n;X Y))) E(n;(x.x x) Y)) ∈ ℚ)

Lemma: expectation-rv-add-cubed
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
  (E(n;(x.(x x) x) Y)
  ((E(n;(x.(x x) x) X) (3 E(n;X Y)) (3 E(n;X Y))) E(n;(x.(x x) x) Y))
  ∈ ℚ)

Lemma: expectation-rv-add-fourth
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
  (E(n;(x.(x x) x) Y)
  ((E(n;(x.(x x) x) X) ((4 E(n;X Y)) (6 E(n;X Y))) (4 E(n;X Y)))
    E(n;(x.(x x) x) Y))
  ∈ ℚ)

Definition: rv-le
X ≤ ==  ∀s:ℕn ─→ Outcome. ((X s) ≤ (Y s))

Lemma: rv-le_wf
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  (X ≤ Y ∈ ℙ)

Lemma: rv-le_witness
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  (X ≤  s.Ax ∈ X ≤ Y))

Lemma: expectation-monotone
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].  E(n;X) ≤ E(n;Y) supposing X ≤ Y

Lemma: Markov-inequality
[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)].  ∀[e:ℚ]. E(n;e ≤ X) ≤ (E(n;X)/e) supposing 0 < supposing 0 ≤ X

Lemma: expectation-imax-list
[p:FinProbSpace]. ∀[n:ℕ]. ∀[k:ℕ+]. ∀[X:ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ].
  (E(n;λs.imax-list(map(λi.(X s);upto(k)))) ≤ Σ0 ≤ i < k. E(n;X i))

Lemma: expectation-non-neg
[p:FinProbSpace]. ∀[n:ℕ]. ∀[Y:RandomVariable(p;n)].  0 ≤ E(n;Y) supposing 0 ≤ Y

Definition: p-open
p-open(p) ==  {C:(n:ℕ × (ℕn ─→ Outcome)) ─→ ℕ2| ∀s:ℕ ─→ Outcome. ∀j:ℕ. ∀i:ℕj.  ((C <i, s>) ≤ (C <j, s>))} 

Lemma: p-open_wf
[p:FinProbSpace]. (p-open(p) ∈ Type)

Definition: p-open-member
s ∈ ==  ∃n:ℕ((C <n, s>1 ∈ ℤ)

Lemma: p-open-member_wf
[p:FinProbSpace]. ∀[C:p-open(p)]. ∀[s:ℕ ─→ Outcome].  (s ∈ C ∈ ℙ)

Definition: p-measure-le
measure(C) ≤ ==  ∀n:ℕE(n;λs.(C <n, s>)) < q

Lemma: p-measure-le_wf
[p:FinProbSpace]. ∀[q:ℚ]. ∀[C:p-open(p)].  (measure(C) ≤ q ∈ ℙ)

Lemma: open-random-variable
p:FinProbSpace. ∀n:ℕ. ∀C:p-open(p).  s.(C <n, s>) ∈ RandomVariable(p;n))

Lemma: open-expectation-monotone
[p:FinProbSpace]. ∀[n,m:ℕ].  ∀[C:p-open(p)]. (E(n;λs.(C <n, s>)) ≤ E(m;λs.(C <m, s>))) supposing n ≤ m

Definition: p-open-measure-one
measure(C) ==  ∀m:ℕ+. ∃n:ℕ((1 (1/m)) ≤ E(n;λs.(C <n, s>)))

Lemma: p-open-measure-one_wf
[p:FinProbSpace]. ∀[C:p-open(p)].  (measure(C) 1 ∈ ℙ)

Lemma: expectation-monotone-in-first
[p:FinProbSpace]. ∀[n,m:ℕ].  ∀[X:RandomVariable(p;n)]. (E(n;X) E(m;X) ∈ ℚsupposing n ≤ m

Definition: p-union
p-union(A;B) ==  λp.if (A =z 1) then else fi 

Lemma: p-union_wf
[p:FinProbSpace]. ∀[A,B:p-open(p)].  (p-union(A;B) ∈ p-open(p))

Lemma: member-p-union
p:FinProbSpace. ∀A,B:p-open(p). ∀s:ℕ ─→ Outcome.  (s ∈ p-union(A;B) ⇐⇒ s ∈ A ∨ s ∈ B)

Definition: countable-p-union
countable-p-union(i.A[i]) ==  λp.if (fst(p) =z 0) then else imax-list(map(λi.(A[i] p);upto(fst(p)))) fi 

Lemma: countable-p-union_wf
[p:FinProbSpace]. ∀[A:ℕ ─→ p-open(p)].  (countable-p-union(i.A[i]) ∈ p-open(p))

Lemma: member-countable-p-union
p:FinProbSpace. ∀A:ℕ ─→ p-open(p). ∀s:ℕ ─→ Outcome.  ((∃i:ℕs ∈ A[i])  s ∈ countable-p-union(i.A[i]))

Definition: nullset
nullset(p;S) ==  ∀q:{q:ℚ0 < q} . ∃C:p-open(p). ((∀s:ℕ ─→ Outcome. ((S s)  s ∈ C)) ∧ measure(C) ≤ q)

Lemma: nullset_wf
[p:FinProbSpace]. ∀[S:(ℕ ─→ Outcome) ─→ ℙ].  (nullset(p;S) ∈ ℙ)

Definition: Konig
Konig(k) ==
  ∀tree:(n:ℕ × (ℕn ─→ ℕk)) ─→ 𝔹
    ((∀i,j:ℕ.  ((i ≤ j)  (∀x:ℕj ─→ ℕk. ((↑(tree <j, x>))  (↑(tree <i, x>))))))
     (∃b:ℕ. ∀x:ℕb ─→ ℕk. (¬↑(tree <b, x>))))
     (∃s:ℕ ─→ ℕk. ∀n:ℕ(↑(tree <n, s>))))

Lemma: Konig_wf
[k:ℕ]. (Konig(k) ∈ ℙ)

Lemma: not-nullset
[p:FinProbSpace]. ¬nullset(p;λs.True) supposing ¬¬Konig(||p||)

Lemma: nullset-union
p:FinProbSpace. ∀[S:ℕ ─→ (ℕ ─→ Outcome) ─→ ℙ]. ((∀i:ℕnullset(p;S[i]))  nullset(p;λs.∃i:ℕ(S[i] s)))

Lemma: nullset-monotone
p:FinProbSpace. ∀[P,Q:(ℕ ─→ Outcome) ─→ ℙ].  ((∀s:ℕ ─→ Outcome. (Q[s]  P[s]))  nullset(p;P)  nullset(p;Q))

Definition: rv-unbounded
(X[n]─→∞ as n─→∞==  λs.∀B:ℚ. ∃n:ℕ. ∀m:ℕ((n ≤ m)  (B ≤ (X[m] s)))

Lemma: rv-unbounded_wf
[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].  ((X[n]─→∞ as n─→∞) ∈ (ℕ ─→ Outcome) ─→ ℙ)

Lemma: bounded-expectation
p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]). ∀B:ℚ.
  (nullset(p;(X[n]─→∞ as n─→∞))) supposing 
     ((∀n:ℕ(0 ≤ X[n] ∧ E(f[n];X[n]) < B)) and 
     0 < and 
     (∀n:ℕ. ∀i:ℕn.  X[i] ≤ X[n]) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))

Definition: rv-identically-distributed
rv-identically-distributed(p;n.f[n];i.X[i]) ==
  ∀n,m:ℕ.
    ((E(f[n];X[n]) E(f[m];X[m]) ∈ ℚ)
    ∧ (E(f[n];(x.x x) X[n]) E(f[m];(x.x x) X[m]) ∈ ℚ)
    ∧ (E(f[n];(x.(x x) x) X[n]) E(f[m];(x.(x x) x) X[m]) ∈ ℚ)
    ∧ (E(f[n];(x.(x x) x) X[n]) E(f[m];(x.(x x) x) X[m]) ∈ ℚ))

Lemma: rv-identically-distributed_wf
[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].  (rv-identically-distributed(p;n.f[n];n.X[n]) ∈ ℙ)

Definition: rv-iid
rv-iid(p;n.f[n];i.X[i]) ==
  rv-identically-distributed(p;n.f[n];i.X[i]) ∧ (∀n:ℕ. ∀i:ℕn.  (f[i] < f[n] ∧ rv-disjoint(p;f[n];X[i];X[n])))

Lemma: rv-iid_wf
[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].  (rv-iid(p;n.f[n];n.X[n]) ∈ ℙ)

Lemma: rv-iid-add
p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X,Y:n:ℕ ─→ RandomVariable(p;f[n]).
  (rv-iid(p;n.f[n];n.X[n])
   rv-iid(p;n.f[n];n.Y[n])
   (∀n:ℕ. ∀i:ℕ1.  (rv-disjoint(p;f[n];Y[i];X[n]) ∧ rv-disjoint(p;f[n];X[i];Y[n])))
   rv-iid(p;n.f[n];n.X[n] Y[n]))

Lemma: rv-iid-add-const
p:FinProbSpace. ∀a:ℚ. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]).
  (rv-iid(p;n.f[n];n.X[n])  rv-iid(p;n.f[n];n.X[n] a))

Definition: rv-partial-sum
rv-partial-sum(n;i.X[i]) ==  λs.Σ0 ≤ i < n. X[i] s

Lemma: rv-partial-sum_wf
[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])]. ∀[n:ℕ].
  rv-partial-sum(n;i.X[i]) ∈ RandomVariable(p;f[n]) supposing ∀n:ℕ. ∀i:ℕn.  f[i] < f[n]

Lemma: rv-partial-sum-unroll
[m:ℕ+]. ∀[X:Top].  (rv-partial-sum(m;i.X[i]) rv-partial-sum(m 1;i.X[i]) X[m 1])

Lemma: rv-disjoint-rv-partial-sum
p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]). ∀N:ℕ. ∀Z:RandomVariable(p;N). ∀n:ℕ.
  (∀i:ℕ1. rv-disjoint(p;N;X[i];Z))  (∀k:ℕn. rv-disjoint(p;N;rv-partial-sum(k;i.X[i]);Z)) supposing ∀i:ℕn. f[i] < N

Lemma: rv-partial-sum-monotone
[p:FinProbSpace]. ∀[f:ℕ ─→ ℕ]. ∀[X:n:ℕ ─→ RandomVariable(p;f[n])].
  (∀[m:ℕ]. ∀[n:ℕ1].  rv-partial-sum(n;i.X[i]) ≤ rv-partial-sum(m;i.X[i])) supposing 
     ((∀n:ℕ0 ≤ X[n]) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))

Lemma: slln-lemma1
p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]). ∀s,k:ℚ.
  ((∀n:ℕ. ∀i:ℕn.  rv-disjoint(p;f[n];X[i];X[n]))
      (∃B:ℚ((0 ≤ B) ∧ (∀n:ℕ(E(f[n];(x.(x x) x) rv-partial-sum(n;i.X[i])) ≤ (B n)))))) supposing 
     ((∀n:ℕ
         ((E(f[n];X[n]) 0 ∈ ℚ)
         ∧ (E(f[n];(x.x x) X[n]) s ∈ ℚ)
         ∧ (E(f[n];(x.(x x) x) X[n]) k ∈ ℚ))) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))

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) (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) X[n]) s ∈ ℚ)
         ∧ (E(f[n];(x.(x x) x) X[n]) k ∈ ℚ))) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))

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) X[n]) s ∈ ℚ)
         ∧ (E(f[n];(x.(x x) x) X[n]) k ∈ ℚ))) and 
     (∀n:ℕ. ∀i:ℕn.  f[i] < f[n]))

Lemma: slln-lemma4
p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]).
  (rv-iid(p;n.f[n];n.X[n])
   nullset(p;λs.∃q:ℚ(0 < q ∧ (∀n:ℕ. ∃m:ℕ(n < m ∧ (q ≤ 0 ≤ i < m. (1/m) (X[i] s)|))))) 
     supposing E(f[0];X[0]) 0 ∈ ℚ)

Lemma: strong-law-of-large-numbers
p:FinProbSpace. ∀f:ℕ ─→ ℕ. ∀X:n:ℕ ─→ RandomVariable(p;f[n]).
  (rv-iid(p;n.f[n];n.X[n])
   (∀mean:ℚ
        nullset(p;λs.∃q:ℚ(0 < q ∧ (∀n:ℕ. ∃m:ℕ(n < m ∧ (q ≤ 0 ≤ i < m. (1/m) (X[i] s) mean|))))) 
        supposing E(f[0];X[0]) mean ∈ ℚ))

Definition: random
random(p;a;b) ==  PRIMITIVE

Lemma: random_wf
[p:FinProbSpace]. ∀[a,b:Atom2].  (random(p;a;b) ∈ ℕ ─→ Outcome)

Definition: find-random
find-random{$k}(C;p;a;b) ==  PRIMITIVE

Lemma: find-random_wf
[p:FinProbSpace]. ∀[a,b:Atom2]. ∀[C:p-open(p)].
  (find-random{2}(C;p;a;b) ∈ {n:ℕ(C <n, random(p;a;b)>1 ∈ ℤsupposing ((a#C:p-open(p) ∨ b#C:p-open(p)) and meas\000Cure(C) 1)

Lemma: randomness
p:FinProbSpace. ∀a,b:Atom2. ∀C:p-open(p).
  (measure(C)  (a#C:p-open(p) ∨ b#C:p-open(p))  (∃n:ℕ((C <n, random(p;a;b)>1 ∈ ℤ)))



Home Index