diff --git a/thys/Laws_of_Large_Numbers/Laws_of_Large_Numbers.thy b/thys/Laws_of_Large_Numbers/Laws_of_Large_Numbers.thy
--- a/thys/Laws_of_Large_Numbers/Laws_of_Large_Numbers.thy
+++ b/thys/Laws_of_Large_Numbers/Laws_of_Large_Numbers.thy
@@ -1,156 +1,156 @@
 (*
    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
+  imports Ergodic_Theory.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 
+  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
diff --git a/thys/Laws_of_Large_Numbers/ME_Library_Complement.thy b/thys/Laws_of_Large_Numbers/ME_Library_Complement.thy
deleted file mode 100644
--- a/thys/Laws_of_Large_Numbers/ME_Library_Complement.thy
+++ /dev/null
@@ -1,62 +0,0 @@
-(*
-   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
diff --git a/thys/Laws_of_Large_Numbers/Shift_Operator.thy b/thys/Laws_of_Large_Numbers/Shift_Operator.thy
deleted file mode 100644
--- a/thys/Laws_of_Large_Numbers/Shift_Operator.thy
+++ /dev/null
@@ -1,268 +0,0 @@
-(*
-   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
-            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.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.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.pullback_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.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.pullback_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.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.pullback_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_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>)
-qed
-
-end
-
-end
\ No newline at end of file