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) ~ 0 + ((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 x else s (n - 1) fi
Lemma: cons-seq_wf
∀[T:Type]. ∀[k:ℕ]. ∀[x:T]. ∀[s:ℕk ─→ T]. (cons-seq(x;s) ∈ ℕk + 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) ⊆r RandomVariable(k;m) supposing n ≤ m
Definition: rv-add
X + Y == λ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
X * Y == λ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 ≤ B == λs.if q_le(A s;B s) then 1 else 0 fi
Lemma: rv-qle_wf
∀[k:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(k;n)]. (X ≤ Y ∈ RandomVariable(k;n))
Definition: rv-const
a == λs.a
Lemma: rv-const_wf
∀[p:FinProbSpace]. ∀[a:ℚ]. ∀[n:ℕ]. (a ∈ RandomVariable(p;n))
Definition: expectation
E(n;F) == Y (λexpectation,n,F. if (n =z 0) then F null else weighted-sum(p;λx.(expectation (n - 1) rv-shift(x;F))) fi )\000C n 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. X i 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]) o X == λs.F[X s]
Lemma: rv-compose_wf
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X:RandomVariable(p;n)]. ∀[F:ℚ ─→ ℚ]. ((X.F[X]) o 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]) o X;(Y.G[Y]) o 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) o X + Y) = ((E(n;(x.x * x) o X) + (2 * E(n;X * Y))) + E(n;(x.x * x) o Y)) ∈ ℚ)
Lemma: expectation-rv-add-cubed
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
(E(n;(x.(x * x) * x) o X + Y)
= ((E(n;(x.(x * x) * x) o X) + (3 * E(n;X * X * Y)) + (3 * E(n;X * Y * Y))) + E(n;(x.(x * x) * x) o Y))
∈ ℚ)
Lemma: expectation-rv-add-fourth
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[X,Y:RandomVariable(p;n)].
(E(n;(x.(x * x) * x * x) o X + Y)
= ((E(n;(x.(x * x) * x * x) o X) + ((4 * E(n;X * X * X * Y)) + (6 * E(n;X * X * Y * Y))) + (4 * E(n;X * Y * Y * Y)))
+ E(n;(x.(x * x) * x * x) o Y))
∈ ℚ)
Definition: rv-le
X ≤ Y == ∀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 ≤ Y ⇒ (λ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 < e supposing 0 ≤ X
Lemma: expectation-imax-list
∀[p:FinProbSpace]. ∀[n:ℕ]. ∀[k:ℕ+]. ∀[X:ℕk ─→ (ℕn ─→ Outcome) ─→ ℕ].
(E(n;λs.imax-list(map(λi.(X i 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 ∈ C == ∃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) ≤ q == ∀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) = 1 == ∀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 p =z 1) then 1 else B p 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 0 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 < B 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) o X[n]) = E(f[m];(x.x * x) o X[m]) ∈ ℚ)
∧ (E(f[n];(x.(x * x) * x) o X[n]) = E(f[m];(x.(x * x) * x) o X[m]) ∈ ℚ)
∧ (E(f[n];(x.(x * x) * x * x) o X[n]) = E(f[m];(x.(x * x) * x * x) o 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:ℕn + 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:ℕn - 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:ℕm + 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 * x) o rv-partial-sum(n;i.X[i])) ≤ (B * n * n)))))) 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]))
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]))
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]))
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) = 1 ⇒ (a#C:p-open(p) ∨ b#C:p-open(p)) ⇒ (∃n:ℕ. ((C <n, random(p;a;b)>) = 1 ∈ ℤ)))
Home
Index