Commit 45c42398 authored by Gerwin Klein's avatar Gerwin Klein
Browse files

new entry Laws_of_Large_Numbers

parent b4869ef2d1ca
......@@ -10080,3 +10080,29 @@ abstract =
modeling the behavior of perfect logicians and formalize a solution of
the puzzle.
 
[Laws_of_Large_Numbers]
title = The Laws of Large Numbers
author = Manuel Eberl <https://www21.in.tum.de/~eberlm>
topic = Mathematics/Probability theory
date = 2021-02-10
notify = eberlm@in.tum.de
abstract =
<p>The Law of Large Numbers states that, informally, if one
performs a random experiment $X$ many times and takes the average of
the results, that average will be very close to the expected value
$E[X]$.</p> <p> More formally, let
$(X_i)_{i\in\mathbb{N}}$ be a sequence of independently identically
distributed random variables whose expected value $E[X_1]$ exists.
Denote the running average of $X_1, \ldots, X_n$ as $\overline{X}_n$.
Then:</p> <ul> <li>The Weak Law of Large Numbers
states that $\overline{X}_{n} \longrightarrow E[X_1]$ in probability
for $n\to\infty$, i.e. $\mathcal{P}(|\overline{X}_{n} - E[X_1]| >
\varepsilon) \longrightarrow 0$ as $n\to\infty$ for any $\varepsilon
> 0$.</li> <li>The Strong Law of Large Numbers states
that $\overline{X}_{n} \longrightarrow E[X_1]$ almost surely for
$n\to\infty$, i.e. $\mathcal{P}(\overline{X}_{n} \longrightarrow
E[X_1]) = 1$.</li> </ul> <p>In this entry, I
formally prove the strong law and from it the weak law. The approach
used for the proof of the strong law is a particularly quick and slick
one based on ergodic theory, which was formalised by Gouëzel in
another AFP entry.</p>
(*
File: Laws_of_Large_Numbers.thy
Author: Manuel Eberl, TU München
*)
section \<open>The Laws of Large Numbers\<close>
theory Laws_of_Large_Numbers
imports Ergodic_Theory.Ergodicity Shift_Operator
begin
text \<open>
We prove the strong law of large numbers in the following form: Let $(X_i)_{i\in\mathbb{N}}$
be a sequence of i.i.d. random variables over a probability space \<open>M\<close>. Further assume that
the expected value $E[X_0]$ of $X_0$ exists. Then the sequence of random variables
\[\overline{X}_n = \frac{1}{n} \sum_{i=0}^n X_i\]
of running averages almost surely converges to $E[X_0]$.
This means that
\[\mathcal{P}[\overline{X}_n \longrightarrow E[X_0]] = 1\ .\]
We start with the strong law.
\<close>
subsection \<open>The strong law\<close>
text \<open>
The proof uses Birkhoff's Theorem from Gouëzel's formalisation of ergodic theory~\cite{gouezel}
and the fact that the shift operator $T(x_1, x_2, x_3, \ldots) = (x_2, x_3, \ldots)$ is ergodic.
This proof can be found in various textbooks on probability theory/ergodic
theory, e.g. the ones by Krengel~\cite[p.~24]{krengel} and
Simmonet~\cite[Chapter 15, pp.~311--325]{Simonnet1996}.
\<close>
theorem (in prob_space) strong_law_of_large_numbers_iid:
fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> real"
assumes indep: "indep_vars (\<lambda>_. borel) X UNIV"
assumes distr: "\<And>i. distr M borel (X i) = distr M borel (X 0)"
assumes L1: "integrable M (X 0)"
shows "AE x in M. (\<lambda>n. (\<Sum>i<n. X i x) / n) \<longlonglongrightarrow> expectation (X 0)"
proof -
text \<open>
We adopt a more explicit view of \<^term>\<open>M\<close> as a countably infinite product of i.i.d.
random variables, indexed by the natural numbers:
\<close>
define M' :: "(nat \<Rightarrow> real) measure" where "M' = Pi\<^sub>M UNIV (\<lambda>i. distr M borel (X i))"
have [measurable]: "random_variable borel (X i)" for i
using indep by (auto simp: indep_vars_def)
have M'_eq: "M' = distr M (Pi\<^sub>M UNIV (\<lambda>i. borel)) (\<lambda>x. \<lambda>i\<in>UNIV. X i x)"
using indep unfolding M'_def by (subst (asm) indep_vars_iff_distr_eq_PiM) auto
have space_M': "space M' = UNIV"
by (simp add: M'_def space_PiM)
have sets_M' [measurable_cong]: "sets M' = sets (Pi\<^sub>M UNIV (\<lambda>i. borel))"
by (simp add: M'_eq)
interpret M': prob_space M'
unfolding M'_eq by (intro prob_space_distr) auto
text \<open>We introduce a shift operator that forgets the first variable in the sequence.\<close>
define T :: "(nat \<Rightarrow> real) \<Rightarrow> (nat \<Rightarrow> real)" where
"T = (\<lambda>f. f \<circ> Suc)"
have funpow_T: "(T ^^ i) = (\<lambda>f. f \<circ> (\<lambda>n. n + i))" for i
by (induction i) (auto simp: T_def)
interpret T: shift_operator_ergodic "distr M borel (X 0)" T M'
proof -
interpret X0: prob_space "distr M borel (X 0)"
by (rule prob_space_distr) auto
show "shift_operator_ergodic (distr M borel (X 0))"
by unfold_locales
show "M' \<equiv> Pi\<^sub>M UNIV (\<lambda>_. distr M borel (X 0)) "
unfolding M'_def by (subst distr)
qed (simp_all add: T_def)
have [intro]: "integrable M' (\<lambda>f. f 0)"
unfolding M'_eq by (subst integrable_distr_eq) (use L1 in auto)
have "AE f in M'. (\<lambda>n. T.birkhoff_sum (\<lambda>f. f 0) n f / real n)
\<longlonglongrightarrow> real_cond_exp M' T.Invariants (\<lambda>f. f 0) f"
by (rule T.birkhoff_theorem_AE_nonergodic) auto
moreover have "AE x in M'. real_cond_exp M' T.Invariants (\<lambda>f. f 0) x =
M'.expectation (\<lambda>f. f 0) / M'.prob (space M')"
by (intro T.Invariants_cond_exp_is_integral_fmpt) auto
ultimately have "AE f in M'. (\<lambda>n. T.birkhoff_sum (\<lambda>f. f 0) n f / real n)
\<longlonglongrightarrow> M'.expectation (\<lambda>f. f 0)"
by eventually_elim (simp_all add: M'.prob_space)
also have "M'.expectation (\<lambda>f. f 0) = expectation (X 0)"
unfolding M'_eq by (subst integral_distr) simp_all
also have "T.birkhoff_sum (\<lambda>f. f 0) = (\<lambda>n f. sum f {..<n})"
by (intro ext) (simp_all add:T.birkhoff_sum_def funpow_T)
finally show ?thesis
unfolding M'_eq by (subst (asm) AE_distr_iff) simp_all
qed
subsection \<open>The weak law\<close>
text \<open>
To go from the strong law to the weak one, we need the fact that almost sure convergence
implies convergence in probability. We prove this for sequences of random variables here.
\<close>
lemma (in prob_space) AE_convergence_imp_convergence_in_prob:
assumes [measurable]: "\<And>i. random_variable borel (X i)" "random_variable borel Y"
assumes AE: "AE x in M. (\<lambda>i. X i x) \<longlonglongrightarrow> Y x"
assumes "\<epsilon> > (0 :: real)"
shows "(\<lambda>i. prob {x\<in>space M. \<bar>X i x - Y x\<bar> > \<epsilon>}) \<longlonglongrightarrow> 0"
proof -
define A where "A = (\<lambda>i. {x\<in>space M. \<bar>X i x - Y x\<bar> > \<epsilon>})"
define B where "B = (\<lambda>n. (\<Union>i\<in>{n..}. A i))"
have [measurable]: "A i \<in> sets M" "B i \<in> sets M" for i
unfolding A_def B_def by measurable
have "AE x in M. x \<notin> (\<Inter>i. B i)"
using AE unfolding B_def A_def
by eventually_elim
(use \<open>\<epsilon> > 0\<close> in \<open>fastforce simp: tendsto_iff dist_norm eventually_at_top_linorder\<close>)
hence "(\<Inter>i. B i) \<in> null_sets M"
by (subst AE_iff_null_sets) auto
show "(\<lambda>i. prob (A i)) \<longlonglongrightarrow> 0"
proof (rule Lim_null_comparison)
have "(\<lambda>i. prob (B i)) \<longlonglongrightarrow> prob (\<Inter>i. B i)"
proof (rule finite_Lim_measure_decseq)
show "decseq B"
by (rule decseq_SucI) (force simp: B_def)
qed auto
also have "prob (\<Inter>i. B i) = 0"
using \<open>(\<Inter>i. B i) \<in> null_sets M\<close> by (simp add: measure_eq_0_null_sets)
finally show "(\<lambda>i. prob (B i)) \<longlonglongrightarrow> 0" .
next
have "prob (A n) \<le> prob (B n)" for n
unfolding B_def by (intro finite_measure_mono) auto
thus "\<forall>\<^sub>F n in at_top. norm (prob (A n)) \<le> prob (B n)"
by (intro always_eventually) auto
qed
qed
text \<open>
The weak law is now a simple corollary: we again have the same setting as before. The weak
law now states that $\overline{X}_n$ converges to $E[X_0]$ in probability. This means that
for any \<open>\<epsilon> > 0\<close>, the probability that $|\overline{X}_n - X_0| > \varepsilon$ vanishes as
\<open>n \<rightarrow> \<infinity>\<close>.
\<close>
corollary (in prob_space) weak_law_of_large_numbers_iid:
fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> real" and \<epsilon> :: real
assumes indep: "indep_vars (\<lambda>_. borel) X UNIV"
assumes distr: "\<And>i. distr M borel (X i) = distr M borel (X 0)"
assumes L1: "integrable M (X 0)"
assumes "\<epsilon> > 0"
shows "(\<lambda>n. prob {x\<in>space M. \<bar>(\<Sum>i<n. X i x) / n - expectation (X 0)\<bar> > \<epsilon>}) \<longlonglongrightarrow> 0"
proof (rule AE_convergence_imp_convergence_in_prob)
show "AE x in M. (\<lambda>n. (\<Sum>i<n. X i x) / n) \<longlonglongrightarrow> expectation (X 0)"
by (rule strong_law_of_large_numbers_iid) fact+
next
have [measurable]: "random_variable borel (X i)" for i
using indep by (auto simp: indep_vars_def)
show "random_variable borel (\<lambda>x. (\<Sum>i<n. X i x) / real n)" for n
by measurable
qed (use \<open>\<epsilon> > 0\<close> in simp_all)
end
\ No newline at end of file
(*
File: Laws_of_Large_Numbers.thy
Author: Manuel Eberl, TU München
*)
subsection \<open>Example\<close>
theory Laws_of_Large_Numbers_Example
imports Laws_of_Large_Numbers
begin
text \<open>
As an example, we apply the strong law to the proportion of successes in an independent sequence
of coin flips with success probability \<open>p\<close>. We will show that proportion of successful coin
flips among the first \<open>n\<close> attempts almost surely converges to \<open>p\<close> as \<open>n \<rightarrow> \<infinity>\<close>.
\<close>
(* TODO: Move *)
lemma (in prob_space) indep_vars_iff_distr_eq_PiM':
fixes I :: "'i set" and X :: "'i \<Rightarrow> 'a \<Rightarrow> 'b"
assumes "I \<noteq> {}"
assumes rv: "\<And>i. i \<in> I \<Longrightarrow> random_variable (M' i) (X i)"
shows "indep_vars M' X I \<longleftrightarrow>
distr M (\<Pi>\<^sub>M i\<in>I. M' i) (\<lambda>x. \<lambda>i\<in>I. X i x) = (\<Pi>\<^sub>M i\<in>I. distr M (M' i) (X i))"
proof -
from assms obtain j where j: "j \<in> I"
by auto
define N' where "N' = (\<lambda>i. if i \<in> I then M' i else M' j)"
define Y where "Y = (\<lambda>i. if i \<in> I then X i else X j)"
have rv: "random_variable (N' i) (Y i)" for i
using j by (auto simp: N'_def Y_def intro: assms)
have "indep_vars M' X I = indep_vars N' Y I"
by (intro indep_vars_cong) (auto simp: N'_def Y_def)
also have "\<dots> \<longleftrightarrow> distr M (\<Pi>\<^sub>M i\<in>I. N' i) (\<lambda>x. \<lambda>i\<in>I. Y i x) = (\<Pi>\<^sub>M i\<in>I. distr M (N' i) (Y i))"
by (intro indep_vars_iff_distr_eq_PiM rv assms)
also have "(\<Pi>\<^sub>M i\<in>I. N' i) = (\<Pi>\<^sub>M i\<in>I. M' i)"
by (intro PiM_cong) (simp_all add: N'_def)
also have "(\<lambda>x. \<lambda>i\<in>I. Y i x) = (\<lambda>x. \<lambda>i\<in>I. X i x)"
by (simp_all add: Y_def fun_eq_iff)
also have "(\<Pi>\<^sub>M i\<in>I. distr M (N' i) (Y i)) = (\<Pi>\<^sub>M i\<in>I. distr M (M' i) (X i))"
by (intro PiM_cong distr_cong) (simp_all add: N'_def Y_def)
finally show ?thesis .
qed
(* TODO: Move *)
lemma indep_vars_PiM_components:
assumes "\<And>i. i \<in> A \<Longrightarrow> prob_space (M i)"
shows "prob_space.indep_vars (PiM A M) M (\<lambda>i f. f i) A"
proof (cases "A = {}")
case False
have "distr (Pi\<^sub>M A M) (Pi\<^sub>M A M) (\<lambda>x. restrict x A) = distr (Pi\<^sub>M A M) (Pi\<^sub>M A M) (\<lambda>x. x)"
by (intro distr_cong) (auto simp: restrict_def space_PiM PiE_def extensional_def Pi_def)
also have "\<dots> = Pi\<^sub>M A M"
by simp
also have "\<dots> = Pi\<^sub>M A (\<lambda>i. distr (Pi\<^sub>M A M) (M i) (\<lambda>f. f i))"
by (intro PiM_cong refl, subst distr_PiM_component) (auto simp: assms)
finally show ?thesis
by (subst prob_space.indep_vars_iff_distr_eq_PiM') (simp_all add: prob_space_PiM assms False)
next
case True
interpret prob_space "PiM A M"
by (intro prob_space_PiM assms)
show ?thesis
unfolding indep_vars_def indep_sets_def by (auto simp: True)
qed
(* TODO: Move *)
lemma indep_vars_PiM_components':
assumes "\<And>i. i \<in> A \<Longrightarrow> prob_space (M i)"
assumes "\<And>i. i \<in> A \<Longrightarrow> g i \<in> M i \<rightarrow>\<^sub>M N i"
shows "prob_space.indep_vars (PiM A M) N (\<lambda>i f. g i (f i)) A"
by (rule prob_space.indep_vars_compose2[OF prob_space_PiM indep_vars_PiM_components])
(use assms in simp_all)
(* TODO: Move *)
lemma integrable_bernoulli_pmf [intro]:
fixes f :: "bool \<Rightarrow> 'a :: {banach, second_countable_topology}"
shows "integrable (bernoulli_pmf p) f"
by (rule integrable_measure_pmf_finite) auto
(* TODO: Move *)
lemma expectation_bernoulli_pmf:
fixes f :: "bool \<Rightarrow> 'a :: {banach, second_countable_topology}"
assumes p: "p \<in> {0..1}"
shows "measure_pmf.expectation (bernoulli_pmf p) f = p *\<^sub>R f True + (1 - p) *\<^sub>R f False"
using p by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
experiment
fixes p :: real
assumes p: "p \<in> {0..1}"
begin
definition M :: "(nat \<Rightarrow> bool) measure"
where "M = (\<Pi>\<^sub>M i\<in>(UNIV :: nat set). measure_pmf (bernoulli_pmf p))"
definition X :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> real"
where "X = (\<lambda>i f. if f i then 1 else 0)"
interpretation prob_space M
unfolding M_def by (intro prob_space_PiM measure_pmf.prob_space_axioms)
lemma random_variable_component: "random_variable (count_space UNIV) (\<lambda>f. f i)"
unfolding X_def M_def by measurable
lemma random_variable_X [measurable]: "random_variable borel (X i)"
unfolding X_def M_def by measurable
lemma distr_M_component: "distr M (count_space UNIV) (\<lambda>f. f i) = measure_pmf (bernoulli_pmf p)"
proof -
have "distr M (count_space UNIV) (\<lambda>f. f i) = distr M (measure_pmf (bernoulli_pmf p)) (\<lambda>f. f i)"
by (rule distr_cong) auto
also have "\<dots> = measure_pmf (bernoulli_pmf p)"
unfolding M_def by (subst distr_PiM_component) (simp_all add: measure_pmf.prob_space_axioms)
finally show ?thesis .
qed
lemma distr_M_X:
"distr M borel (X i) = distr (measure_pmf (bernoulli_pmf p)) borel (\<lambda>b. if b then 1 else 0)"
proof -
have "distr M borel (X i) = distr (distr M (count_space UNIV) (\<lambda>f. f i))
borel (\<lambda>b. if b then 1 else 0 :: real)"
by (subst distr_distr) (auto simp: M_def X_def o_def)
also note distr_M_component[of i]
finally show ?thesis
by simp
qed
lemma X_has_expectation: "integrable M (X 0)"
proof -
have "integrable (bernoulli_pmf p) (\<lambda>b. if b then 1 else 0 :: real)"
by auto
also have "measure_pmf (bernoulli_pmf p) = distr M (count_space UNIV) (\<lambda>f. f 0)"
by (simp add: distr_M_component)
also have "integrable \<dots> (\<lambda>b. if b then 1 else 0 :: real) = integrable M (X 0)"
unfolding X_def using random_variable_component by (subst integrable_distr_eq) auto
finally show ?thesis .
qed
lemma indep: "indep_vars (\<lambda>_. borel) X UNIV"
unfolding M_def X_def
by (rule indep_vars_PiM_components') (simp_all add: measure_pmf.prob_space_axioms)
lemma expectation_X: "expectation (X i) = p"
proof -
have "expectation (X i) =
lebesgue_integral (distr M (count_space UNIV) (\<lambda>f. f i)) (\<lambda>b. if b then 1 else 0 :: real)"
by (subst integral_distr) (simp_all add: random_variable_component X_def)
also have "distr M (count_space UNIV) (\<lambda>x. x i) = measure_pmf (bernoulli_pmf p)"
by (rule distr_M_component)
also have "measure_pmf.expectation (bernoulli_pmf p) (\<lambda>b. if b then 1 else 0 :: real) = p"
using p by (subst integral_bernoulli_pmf) auto
finally show ?thesis .
qed
theorem "AE f in M. (\<lambda>n. card {i. i < n \<and> f i} / n) \<longlonglongrightarrow> p"
proof -
have "AE f in M. (\<lambda>n. (\<Sum>i<n. X i f) / real n) \<longlonglongrightarrow> expectation (X 0)"
by (rule strong_law_of_large_numbers_iid)
(use indep X_has_expectation in \<open>simp_all add: distr_M_X\<close>)
also have "expectation (X 0) = p"
by (simp add: expectation_X)
also have "(\<lambda>x n. \<Sum>i<n. X i x) = (\<lambda>x n. \<Sum>i\<in>{i\<in>{..<n}. x i}. 1)"
by (intro ext sum.mono_neutral_cong_right) (auto simp: X_def)
also have "\<dots> = (\<lambda>x n. real (card {i. i < n \<and> x i}))"
by simp
finally show ?thesis .
qed
end
end
\ No newline at end of file
(*
File: ME_Library_Complement.thy
Author: Manuel Eberl, TU München
*)
section \<open>Auxiliary Material\<close>
theory ME_Library_Complement
imports "HOL-Analysis.Analysis"
begin
(* TODO: this file is redundent for AFP 2021 since it is then already in Ergodic_Theory *)
subsection \<open>The trivial measurable space\<close>
text \<open>
The trivial measurable space is the smallest possible \<open>\<sigma>\<close>-algebra, i.e. only the empty set
and everything.
\<close>
definition trivial_measure :: "'a set \<Rightarrow> 'a measure" where
"trivial_measure X = sigma X {{}, X}"
lemma space_trivial_measure [simp]: "space (trivial_measure X) = X"
by (simp add: trivial_measure_def)
lemma sets_trivial_measure: "sets (trivial_measure X) = {{}, X}"
by (simp add: trivial_measure_def sigma_algebra_trivial sigma_algebra.sigma_sets_eq)
lemma measurable_trivial_measure:
assumes "f \<in> space M \<rightarrow> X" and "f -` X \<inter> space M \<in> sets M"
shows "f \<in> M \<rightarrow>\<^sub>M trivial_measure X"
using assms unfolding measurable_def by (auto simp: sets_trivial_measure)
lemma measurable_trivial_measure_iff:
"f \<in> M \<rightarrow>\<^sub>M trivial_measure X \<longleftrightarrow> f \<in> space M \<rightarrow> X \<and> f -` X \<inter> space M \<in> sets M"
unfolding measurable_def by (auto simp: sets_trivial_measure)
subsection \<open>Pullback algebras\<close>
text \<open>
The pullback algebra $f^{-1}(\Sigma)$ of a \<open>\<sigma>\<close>-algebra $(\Omega, \Sigma)$ is the smallest
\<open>\<sigma>\<close>-algebra such that $f$ is $f^{-1}(\Sigma)$--$\Sigma$-measurable.
\<close>
definition (in sigma_algebra) pullback_algebra :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b set set" where
"pullback_algebra f \<Omega>' = sigma_sets \<Omega>' {f -` A \<inter> \<Omega>' |A. A \<in> M}"
lemma pullback_algebra_minimal:
assumes "f \<in> M \<rightarrow>\<^sub>M N"
shows "sets.pullback_algebra N f (space M) \<subseteq> sets M"
proof
fix X assume "X \<in> sets.pullback_algebra N f (space M)"
thus "X \<in> sets M"
unfolding sets.pullback_algebra_def
by induction (use assms in \<open>auto simp: measurable_def\<close>)
qed
lemma (in sigma_algebra) sigma_algebra_pullback: "sigma_algebra \<Omega>' (pullback_algebra f \<Omega>')"
unfolding pullback_algebra_def by (rule sigma_algebra_sigma_sets) auto
lemma (in sigma_algebra) in_pullback_algebra: "A \<in> M \<Longrightarrow> f -` A \<inter> \<Omega>' \<in> pullback_algebra f \<Omega>'"
unfolding pullback_algebra_def by (rule sigma_sets.Basic) auto
end
\ No newline at end of file
chapter AFP
session "Laws_of_Large_Numbers" (AFP) = "Ergodic_Theory" +
options [timeout = 600]
theories
Laws_of_Large_Numbers
Laws_of_Large_Numbers_Example
document_files
"root.tex"
"root.bib"
(*
File: Shift_Operator.thy
Author: Manuel Eberl, TU München
*)
section \<open>The shift operator on an infinite product measure\<close>
theory Shift_Operator
imports Ergodic_Theory.Ergodicity ME_Library_Complement
begin
text \<open>
Let \<open>P\<close> be an an infinite product of i.i.d. instances of the distribution \<open>M\<close>.
Then the shift operator is the map
\[T(x_0, x_1, x_2, \ldots) = T(x_1, x_2, \ldots)\ .\]
In this section, we define this operator and show that it is ergodic using Kolmogorov's
0--1 law.
\<close>
locale shift_operator_ergodic = prob_space +
fixes T :: "(nat \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a)" and P :: "(nat \<Rightarrow> 'a) measure"
defines "T \<equiv> (\<lambda>f. f \<circ> Suc)"
defines "P \<equiv> PiM (UNIV :: nat set) (\<lambda>_. M)"
begin
sublocale P: product_prob_space "\<lambda>_. M" UNIV
by unfold_locales
sublocale P: prob_space P
by (simp add: prob_space_PiM prob_space_axioms P_def)
lemma measurable_T [measurable]: "T \<in> P \<rightarrow>\<^sub>M P"
unfolding P_def T_def o_def
by (rule measurable_abs_UNIV[OF measurable_compose[OF measurable_component_singleton]]) auto
text \<open>
The \<open>n\<close>-th tail algebra $\mathcal{T}_n$ is, in some sense, the algebra in which we forget all
information about all $x_i$ with \<open>i < n\<close>. We simply change the product algebra of \<open>P\<close> by replacing
the algebra for each \<open>i < n\<close> with the trivial algebra that contains only the empty set and the
entire space.
\<close>
definition tail_algebra :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) measure"
where "tail_algebra n = PiM UNIV (\<lambda>i. if i < n then trivial_measure (space M) else M)"
lemma tail_algebra_0 [simp]: "tail_algebra 0 = P"
by (simp add: tail_algebra_def P_def)
lemma space_tail_algebra [simp]: "space (tail_algebra n) = PiE UNIV (\<lambda>_. space M)"
by (simp add: tail_algebra_def space_PiM PiE_def Pi_def)
lemma measurable_P_component [measurable]: "P.random_variable M (\<lambda>f. f i)"
unfolding P_def by measurable
lemma P_component [simp]: "distr P M (\<lambda>f. f i) = M"
unfolding P_def by (subst P.PiM_component) auto
lemma indep_vars: "P.indep_vars (\<lambda>_. M) (\<lambda>i f. f i) UNIV"
by (subst P.indep_vars_iff_distr_eq_PiM)
(simp_all add: restrict_def distr_id2 P.PiM_component P_def)
text \<open>
The shift operator takes us from $\mathcal{T}_n$ to $\mathcal{T}_{n+1}$ (it forgets the
information about one more variable):
\<close>
lemma measurable_T_tail: "T \<in> tail_algebra (Suc n) \<rightarrow>\<^sub>M tail_algebra n"
unfolding T_def tail_algebra_def o_def
by (rule measurable_abs_UNIV[OF measurable_compose[OF measurable_component_singleton]]) simp_all
lemma measurable_funpow_T: "T ^^ n \<in> tail_algebra (m + n) \<rightarrow>\<^sub>M tail_algebra m"
proof (induction n)
case (Suc n)
have "(T ^^ n) \<circ> T \<in> tail_algebra (m + Suc n) \<rightarrow>\<^sub>M tail_algebra m"
by (rule measurable_comp[OF _ Suc]) (simp_all add: measurable_T_tail)
thus ?case by (simp add: o_def funpow_swap1)
qed auto
lemma measurable_funpow_T': "T ^^ n \<in> tail_algebra n \<rightarrow>\<^sub>M P"
using measurable_funpow_T[of n 0] by simp
text \<open>
The shift operator is clearly measure-preserving:
\<close>
lemma measure_preserving: "T \<in> measure_preserving P P"
proof
fix A :: "(nat \<Rightarrow> 'a) set" assume "A \<in> P.events"
hence "emeasure P (T -` A \<inter> space P) = emeasure (distr P P T) A"
by (subst emeasure_distr) simp_all
also have "distr P P T = P" unfolding P_def T_def o_def
using distr_PiM_reindex[of UNIV "\<lambda>_. M" Suc UNIV] by (simp add: prob_space_axioms restrict_def)
finally show "emeasure P (T -` A \<inter> space P) = emeasure P A" .
qed auto
sublocale fmpt P T
by unfold_locales
(use measure_preserving in \<open>blast intro: measure_preserving_is_quasi_measure_preserving\<close>)+
text \<open>
Related to the tail algebra, we define the algebra induced by the \<open>i\<close>-th variable (i.e.
the algebra that contains only information about the \<open>i\<close>-th variable):
\<close>
sublocale X: sigma_algebra "space P" "sets.pullback_algebra M (\<lambda>f. f i) (space P)"
by (rule sets.sigma_algebra_pullback)
lemma indep_sets_pullback_algebra:
"P.indep_sets (\<lambda>i. sets.pullback_algebra M (\<lambda>f. f i) (space P)) UNIV"
using indep_vars unfolding P.indep_vars_def sets.pullback_algebra_def by blast
text \<open>
We can now show that the tail algebra $\mathcal{T}_n$ is a subalgebra of the algebra generated by the
algebras induced by all the variables \<open>x\<^sub>i\<close> with \<open>i \<ge> n\<close>:
\<close>
lemma tail_algebra_subset:
"sets (tail_algebra n) \<subseteq>
sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
proof -
have "sets (tail_algebra n) = sigma_sets (space P)
(prod_algebra UNIV (\<lambda>i. if i < n then trivial_measure (space M) else M))"
by (simp add: tail_algebra_def sets_PiM PiE_def Pi_def P_def space_PiM)
also have "\<dots> \<subseteq> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
proof (intro sigma_sets_mono subsetI)
fix C assume "C \<in> prod_algebra UNIV (\<lambda>i. if i < n then trivial_measure (space M) else M)"
then obtain C'
where C': "C = Pi\<^sub>E UNIV C'"
"C' \<in> (\<Pi> i\<in>UNIV. sets (if i < n then trivial_measure (space M) else M))"
by (elim prod_algebraE_all)
have C'_1: "C' i \<in> {{}, space M}" if "i < n" for i
using C'(2) that by (auto simp: Pi_def sets_trivial_measure split: if_splits)
have C'_2: "C' i \<in> sets M" if "i \<ge> n" for i
proof -
from that have "\<not>(i < n)"
by auto
with C'(2) show ?thesis
by (force simp: Pi_def sets_trivial_measure split: if_splits)
qed
have "C' i \<in> events" for i
using C'_1[of i] C'_2[of i] by (cases "i \<ge> n") auto
hence "C \<in> sets P"
unfolding P_def C'(1) by (intro sets_PiM_I_countable) auto
hence "C \<subseteq> space P"
using sets.sets_into_space by blast
show "C \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
proof (cases "C = {}")
case False
have "C = (\<Inter>i\<in>{n..}. (\<lambda>f. f i) -` C' i) \<inter> space P"
proof (intro equalityI subsetI, goal_cases)
case (1 f)
hence "f \<in> space P"
using 1 \<open>C \<subseteq> space P\<close> by blast
thus ?case
using C' 1 by (auto simp: Pi_def sets_trivial_measure split: if_splits)
next
case (2 f)
hence f: "f i \<in> C' i" if "i \<ge> n" for i
using that by auto
have "f i \<in> C' i" for i
proof (cases "i \<ge> n")
case True
thus ?thesis using C'_2[of i] f[of i] by auto
next
case False
thus ?thesis using C'_1[of i] C'(1) \<open>C \<noteq> {}\<close> 2
by (auto simp: P_def space_PiM)
qed
thus "f \<in> C"
using C' by auto
qed
also have "(\<Inter>i\<in>{n..}. (\<lambda>f. f i) -` C' i) \<inter> space P =
(\<Inter>i\<in>{n..}. (\<lambda>f. f i) -` C' i \<inter> space P)"
by blast
also have "\<dots> \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
(is "_ \<in> ?rhs")
proof (intro sigma_sets_INTER, goal_cases)
fix i show "(\<lambda>f. f i) -` C' i \<inter> space P \<in> ?rhs"
proof (cases "i \<ge> n")
case False
hence "C' i = {} \<or> C' i = space M"
using C'_1[of i] by auto
thus ?thesis
proof