Theory Shift_Operator
section ‹The shift operator on an infinite product measure›
theory Shift_Operator
imports Ergodicity ME_Library_Complement
begin
text ‹
Let ‹P› be an an infinite product of i.i.d. instances of the distribution ‹M›.
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.
›
locale shift_operator_ergodic = prob_space +
fixes T :: "(nat ⇒ 'a) ⇒ (nat ⇒ 'a)" and P :: "(nat ⇒ 'a) measure"
defines "T ≡ (λf. f ∘ Suc)"
defines "P ≡ PiM (UNIV :: nat set) (λ_. M)"
begin
sublocale P: product_prob_space "λ_. 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 ∈ P →⇩M P"
unfolding P_def T_def o_def
by (rule measurable_abs_UNIV[OF measurable_compose[OF measurable_component_singleton]]) auto
text ‹
The ‹n›-th tail algebra $\mathcal{T}_n$ is, in some sense, the algebra in which we forget all
information about all $x_i$ with ‹i < n›. We simply change the product algebra of ‹P› by replacing
the algebra for each ‹i < n› with the trivial algebra that contains only the empty set and the
entire space.
›
definition tail_algebra :: "nat ⇒ (nat ⇒ 'a) measure"
where "tail_algebra n = PiM UNIV (λ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 (λ_. space M)"
by (simp add: tail_algebra_def space_PiM PiE_def Pi_def)
lemma measurable_P_component [measurable]: "P.random_variable M (λf. f i)"
unfolding P_def by measurable
lemma P_component [simp]: "distr P M (λf. f i) = M"
unfolding P_def by (subst P.PiM_component) auto
lemma indep_vars: "P.indep_vars (λ_. M) (λ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 ‹
The shift operator takes us from $\mathcal{T}_n$ to $\mathcal{T}_{n+1}$ (it forgets the
information about one more variable):
›
lemma measurable_T_tail: "T ∈ tail_algebra (Suc n) →⇩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 ∈ tail_algebra (m + n) →⇩M tail_algebra m"
proof (induction n)
case (Suc n)
have "(T ^^ n) ∘ T ∈ tail_algebra (m + Suc n) →⇩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 ∈ tail_algebra n →⇩M P"
using measurable_funpow_T[of n 0] by simp
text ‹
The shift operator is clearly measure-preserving:
›
lemma measure_preserving: "T ∈ measure_preserving P P"
proof
fix A :: "(nat ⇒ 'a) set" assume "A ∈ P.events"
hence "emeasure P (T -` A ∩ 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 "λ_. M" Suc UNIV] by (simp add: prob_space_axioms restrict_def)
finally show "emeasure P (T -` A ∩ space P) = emeasure P A" .
qed auto
sublocale fmpt P T
by unfold_locales
(use measure_preserving in ‹blast intro: measure_preserving_is_quasi_measure_preserving›)+
lemma indep_sets_vimage_algebra:
"P.indep_sets (λi. sets (vimage_algebra (space P) (λf. f i) M)) UNIV"
using indep_vars unfolding P.indep_vars_def sets_vimage_algebra by blast
text ‹
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 ‹x⇩i› with ‹i ≥ n›:
›
lemma tail_algebra_subset:
"sets (tail_algebra n) ⊆
sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))"
proof -
have "sets (tail_algebra n) = sigma_sets (space P)
(prod_algebra UNIV (λ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 "… ⊆ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))"
proof (intro sigma_sets_mono subsetI)
fix C assume "C ∈ prod_algebra UNIV (λi. if i < n then trivial_measure (space M) else M)"
then obtain C'
where C': "C = Pi⇩E UNIV C'"
"C' ∈ (Π i∈UNIV. sets (if i < n then trivial_measure (space M) else M))"
by (elim prod_algebraE_all)
have C'_1: "C' i ∈ {{}, 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 ∈ sets M" if "i ≥ n" for i
proof -
from that have "¬(i < n)"
by auto
with C'(2) show ?thesis
by (force simp: Pi_def sets_trivial_measure split: if_splits)
qed
have "C' i ∈ events" for i
using C'_1[of i] C'_2[of i] by (cases "i ≥ n") auto
hence "C ∈ sets P"
unfolding P_def C'(1) by (intro sets_PiM_I_countable) auto
hence "C ⊆ space P"
using sets.sets_into_space by blast
show "C ∈ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))"
proof (cases "C = {}")
case False
have "C = (⋂i∈{n..}. (λf. f i) -` C' i) ∩ space P"
proof (intro equalityI subsetI, goal_cases)
case (1 f)
hence "f ∈ space P"
using 1 ‹C ⊆ space P› 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 ∈ C' i" if "i ≥ n" for i
using that by auto
have "f i ∈ C' i" for i
proof (cases "i ≥ 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) ‹C ≠ {}› 2
by (auto simp: P_def space_PiM)
qed
thus "f ∈ C"
using C' by auto
qed
also have "(⋂i∈{n..}. (λf. f i) -` C' i) ∩ space P =
(⋂i∈{n..}. (λf. f i) -` C' i ∩ space P)"
by blast
also have "… ∈ sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))"
(is "_ ∈ ?rhs")
proof (intro sigma_sets_INTER, goal_cases)
fix i show "(λf. f i) -` C' i ∩ space P ∈ ?rhs"
proof (cases "i ≥ n")
case False
hence "C' i = {} ∨ C' i = space M"
using C'_1[of i] by auto
thus ?thesis
proof
assume [simp]: "C' i = space M"
have "space P ⊆ (λf. f i) -` C' i"
by (auto simp: P_def space_PiM)
hence "(λf. f i) -` C' i ∩ 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 "(λf. f i) -` C' i ∩ space P ∈ sets (vimage_algebra (space P) (λf. f i) M)"
using C'_2[OF i] by (blast intro: in_vimage_algebra)
thus ?thesis using i by blast
qed
next
have "C ⊆ space P" if "C ∈ sets (vimage_algebra (space P) (λf. f i) M)" for i C
using sets.sets_into_space[OF that] by simp
thus "(⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M)) ⊆ Pow (space P)"
by auto
qed auto
finally show ?thesis .
qed (auto simp: sigma_sets.Empty)
qed
finally show ?thesis .
qed
text ‹
It now follows that the ‹T›-invariant events are a subset of the tail algebra induced
by the variables:
›
lemma Invariants_subset_tail_algebra:
"sets Invariants ⊆ P.tail_events (λi. sets (vimage_algebra (space P) (λf. f i) M))"
proof
fix A assume A: "A ∈ sets Invariants"
have A': "A ∈ P.events"
using A unfolding Invariants_sets by simp_all
show "A ∈ P.tail_events (λi. sets (vimage_algebra (space P) (λf. f i) M))"
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 ∩ space P) ∩ space P"
unfolding vimage_restr_def ..
also have "A ∩ 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 ∩ space (tail_algebra n) ∈ sets (tail_algebra n)"
by (rule measurable_sets[OF measurable_funpow_T' A'])
also have "sets (tail_algebra n) ⊆
sigma_sets (space P) (⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))"
by (rule tail_algebra_subset)
finally show "A ∈ sigma_sets (space P)
(⋃i∈{n..}. sets (vimage_algebra (space P) (λf. f i) M))" .
qed
qed
text ‹
A simple invocation of Kolmogorov's 0--1 law now proves that ‹T› is indeed ergodic:
›
sublocale ergodic_fmpt P T
proof
fix A assume A: "A ∈ sets Invariants"
have A': "A ∈ P.events"
using A unfolding Invariants_sets by simp_all
have "sigma_algebra (space P) (sets (vimage_algebra (space P) (λf. f i) M))" for i
by (metis sets.sigma_algebra_axioms space_vimage_algebra)
hence "P.prob A = 0 ∨ P.prob A = 1"
using indep_sets_vimage_algebra
by (rule P.kolmogorov_0_1_law) (use A Invariants_subset_tail_algebra in blast)
thus "A ∈ null_sets P ∨ space P - A ∈ null_sets P"
by (rule disj_forward) (use A'(1) P.prob_compl[of A] in ‹auto simp: P.emeasure_eq_measure›)
qed
end
end