This instance will be upgraded to Heptapod 0.23.2 on 2021-08-05 at 11:00 UTC+2 (a few minutes of down time)

Commit 6f3b431f authored by Manuel Eberl's avatar Manuel Eberl
Browse files

Ergodic_Theory: tuned some names

parent 24b6785e3e55
(*
File: Trivial_Measure.thy
File: ME_Library_Complement.thy
Author: Manuel Eberl, TU München
*)
theory Trivial_Measure
theory ME_Library_Complement
imports "HOL-Analysis.Analysis"
begin
......@@ -33,13 +33,29 @@ lemma measurable_trivial_measure_iff:
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}"
subsection \<open>Pullback algebras\<close>
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
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
......@@ -4,7 +4,7 @@ session "Ergodic_Theory" (AFP) = "HOL-Probability" +
options [timeout = 900]
theories
SG_Library_Complement
Trivial_Measure
ME_Library_Complement
Fekete
Asymptotic_Density
Measure_Preserving_Transformations
......
......@@ -4,7 +4,7 @@
*)
section \<open>The shift operator on an infinite product measure\<close>
theory Shift_Operator
imports Ergodicity Trivial_Measure
imports Ergodicity ME_Library_Complement
begin
text \<open>
......@@ -33,9 +33,9 @@ lemma measurable_T [measurable]: "T \<in> P \<rightarrow>\<^sub>M P"
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
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"
......@@ -100,12 +100,12 @@ 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)
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_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
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>
......@@ -114,13 +114,13 @@ text \<open>
\<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))"
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.induced_algebra M (\<lambda>f. f i) (space P))"
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'
......@@ -143,7 +143,7 @@ proof -
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))"
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"
......@@ -174,7 +174,7 @@ proof -
(\<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))"
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"
......@@ -194,17 +194,17 @@ proof -
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
have "(\<lambda>f. f i) -` C' i \<inter> space P \<in> sets.pullback_algebra M (\<lambda>f. f i) (space P)"
using C'_2[OF i] by (intro sets.in_pullback_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
have "C \<subseteq> space P" if "C \<in> sets.pullback_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)"
thus "(\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))\<subseteq> Pow (space P)"
by auto
qed auto
......@@ -220,12 +220,12 @@ text \<open>
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))"
"sets Invariants \<subseteq> P.tail_events (\<lambda>i. sets.pullback_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))"
show "A \<in> P.tail_events (\<lambda>i. sets.pullback_algebra M (\<lambda>f. f i) (space P))"
unfolding P.tail_events_def
proof safe
fix n :: nat
......@@ -242,9 +242,9 @@ proof
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))"
sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_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))" .
finally show "A \<in> sigma_sets (space P) (\<Union>i\<in>{n..}. sets.pullback_algebra M (\<lambda>f. f i) (space P))" .
qed
qed
......@@ -257,7 +257,7 @@ proof
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
using X.sigma_algebra_axioms indep_sets_pullback_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>)
......
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