Commit 9767b4a3 authored by Manuel Eberl's avatar Manuel Eberl
Browse files

Ergodic_Theory: ergodicity of the shift operator

parent 0b7b6eb56c31
......@@ -5768,6 +5768,7 @@ notify =
[Ergodic_Theory]
title = Ergodic Theory
author = Sebastien Gouezel <mailto:sebastien.gouezel@univ-rennes1.fr>
contributors = Manuel Eberl <https://www21.in.tum.de/~eberlm>
date = 2015-12-01
topic = Mathematics/Probability theory
abstract = Ergodic theory is the branch of mathematics that studies the behaviour of measure preserving transformations, in finite or infinite measure. It interacts both with probability theory (mainly through measure theory) and with geometry as a lot of interesting examples are from geometric origin. We implement the first definitions and theorems of ergodic theory, including notably Poicaré recurrence theorem for finite measure preserving systems (together with the notion of conservativity in general), induced maps, Kac's theorem, Birkhoff theorem (arguably the most important theorem in ergodic theory), and variations around it such as conservativity of the corresponding skew product, or Atkinson lemma.
......
......@@ -4,12 +4,14 @@ session "Ergodic_Theory" (AFP) = "HOL-Probability" +
options [timeout = 900]
theories
SG_Library_Complement
Trivial_Measure
Fekete
Asymptotic_Density
Measure_Preserving_Transformations
Recurrence
Invariants
Ergodicity
Shift_Operator
Kingman
Gouezel_Karlsson
Kohlberg_Neyman_Karlsson
......
(*
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 Ergodicity Trivial_Measure
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.induced_algebra M (\<lambda>f. f i) (space P)"
by (rule sets.sigma_algebra_induced)
lemma indep_sets_induced_algebra:
"P.indep_sets (\<lambda>i. sets.induced_algebra M (\<lambda>f. f i) (space P)) UNIV"
using indep_vars unfolding P.indep_vars_def sets.induced_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.induced_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.induced_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.induced_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.induced_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
assume [simp]: "C' i = space M"
have "space P \<subseteq> (\<lambda>f. f i) -` C' i"
by (auto simp: P_def space_PiM)
hence "(\<lambda>f. f i) -` C' i \<inter> space P = space P"
by blast
thus ?thesis using sigma_sets_top
by metis
qed (auto intro: sigma_sets.Empty)
next
case i: True
have "(\<lambda>f. f i) -` C' i \<inter> space P \<in> sets.induced_algebra M (\<lambda>f. f i) (space P)"
using C'_2[OF i] by (intro sets.in_induced_algebra) auto
thus ?thesis using i by blast
qed
next
have "C \<subseteq> space P" if "C \<in> sets.induced_algebra M (\<lambda>f. f i) (space P)" for i C
proof -
show ?thesis
by (rule sigma_sets_into_sp) (use that X.space_closed[of i] in auto)
qed
thus "(\<Union>i\<in>{n..}. sets.induced_algebra M (\<lambda>f. f i) (space P))\<subseteq> Pow (space P)"
by auto
qed auto
finally show ?thesis .
qed (auto simp: sigma_sets.Empty)
qed
finally show ?thesis .
qed
text \<open>
It now follows that the \<open>T\<close>-invariant events are a subset of the tail algebra induced
by the variables:
\<close>
lemma Invariants_subset_tail_algebra:
"sets Invariants \<subseteq> P.tail_events (\<lambda>i. sets.induced_algebra M (\<lambda>f. f i) (space P))"
proof
fix A assume A: "A \<in> sets Invariants"
have A': "A \<in> P.events"
using A unfolding Invariants_sets by simp_all
show "A \<in> P.tail_events (\<lambda>i. sets.induced_algebra M (\<lambda>f. f i) (space P))"
unfolding P.tail_events_def
proof safe
fix n :: nat
have "vimage_restr T A = A"
using A by (simp add: Invariants_vrestr)
hence "A = vimage_restr (T ^^ n) A"
using A' by (induction n) (simp_all add: vrestr_comp)
also have "vimage_restr (T ^^ n) A = (T ^^ n) -` (A \<inter> space P) \<inter> space P"
unfolding vimage_restr_def ..
also have "A \<inter> space P = A"
using A' by simp
also have "space P = space (tail_algebra n)"
by (simp add: P_def space_PiM)
also have "(T ^^ n) -` A \<inter> space (tail_algebra n) \<in> sets (tail_algebra n)"
by (rule measurable_sets[OF measurable_funpow_T' A'])
also have "sets (tail_algebra n) \<subseteq>
sigma_sets (space P) (\<Union>i\<in>{n..}. sets.induced_algebra M (\<lambda>f. f i) (space P))"
by (rule tail_algebra_subset)
finally show "A \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.induced_algebra M (\<lambda>f. f i) (space P))" .
qed
qed
text \<open>
A simple invocation of Kolmogorov's 0--1 law now proves that \<open>T\<close> is indeed ergodic:
\<close>
sublocale ergodic_fmpt P T
proof
fix A assume A: "A \<in> sets Invariants"
have A': "A \<in> P.events"
using A unfolding Invariants_sets by simp_all
have "P.prob A = 0 \<or> P.prob A = 1"
using X.sigma_algebra_axioms indep_sets_induced_algebra
by (rule P.kolmogorov_0_1_law) (use A Invariants_subset_tail_algebra in blast)
thus "A \<in> null_sets P \<or> space P - A \<in> null_sets P"
by (rule disj_forward) (use A'(1) P.prob_compl[of A] in \<open>auto simp: P.emeasure_eq_measure\<close>)
qed
end
end
\ No newline at end of file
(*
File: Trivial_Measure.thy
Author: Manuel Eberl, TU München
*)
theory Trivial_Measure
imports "HOL-Analysis.Analysis"
begin
(* TODO: could be put in the distribution *)
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)
definition (in sigma_algebra) induced_algebra :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'b set set" where
"induced_algebra f \<Omega>' = sigma_sets \<Omega>' {f -` A \<inter> \<Omega>' |A. A \<in> M}"
lemma (in sigma_algebra) sigma_algebra_induced: "sigma_algebra \<Omega>' (induced_algebra f \<Omega>')"
unfolding induced_algebra_def by (rule sigma_algebra_sigma_sets) auto
lemma (in sigma_algebra) in_induced_algebra: "A \<in> M \<Longrightarrow> f -` A \<inter> \<Omega>' \<in> induced_algebra f \<Omega>'"
unfolding induced_algebra_def by (rule sigma_sets.Basic) auto
end
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment