[STATEMENT]
lemma (in ergodic_qmpt) Invariant_func_is_AE_constant:
  fixes f::"_\<Rightarrow> 'b::{second_countable_topology, t1_space}"
  assumes "f \<in> borel_measurable Invariants"
  shows "\<exists>y. AE x in M. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. AE x in M. f x = y
 2. \<not> ?P \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
assume "space M \<in> null_sets M"
[PROOF STATE]
proof (state)
this:
space M \<in> null_sets M

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. AE x in M. f x = y
 2. \<not> ?P \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
obtain y::'b where "True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (True \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
True

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. AE x in M. f x = y
 2. \<not> ?P \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "AE x in M. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. f x = y
[PROOF STEP]
using \<open>space M \<in> null_sets M\<close> AE_I'
[PROOF STATE]
proof (prove)
using this:
space M \<in> null_sets M
\<lbrakk>?N \<in> null_sets ?M; {x \<in> space ?M. \<not> ?P x} \<subseteq> ?N\<rbrakk> \<Longrightarrow> almost_everywhere ?M ?P

goal (1 subgoal):
 1. AE x in M. f x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AE x in M. f x = y

goal (2 subgoals):
 1. ?P \<Longrightarrow> \<exists>y. AE x in M. f x = y
 2. \<not> ?P \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. f x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. f x = y

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. AE x in M. f x = y

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
assume *: "\<not>(space M \<in> null_sets M)"
[PROOF STATE]
proof (state)
this:
space M \<notin> null_sets M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
obtain B::"'b set set" where B: "countable B" "topological_basis B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. \<lbrakk>countable B; topological_basis B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_countable_basis
[PROOF STATE]
proof (prove)
using this:
\<exists>B. countable B \<and> topological_basis B

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>countable B; topological_basis B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
countable B
topological_basis B

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
define C where "C = {b \<in> B. space M - f-`b \<in> null_sets M}"
[PROOF STATE]
proof (state)
this:
C = {b \<in> B. space M - f -` b \<in> null_sets M}

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C = {b \<in> B. space M - f -` b \<in> null_sets M}
[PROOF STEP]
have "countable C"
[PROOF STATE]
proof (prove)
using this:
C = {b \<in> B. space M - f -` b \<in> null_sets M}

goal (1 subgoal):
 1. countable C
[PROOF STEP]
using \<open>countable B\<close>
[PROOF STATE]
proof (prove)
using this:
C = {b \<in> B. space M - f -` b \<in> null_sets M}
countable B

goal (1 subgoal):
 1. countable C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
countable C

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
define Y where "Y = \<Inter> C"
[PROOF STATE]
proof (state)
this:
Y = \<Inter> C

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "space M - f-`Y = (\<Union> b\<in> C. space M - f-`b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space M - f -` Y = (\<Union>b\<in>C. space M - f -` b)
[PROOF STEP]
unfolding Y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space M - f -` \<Inter> C = (\<Union>b\<in>C. space M - f -` b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space M - f -` Y = (\<Union>b\<in>C. space M - f -` b)

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
space M - f -` Y = (\<Union>b\<in>C. space M - f -` b)

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "\<And>b. b \<in> C \<Longrightarrow> space M - f-`b \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. b \<in> C \<Longrightarrow> space M - f -` b \<in> null_sets M
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. b \<in> {b \<in> B. space M - f -` b \<in> null_sets M} \<Longrightarrow> space M - f -` b \<in> null_sets M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?b3 \<in> C \<Longrightarrow> space M - f -` ?b3 \<in> null_sets M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
space M - f -` Y = (\<Union>b\<in>C. space M - f -` b)
?b3 \<in> C \<Longrightarrow> space M - f -` ?b3 \<in> null_sets M
[PROOF STEP]
have i: "space M - f-`Y \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
space M - f -` Y = (\<Union>b\<in>C. space M - f -` b)
?b3 \<in> C \<Longrightarrow> space M - f -` ?b3 \<in> null_sets M

goal (1 subgoal):
 1. space M - f -` Y \<in> null_sets M
[PROOF STEP]
using \<open>countable C\<close>
[PROOF STATE]
proof (prove)
using this:
space M - f -` Y = (\<Union>b\<in>C. space M - f -` b)
?b3 \<in> C \<Longrightarrow> space M - f -` ?b3 \<in> null_sets M
countable C

goal (1 subgoal):
 1. space M - f -` Y \<in> null_sets M
[PROOF STEP]
by (metis null_sets_UN')
[PROOF STATE]
proof (state)
this:
space M - f -` Y \<in> null_sets M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
space M - f -` Y \<in> null_sets M
[PROOF STEP]
have "f-`Y \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
space M - f -` Y \<in> null_sets M

goal (1 subgoal):
 1. f -` Y \<noteq> {}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
space M - f -` Y \<in> null_sets M
space M \<notin> null_sets M

goal (1 subgoal):
 1. f -` Y \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f -` Y \<noteq> {}

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f -` Y \<noteq> {}
[PROOF STEP]
have "Y \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
f -` Y \<noteq> {}

goal (1 subgoal):
 1. Y \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Y \<noteq> {}

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Y \<noteq> {}
[PROOF STEP]
obtain y where "y \<in> Y"
[PROOF STATE]
proof (prove)
using this:
Y \<noteq> {}

goal (1 subgoal):
 1. (\<And>y. y \<in> Y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> Y

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
define D where "D = {b \<in> B. y\<notin>b \<and> f-`b \<inter> space M \<in> null_sets M}"
[PROOF STATE]
proof (state)
this:
D = {b \<in> B. y \<notin> b \<and> f -` b \<inter> space M \<in> null_sets M}

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "countable D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. countable D
[PROOF STEP]
using \<open>countable B\<close> D_def
[PROOF STATE]
proof (prove)
using this:
countable B
D = {b \<in> B. y \<notin> b \<and> f -` b \<inter> space M \<in> null_sets M}

goal (1 subgoal):
 1. countable D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
countable D

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
countable D

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
assume "z \<noteq> y"
[PROOF STATE]
proof (state)
this:
z \<noteq> y

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
obtain U where U: "open U" "z \<in> U" "y \<notin> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U. \<lbrakk>open U; z \<in> U; y \<notin> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using t1_space[OF \<open>z \<noteq> y\<close>]
[PROOF STATE]
proof (prove)
using this:
\<exists>U. open U \<and> z \<in> U \<and> y \<notin> U

goal (1 subgoal):
 1. (\<And>U. \<lbrakk>open U; z \<in> U; y \<notin> U\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
open U
z \<in> U
y \<notin> U

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
obtain V where "V \<in> B" "V \<subseteq> U" "z \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V. \<lbrakk>V \<in> B; V \<subseteq> U; z \<in> V\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule topological_basisE[OF \<open>topological_basis B\<close> \<open>open U\<close> \<open>z \<in> U\<close>])
[PROOF STATE]
proof (state)
this:
V \<in> B
V \<subseteq> U
z \<in> V

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V \<in> B
V \<subseteq> U
z \<in> V
[PROOF STEP]
have "y \<notin> V"
[PROOF STATE]
proof (prove)
using this:
V \<in> B
V \<subseteq> U
z \<in> V

goal (1 subgoal):
 1. y \<notin> V
[PROOF STEP]
using U
[PROOF STATE]
proof (prove)
using this:
V \<in> B
V \<subseteq> U
z \<in> V
open U
z \<in> U
y \<notin> U

goal (1 subgoal):
 1. y \<notin> V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<notin> V

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<notin> V
[PROOF STEP]
have "V \<notin> C"
[PROOF STATE]
proof (prove)
using this:
y \<notin> V

goal (1 subgoal):
 1. V \<notin> C
[PROOF STEP]
using \<open>y \<in> Y\<close> Y_def
[PROOF STATE]
proof (prove)
using this:
y \<notin> V
y \<in> Y
Y = \<Inter> C

goal (1 subgoal):
 1. V \<notin> C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<notin> C

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V \<notin> C
[PROOF STEP]
have "space M - f-`V \<inter> space M \<notin> null_sets M"
[PROOF STATE]
proof (prove)
using this:
V \<notin> C

goal (1 subgoal):
 1. space M - f -` V \<inter> space M \<notin> null_sets M
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
using this:
V \<notin> {b \<in> B. space M - f -` b \<in> null_sets M}

goal (1 subgoal):
 1. space M - f -` V \<inter> space M \<notin> null_sets M
[PROOF STEP]
using \<open>V \<in> B\<close>
[PROOF STATE]
proof (prove)
using this:
V \<notin> {b \<in> B. space M - f -` b \<in> null_sets M}
V \<in> B

goal (1 subgoal):
 1. space M - f -` V \<inter> space M \<notin> null_sets M
[PROOF STEP]
by (metis (no_types, lifting) Diff_Int2 inf.idem mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
space M - f -` V \<inter> space M \<notin> null_sets M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
space M - f -` V \<inter> space M \<notin> null_sets M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "f-`V \<inter> space M \<in> sets Invariants"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f -` V \<inter> space M \<in> sets Invariants
[PROOF STEP]
using measurable_sets[OF assms borel_open[OF topological_basis_open[OF B(2) \<open>V \<in> B\<close>]]] subalgebra_def Invariants_is_subalg
[PROOF STATE]
proof (prove)
using this:
f -` V \<inter> space Invariants \<in> sets Invariants
subalgebra ?M ?F = (space ?F = space ?M \<and> sets ?F \<subseteq> sets ?M)
subalgebra M Invariants

goal (1 subgoal):
 1. f -` V \<inter> space M \<in> sets Invariants
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f -` V \<inter> space M \<in> sets Invariants

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
space M - f -` V \<inter> space M \<notin> null_sets M
f -` V \<inter> space M \<in> sets Invariants
[PROOF STEP]
have "f-`V \<inter> space M \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
space M - f -` V \<inter> space M \<notin> null_sets M
f -` V \<inter> space M \<in> sets Invariants

goal (1 subgoal):
 1. f -` V \<inter> space M \<in> null_sets M
[PROOF STEP]
using ergodic
[PROOF STATE]
proof (prove)
using this:
space M - f -` V \<inter> space M \<notin> null_sets M
f -` V \<inter> space M \<in> sets Invariants
?A \<in> sets Invariants \<Longrightarrow> ?A \<in> null_sets M \<or> space M - ?A \<in> null_sets M

goal (1 subgoal):
 1. f -` V \<inter> space M \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f -` V \<inter> space M \<in> null_sets M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f -` V \<inter> space M \<in> null_sets M
[PROOF STEP]
have "V \<in> D"
[PROOF STATE]
proof (prove)
using this:
f -` V \<inter> space M \<in> null_sets M

goal (1 subgoal):
 1. V \<in> D
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
using this:
f -` V \<inter> space M \<in> null_sets M

goal (1 subgoal):
 1. V \<in> {b \<in> B. y \<notin> b \<and> f -` b \<inter> space M \<in> null_sets M}
[PROOF STEP]
using \<open>V \<in> B\<close> \<open>y \<notin> V\<close>
[PROOF STATE]
proof (prove)
using this:
f -` V \<inter> space M \<in> null_sets M
V \<in> B
y \<notin> V

goal (1 subgoal):
 1. V \<in> {b \<in> B. y \<notin> b \<and> f -` b \<inter> space M \<in> null_sets M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V \<in> D

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
V \<in> D
[PROOF STEP]
have "\<exists>b \<in> D. z \<in> b"
[PROOF STATE]
proof (prove)
using this:
V \<in> D

goal (1 subgoal):
 1. \<exists>b\<in>D. z \<in> b
[PROOF STEP]
using \<open>z \<in> V\<close>
[PROOF STATE]
proof (prove)
using this:
V \<in> D
z \<in> V

goal (1 subgoal):
 1. \<exists>b\<in>D. z \<in> b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>b\<in>D. z \<in> b

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?z5 \<noteq> y \<Longrightarrow> \<exists>b\<in>D. ?z5 \<in> b

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?z5 \<noteq> y \<Longrightarrow> \<exists>b\<in>D. ?z5 \<in> b
[PROOF STEP]
have *: "\<Union>D = UNIV - {y}"
[PROOF STATE]
proof (prove)
using this:
?z5 \<noteq> y \<Longrightarrow> \<exists>b\<in>D. ?z5 \<in> b

goal (1 subgoal):
 1. \<Union> D = UNIV - {y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>X. \<lbrakk>\<And>z. z \<noteq> y \<Longrightarrow> \<exists>x\<in>D. z \<in> x; y \<in> X; X \<in> D\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>X. \<lbrakk>\<And>z. z \<noteq> y \<Longrightarrow> \<exists>x\<in>{b \<in> B. y \<notin> b \<and> f -` b \<inter> space M \<in> null_sets M}. z \<in> x; y \<in> X; X \<in> {b \<in> B. y \<notin> b \<and> f -` b \<inter> space M \<in> null_sets M}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> D = UNIV - {y}

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "space M - f-`{y} = f-`(UNIV -{y}) \<inter> space M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. space M - f -` {y} = f -` (UNIV - {y}) \<inter> space M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
space M - f -` {y} = f -` (UNIV - {y}) \<inter> space M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
space M - f -` {y} = f -` (UNIV - {y}) \<inter> space M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "... = (\<Union>b\<in>D. f-`b \<inter> space M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f -` (UNIV - {y}) \<inter> space M = (\<Union>b\<in>D. f -` b \<inter> space M)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<Union> D = UNIV - {y}

goal (1 subgoal):
 1. f -` (UNIV - {y}) \<inter> space M = (\<Union>b\<in>D. f -` b \<inter> space M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f -` (UNIV - {y}) \<inter> space M = (\<Union>b\<in>D. f -` b \<inter> space M)

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f -` (UNIV - {y}) \<inter> space M = (\<Union>b\<in>D. f -` b \<inter> space M)

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "... \<in> null_sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>b\<in>D. f -` b \<inter> space M) \<in> null_sets M
[PROOF STEP]
using D_def \<open>countable D\<close>
[PROOF STATE]
proof (prove)
using this:
D = {b \<in> B. y \<notin> b \<and> f -` b \<inter> space M \<in> null_sets M}
countable D

goal (1 subgoal):
 1. (\<Union>b\<in>D. f -` b \<inter> space M) \<in> null_sets M
[PROOF STEP]
by (metis (no_types, lifting) mem_Collect_eq null_sets_UN')
[PROOF STATE]
proof (state)
this:
(\<Union>b\<in>D. f -` b \<inter> space M) \<in> null_sets M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
space M - f -` {y} \<in> null_sets M
[PROOF STEP]
have "space M - f-`{y} \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
space M - f -` {y} \<in> null_sets M

goal (1 subgoal):
 1. space M - f -` {y} \<in> null_sets M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
space M - f -` {y} \<in> null_sets M

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
with AE_not_in[OF this]
[PROOF STATE]
proof (chain)
picking this:
AE x in M. x \<notin> space M - f -` {y}
space M - f -` {y} \<in> null_sets M
[PROOF STEP]
have "AE x in M. x \<in> f-`{y}"
[PROOF STATE]
proof (prove)
using this:
AE x in M. x \<notin> space M - f -` {y}
space M - f -` {y} \<in> null_sets M

goal (1 subgoal):
 1. AE x in M. x \<in> f -` {y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. x \<in> f -` {y}

goal (1 subgoal):
 1. space M \<notin> null_sets M \<Longrightarrow> \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. x \<in> f -` {y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. x \<in> f -` {y}

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. AE x in M. f x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_qmpt) AE_Invariant_func_is_AE_constant:
  fixes f::"_ \<Rightarrow> 'b::{second_countable_topology, t2_space}"
  assumes "f \<in> borel_measurable M" "AE x in M. f(T x) = f x"
  shows "\<exists>y. AE x in M. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
obtain g where g: "g \<in> borel_measurable Invariants" "AE x in M. f x = g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> borel_measurable Invariants; AE x in M. f x = g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Invariants_quasi_Invariants_functions[OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
(\<exists>g\<in>borel_measurable Invariants. AE x in M. f x = g x) = (AE x in M. f (T x) = f x)
AE x in M. f (T x) = f x

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> borel_measurable Invariants; AE x in M. f x = g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> borel_measurable Invariants
AE x in M. f x = g x

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in> borel_measurable Invariants
AE x in M. f x = g x
[PROOF STEP]
obtain y where y: "AE x in M. g x = y"
[PROOF STATE]
proof (prove)
using this:
g \<in> borel_measurable Invariants
AE x in M. f x = g x

goal (1 subgoal):
 1. (\<And>y. AE x in M. g x = y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Invariant_func_is_AE_constant
[PROOF STATE]
proof (prove)
using this:
g \<in> borel_measurable Invariants
AE x in M. f x = g x
?f \<in> borel_measurable Invariants \<Longrightarrow> \<exists>y. AE x in M. ?f x = y

goal (1 subgoal):
 1. (\<And>y. AE x in M. g x = y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. g x = y

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "AE x in M. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. f x = y
[PROOF STEP]
using g(2) y
[PROOF STATE]
proof (prove)
using this:
AE x in M. f x = g x
AE x in M. g x = y

goal (1 subgoal):
 1. AE x in M. f x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. f x = y

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. f x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. f x = y

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. AE x in M. f x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_conservative) AE_decreasing_func_is_AE_constant:
  fixes f::"_ \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
  assumes "AE x in M. f(T x) \<le> f x"
    and [measurable]: "f \<in> borel_measurable M"
  shows "\<exists>y. AE x in M. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "AE x in M. f(T x) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. f (T x) = f x
[PROOF STEP]
using AE_decreasing_then_invariant[OF assms]
[PROOF STATE]
proof (prove)
using this:
AE x in M. f (T x) = f x

goal (1 subgoal):
 1. AE x in M. f (T x) = f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. f (T x) = f x

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. f (T x) = f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. f (T x) = f x

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
using AE_Invariant_func_is_AE_constant[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
AE x in M. f (T x) = f x
AE x in M. f (T x) = f x \<Longrightarrow> \<exists>y. AE x in M. f x = y

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. AE x in M. f x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_conservative) AE_increasing_func_is_AE_constant:
  fixes f::"_ \<Rightarrow> 'b::{linorder_topology, second_countable_topology}"
  assumes "AE x in M. f(T x) \<ge> f x"
    and [measurable]: "f \<in> borel_measurable M"
  shows "\<exists>y. AE x in M. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
have "AE x in M. f(T x) = f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. f (T x) = f x
[PROOF STEP]
using AE_increasing_then_invariant[OF assms]
[PROOF STATE]
proof (prove)
using this:
AE x in M. f (T x) = f x

goal (1 subgoal):
 1. AE x in M. f (T x) = f x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. f (T x) = f x

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. f (T x) = f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. f (T x) = f x

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
using AE_Invariant_func_is_AE_constant[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
AE x in M. f (T x) = f x
AE x in M. f (T x) = f x \<Longrightarrow> \<exists>y. AE x in M. f x = y

goal (1 subgoal):
 1. \<exists>y. AE x in M. f x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. AE x in M. f x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_fmpt) Invariant_func_integral:
  fixes f::"_ \<Rightarrow> 'b::{banach, second_countable_topology}"
  assumes [measurable]: "f \<in> borel_measurable Invariants"
  shows "integrable M f"
        "AE x in M. f x = (\<integral>x. f x \<partial>M)/\<^sub>R (measure M (space M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M f &&& AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M f
 2. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
have [measurable]: "f \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
using assms Invariants_measurable_func
[PROOF STATE]
proof (prove)
using this:
f \<in> borel_measurable Invariants
?f \<in> Invariants \<rightarrow>\<^sub>M ?N \<Longrightarrow> ?f \<in> M \<rightarrow>\<^sub>M ?N

goal (1 subgoal):
 1. f \<in> borel_measurable M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> borel_measurable M

goal (2 subgoals):
 1. integrable M f
 2. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
obtain y where y: "AE x in M. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. AE x in M. f x = y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Invariant_func_is_AE_constant[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>y. AE x in M. f x = y

goal (1 subgoal):
 1. (\<And>y. AE x in M. f x = y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. f x = y

goal (2 subgoals):
 1. integrable M f
 2. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. f x = y

goal (2 subgoals):
 1. integrable M f
 2. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
have "integrable M (\<lambda>x. y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. y)

goal (2 subgoals):
 1. integrable M f
 2. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. f x = y
integrable M (\<lambda>x. y)
[PROOF STEP]
show "integrable M f"
[PROOF STATE]
proof (prove)
using this:
AE x in M. f x = y
integrable M (\<lambda>x. y)

goal (1 subgoal):
 1. integrable M f
[PROOF STEP]
by (subst integrable_cong_AE[where ?g = "\<lambda>x. y"], auto)
[PROOF STATE]
proof (state)
this:
integrable M f

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
have "(\<integral>x. f x \<partial>M) = (\<integral>x. y \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L M f = LINT x|M. y
[PROOF STEP]
by (subst integral_cong_AE[where ?g = "\<lambda>x. y"], auto simp add: y)
[PROOF STATE]
proof (state)
this:
integral\<^sup>L M f = LINT x|M. y

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral\<^sup>L M f = LINT x|M. y

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
have "... = measure M (space M) *\<^sub>R y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. y = Sigma_Algebra.measure M (space M) *\<^sub>R y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LINT x|M. y = Sigma_Algebra.measure M (space M) *\<^sub>R y

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral\<^sup>L M f = Sigma_Algebra.measure M (space M) *\<^sub>R y
[PROOF STEP]
have *: "(\<integral>x. f x \<partial>M) = measure M (space M) *\<^sub>R y"
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L M f = Sigma_Algebra.measure M (space M) *\<^sub>R y

goal (1 subgoal):
 1. integral\<^sup>L M f = Sigma_Algebra.measure M (space M) *\<^sub>R y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral\<^sup>L M f = Sigma_Algebra.measure M (space M) *\<^sub>R y

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
show "AE x in M. f x = (\<integral>x. f x \<partial>M)/\<^sub>R (measure M (space M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
 2. \<not> ?P \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
assume "emeasure M (space M) = 0"
[PROOF STATE]
proof (state)
this:
emeasure M (space M) = 0

goal (2 subgoals):
 1. ?P \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
 2. \<not> ?P \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure M (space M) = 0
[PROOF STEP]
have "space M \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) = 0

goal (1 subgoal):
 1. space M \<in> null_sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
space M \<in> null_sets M

goal (2 subgoals):
 1. ?P \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
 2. \<not> ?P \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
space M \<in> null_sets M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
space M \<in> null_sets M

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
using AE_I'
[PROOF STATE]
proof (prove)
using this:
space M \<in> null_sets M
\<lbrakk>?N \<in> null_sets ?M; {x \<in> space ?M. \<not> ?P x} \<subseteq> ?N\<rbrakk> \<Longrightarrow> almost_everywhere ?M ?P

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
assume "\<not>(emeasure M (space M) = 0)"
[PROOF STATE]
proof (state)
this:
emeasure M (space M) \<noteq> 0

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
emeasure M (space M) \<noteq> 0
[PROOF STEP]
have "measure M (space M) > 0"
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) \<noteq> 0

goal (1 subgoal):
 1. 0 < Sigma_Algebra.measure M (space M)
[PROOF STEP]
using emeasure_eq_measure measure_le_0_iff
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) \<noteq> 0
emeasure M ?A = ennreal (Sigma_Algebra.measure M ?A)
(Sigma_Algebra.measure ?M ?X \<le> 0) = (Sigma_Algebra.measure ?M ?X = 0)

goal (1 subgoal):
 1. 0 < Sigma_Algebra.measure M (space M)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 < Sigma_Algebra.measure M (space M)

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < Sigma_Algebra.measure M (space M)
[PROOF STEP]
have "y = (\<integral>x. f x \<partial>M)/\<^sub>R (measure M (space M))"
[PROOF STATE]
proof (prove)
using this:
0 < Sigma_Algebra.measure M (space M)

goal (1 subgoal):
 1. y = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
0 < Sigma_Algebra.measure M (space M)
integral\<^sup>L M f = Sigma_Algebra.measure M (space M) *\<^sub>R y

goal (1 subgoal):
 1. y = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)

goal (1 subgoal):
 1. emeasure M (space M) \<noteq> 0 \<Longrightarrow> AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
y = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
AE x in M. f x = y

goal (1 subgoal):
 1. AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
AE x in M. f x = integral\<^sup>L M f /\<^sub>R Sigma_Algebra.measure M (space M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_fmpt) Invariants_cond_exp_is_integral_fmpt:
  fixes f::"_ \<Rightarrow> real"
  assumes "integrable M f"
  shows "AE x in M. real_cond_exp M Invariants f x = (\<integral>x. f x \<partial>M) / measure M (space M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M f / Sigma_Algebra.measure M (space M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M f / Sigma_Algebra.measure M (space M)
[PROOF STEP]
have "AE x in M. real_cond_exp M Invariants f x = (\<integral>x. real_cond_exp M Invariants f x \<partial>M)/\<^sub>R (measure M (space M))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M (real_cond_exp M Invariants f) /\<^sub>R Sigma_Algebra.measure M (space M)
[PROOF STEP]
by (rule Invariant_func_integral(2), simp add: borel_measurable_cond_exp)
[PROOF STATE]
proof (state)
this:
AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M (real_cond_exp M Invariants f) /\<^sub>R Sigma_Algebra.measure M (space M)

goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M f / Sigma_Algebra.measure M (space M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M (real_cond_exp M Invariants f) /\<^sub>R Sigma_Algebra.measure M (space M)

goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M f / Sigma_Algebra.measure M (space M)
[PROOF STEP]
have "(\<integral>x. real_cond_exp M Invariants f x \<partial>M) = (\<integral>x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L M (real_cond_exp M Invariants f) = integral\<^sup>L M f
[PROOF STEP]
by (simp add: assms real_cond_exp_int(2))
[PROOF STATE]
proof (state)
this:
integral\<^sup>L M (real_cond_exp M Invariants f) = integral\<^sup>L M f

goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M f / Sigma_Algebra.measure M (space M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M (real_cond_exp M Invariants f) /\<^sub>R Sigma_Algebra.measure M (space M)
integral\<^sup>L M (real_cond_exp M Invariants f) = integral\<^sup>L M f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M (real_cond_exp M Invariants f) /\<^sub>R Sigma_Algebra.measure M (space M)
integral\<^sup>L M (real_cond_exp M Invariants f) = integral\<^sup>L M f

goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M f / Sigma_Algebra.measure M (space M)
[PROOF STEP]
by (simp add: divide_real_def mult.commute)
[PROOF STATE]
proof (state)
this:
AE x in M. real_cond_exp M Invariants f x = integral\<^sup>L M f / Sigma_Algebra.measure M (space M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_pmpt) Invariants_cond_exp_is_integral:
  fixes f::"_ \<Rightarrow> real"
  assumes "integrable M f"
  shows "AE x in M. real_cond_exp M Invariants f x = (\<integral>x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
by (metis div_by_1 prob_space Invariants_cond_exp_is_integral_fmpt[OF assms])


[STATEMENT]
lemma (in ergodic_conservative_mpt) local_time_unbounded:
  assumes [measurable]: "A \<in> sets M" "B \<in> sets M"
      and "emeasure M A < \<infinity>" "emeasure M B > 0"
  shows "(\<lambda>n. emeasure M {x \<in> (T^^n)--`A. local_time B n x < k}) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. emeasure M {x \<in> (T ^^ n) --` A. local_time B n x < k}) \<longlonglongrightarrow> 0
[PROOF STEP]
proof (rule local_time_unbounded3)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. A \<in> sets M
 2. B \<in> sets M
 3. emeasure M A < \<infinity>
 4. A - (\<Union>i. (T ^^ i) --` B) \<in> null_sets M
[PROOF STEP]
have "A - (\<Union>i. (T ^^ i) --` B) \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - (\<Union>i. (T ^^ i) --` B) \<in> sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A - (\<Union>i. (T ^^ i) --` B) \<in> sets M

goal (4 subgoals):
 1. A \<in> sets M
 2. B \<in> sets M
 3. emeasure M A < \<infinity>
 4. A - (\<Union>i. (T ^^ i) --` B) \<in> null_sets M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A - (\<Union>i. (T ^^ i) --` B) \<in> sets M

goal (4 subgoals):
 1. A \<in> sets M
 2. B \<in> sets M
 3. emeasure M A < \<infinity>
 4. A - (\<Union>i. (T ^^ i) --` B) \<in> null_sets M
[PROOF STEP]
have "A - (\<Union>i. (T ^^ i) --` B) \<subseteq> space M - (\<Union>i. (T ^^ i) --` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - (\<Union>i. (T ^^ i) --` B) \<subseteq> space M - (\<Union>i. (T ^^ i) --` B)
[PROOF STEP]
using sets.sets_into_space[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> space M

goal (1 subgoal):
 1. A - (\<Union>i. (T ^^ i) --` B) \<subseteq> space M - (\<Union>i. (T ^^ i) --` B)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A - (\<Union>i. (T ^^ i) --` B) \<subseteq> space M - (\<Union>i. (T ^^ i) --` B)

goal (4 subgoals):
 1. A \<in> sets M
 2. B \<in> sets M
 3. emeasure M A < \<infinity>
 4. A - (\<Union>i. (T ^^ i) --` B) \<in> null_sets M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A - (\<Union>i. (T ^^ i) --` B) \<in> sets M
A - (\<Union>i. (T ^^ i) --` B) \<subseteq> space M - (\<Union>i. (T ^^ i) --` B)
[PROOF STEP]
show "A - (\<Union>i. (T ^^ i) --` B) \<in> null_sets M"
[PROOF STATE]
proof (prove)
using this:
A - (\<Union>i. (T ^^ i) --` B) \<in> sets M
A - (\<Union>i. (T ^^ i) --` B) \<subseteq> space M - (\<Union>i. (T ^^ i) --` B)

goal (1 subgoal):
 1. A - (\<Union>i. (T ^^ i) --` B) \<in> null_sets M
[PROOF STEP]
by (metis null_sets_subset preimages_conull(1)[OF assms(2) assms(4)])
[PROOF STATE]
proof (state)
this:
A - (\<Union>i. (T ^^ i) --` B) \<in> null_sets M

goal (3 subgoals):
 1. A \<in> sets M
 2. B \<in> sets M
 3. emeasure M A < \<infinity>
[PROOF STEP]
show "emeasure M A < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emeasure M A < \<infinity>
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
emeasure M A < \<infinity>

goal (1 subgoal):
 1. emeasure M A < \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
emeasure M A < \<infinity>

goal (2 subgoals):
 1. A \<in> sets M
 2. B \<in> sets M
[PROOF STEP]
qed (simp_all add: assms)


[STATEMENT]
theorem (in ergodic_conservative_mpt) kac_formula:
  assumes [measurable]: "A \<in> sets M" and "emeasure M A > 0"
  shows "(\<integral>\<^sup>+y. return_time_function A y \<partial>M) = emeasure M (space M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)
[PROOF STEP]
have a [measurable]: "(\<Union>n. (T^^n)--`A) \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>n. (T ^^ n) --` A) \<in> sets M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>n. (T ^^ n) --` A) \<in> sets M

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Union>n. (T ^^ n) --` A) \<in> sets M
[PROOF STEP]
have "space M = (\<Union>n. (T^^n)--`A) \<union> (space M - (\<Union>n. (T^^n)--`A))"
[PROOF STATE]
proof (prove)
using this:
(\<Union>n. (T ^^ n) --` A) \<in> sets M

goal (1 subgoal):
 1. space M = (\<Union>n. (T ^^ n) --` A) \<union> (space M - (\<Union>n. (T ^^ n) --` A))
[PROOF STEP]
using sets.sets_into_space
[PROOF STATE]
proof (prove)
using this:
(\<Union>n. (T ^^ n) --` A) \<in> sets M
?x \<in> sets ?M \<Longrightarrow> ?x \<subseteq> space ?M

goal (1 subgoal):
 1. space M = (\<Union>n. (T ^^ n) --` A) \<union> (space M - (\<Union>n. (T ^^ n) --` A))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
space M = (\<Union>n. (T ^^ n) --` A) \<union> (space M - (\<Union>n. (T ^^ n) --` A))

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
space M = (\<Union>n. (T ^^ n) --` A) \<union> (space M - (\<Union>n. (T ^^ n) --` A))
[PROOF STEP]
have "emeasure M (space M) = emeasure M (\<Union>n. (T^^n)--`A)"
[PROOF STATE]
proof (prove)
using this:
space M = (\<Union>n. (T ^^ n) --` A) \<union> (space M - (\<Union>n. (T ^^ n) --` A))

goal (1 subgoal):
 1. emeasure M (space M) = emeasure M (\<Union>n. (T ^^ n) --` A)
[PROOF STEP]
by (metis a preimages_conull(1)[OF assms] emeasure_Un_null_set)
[PROOF STATE]
proof (state)
this:
emeasure M (space M) = emeasure M (\<Union>n. (T ^^ n) --` A)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
emeasure M (space M) = emeasure M (\<Union>n. (T ^^ n) --` A)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)
[PROOF STEP]
have "(\<integral>\<^sup>+y. return_time_function A y \<partial>M) = emeasure M (\<Union>n. (T^^n)--`A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (\<Union>n. (T ^^ n) --` A)
[PROOF STEP]
using kac_formula_nonergodic[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (\<Union>n. (T ^^ n) --` A)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (\<Union>n. (T ^^ n) --` A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (\<Union>n. (T ^^ n) --` A)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
emeasure M (space M) = emeasure M (\<Union>n. (T ^^ n) --` A)
\<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (\<Union>n. (T ^^ n) --` A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
emeasure M (space M) = emeasure M (\<Union>n. (T ^^ n) --` A)
\<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (\<Union>n. (T ^^ n) --` A)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. of_nat (return_time_function A x) \<partial>M = emeasure M (space M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_conservative_mpt) induced_function_integral:
  fixes f::"'a \<Rightarrow> real"
  assumes [measurable]: "A \<in> sets M" "integrable M f" and "emeasure M A > 0"
  shows "integrable M (induced_function A f)"
        "(\<integral>y. induced_function A f y \<partial>M) = (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (induced_function A f) &&& integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M (induced_function A f)
 2. integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
show "integrable M (induced_function A f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (induced_function A f)
[PROOF STEP]
using induced_function_integral_nonergodic(1)[OF assms(1) assms(2)]
[PROOF STATE]
proof (prove)
using this:
integrable M (induced_function A f)

goal (1 subgoal):
 1. integrable M (induced_function A f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable M (induced_function A f)

goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
have "(\<integral>y. induced_function A f y \<partial>M) = (\<integral> x \<in> (\<Union>n. (T^^n)--`A). f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f
[PROOF STEP]
using induced_function_integral_nonergodic(2)[OF assms(1) assms(2)]
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L M (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f

goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integral\<^sup>L M (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f

goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral\<^sup>L M (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f

goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
have "... = (\<integral> x \<in> space M. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f = set_lebesgue_integral M (space M) f
[PROOF STEP]
using set_integral_null_delta[OF assms(2), where ?A = "space M" and ?B = "(\<Union>n. (T^^n)--`A)"]
    preimages_conull(2)[OF assms(1) assms(3)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>space M \<in> sets M; (\<Union>n. (T ^^ n) --` A) \<in> sets M; space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M\<rbrakk> \<Longrightarrow> set_lebesgue_integral M (space M) f = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f
space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M

goal (1 subgoal):
 1. set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f = set_lebesgue_integral M (space M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f = set_lebesgue_integral M (space M) f

goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f = set_lebesgue_integral M (space M) f

goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
have "... = (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_lebesgue_integral M (space M) f = integral\<^sup>L M f
[PROOF STEP]
using set_integral_space[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
set_lebesgue_integral M (space M) f = integral\<^sup>L M f

goal (1 subgoal):
 1. set_lebesgue_integral M (space M) f = integral\<^sup>L M f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_lebesgue_integral M (space M) f = integral\<^sup>L M f

goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
show "(\<integral>y. induced_function A f y \<partial>M) = (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f

goal (1 subgoal):
 1. integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral\<^sup>L M (induced_function A f) = integral\<^sup>L M f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_conservative_mpt) induced_function_integral_restr:
  fixes f::"'a \<Rightarrow> real"
  assumes [measurable]: "A \<in> sets M" "integrable M f" and "emeasure M A > 0"
  shows "integrable (restrict_space M A) (induced_function A f)"
        "(\<integral>y. induced_function A f y \<partial>(restrict_space M A)) = (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (restrict_space M A) (induced_function A f) &&& integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable (restrict_space M A) (induced_function A f)
 2. integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
show "integrable (restrict_space M A) (induced_function A f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable (restrict_space M A) (induced_function A f)
[PROOF STEP]
using induced_function_integral_restr_nonergodic(1)[OF assms(1) assms(2)]
[PROOF STATE]
proof (prove)
using this:
integrable (restrict_space M A) (induced_function A f)

goal (1 subgoal):
 1. integrable (restrict_space M A) (induced_function A f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integrable (restrict_space M A) (induced_function A f)

goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
have "(\<integral>y. induced_function A f y \<partial>(restrict_space M A)) = (\<integral> x \<in> (\<Union>n. (T^^n)--`A). f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f
[PROOF STEP]
using induced_function_integral_restr_nonergodic(2)[OF assms(1) assms(2)]
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L (restrict_space M A) (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f

goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (restrict_space M A) (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f

goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (restrict_space M A) (induced_function A f) = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f

goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
have "... = (\<integral> x \<in> space M. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f = set_lebesgue_integral M (space M) f
[PROOF STEP]
using set_integral_null_delta[OF assms(2), where ?A = "space M" and ?B = "(\<Union>n. (T^^n)--`A)"]
    preimages_conull(2)[OF assms(1) assms(3)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>space M \<in> sets M; (\<Union>n. (T ^^ n) --` A) \<in> sets M; space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M\<rbrakk> \<Longrightarrow> set_lebesgue_integral M (space M) f = set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f
space M \<Delta> (\<Union>n. (T ^^ n) --` A) \<in> null_sets M

goal (1 subgoal):
 1. set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f = set_lebesgue_integral M (space M) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f = set_lebesgue_integral M (space M) f

goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set_lebesgue_integral M (\<Union>n. (T ^^ n) --` A) f = set_lebesgue_integral M (space M) f

goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
have "... = (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_lebesgue_integral M (space M) f = integral\<^sup>L M f
[PROOF STEP]
using set_integral_space[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
set_lebesgue_integral M (space M) f = integral\<^sup>L M f

goal (1 subgoal):
 1. set_lebesgue_integral M (space M) f = integral\<^sup>L M f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_lebesgue_integral M (space M) f = integral\<^sup>L M f

goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
show "(\<integral>y. induced_function A f y \<partial>(restrict_space M A)) = (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f

goal (1 subgoal):
 1. integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral\<^sup>L (restrict_space M A) (induced_function A f) = integral\<^sup>L M f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in ergodic_pmpt) birkhoff_theorem_AE:
  fixes f::"'a \<Rightarrow> real"
  assumes "integrable M f"
  shows "AE x in M. (\<lambda>n. birkhoff_sum f n x / n) \<longlonglongrightarrow> (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> expectation f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> expectation f
[PROOF STEP]
have "AE x in M. (\<lambda>n. birkhoff_sum f n x / n) \<longlonglongrightarrow> real_cond_exp M Invariants f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> real_cond_exp M Invariants f x
[PROOF STEP]
using birkhoff_theorem_AE_nonergodic[OF assms]
[PROOF STATE]
proof (prove)
using this:
AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> real_cond_exp M Invariants f x

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> real_cond_exp M Invariants f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> real_cond_exp M Invariants f x

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> expectation f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> real_cond_exp M Invariants f x

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> expectation f
[PROOF STEP]
have "AE x in M. real_cond_exp M Invariants f x = (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
using Invariants_cond_exp_is_integral[OF assms]
[PROOF STATE]
proof (prove)
using this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> expectation f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> real_cond_exp M Invariants f x
AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> real_cond_exp M Invariants f x
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> expectation f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. (\<lambda>n. birkhoff_sum f n x / real n) \<longlonglongrightarrow> expectation f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in ergodic_pmpt) birkhoff_theorem_L1:
  fixes f::"'a \<Rightarrow> real"
  assumes [measurable]: "integrable M f"
  shows "(\<lambda>n. \<integral>\<^sup>+x. norm(birkhoff_sum f n x / n - (\<integral> x. f x \<partial>M)) \<partial>M) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
fix n::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
have "AE x in M. real_cond_exp M Invariants f x = (\<integral> x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
using Invariants_cond_exp_is_integral[OF assms]
[PROOF STATE]
proof (prove)
using this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
have *: "AE x in M. norm(birkhoff_sum f n x / n - real_cond_exp M Invariants f x)
                = norm(birkhoff_sum f n x / n - (\<integral> x. f x \<partial>M))"
[PROOF STATE]
proof (prove)
using this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x) = norm (birkhoff_sum f n x / real n - expectation f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x) = norm (birkhoff_sum f n x / real n - expectation f)

goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<integral>\<^sup>+x. norm(birkhoff_sum f n x / n - real_cond_exp M Invariants f x) \<partial>M)
                = (\<integral>\<^sup>+x. norm(birkhoff_sum f n x / n - (\<integral> x. f x \<partial>M)) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M
[PROOF STEP]
apply (rule nn_integral_cong_AE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) = ennreal (norm (birkhoff_sum f n x / real n - expectation f))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
AE x in M. norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x) = norm (birkhoff_sum f n x / real n - expectation f)

goal (1 subgoal):
 1. AE x in M. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) = ennreal (norm (birkhoff_sum f n x / real n - expectation f))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M

goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f ?n14 x / real ?n14 - real_cond_exp M Invariants f x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f ?n14 x / real ?n14 - expectation f)) \<partial>M

goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f ?n14 x / real ?n14 - real_cond_exp M Invariants f x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f ?n14 x / real ?n14 - expectation f)) \<partial>M

goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. \<integral>\<^sup>+x. norm(birkhoff_sum f n x / n - real_cond_exp M Invariants f x) \<partial>M) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
using birkhoff_theorem_L1_nonergodic[OF assms]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) \<partial>M) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) \<partial>M) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f ?n14 x / real ?n14 - real_cond_exp M Invariants f x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f ?n14 x / real ?n14 - expectation f)) \<partial>M
(\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f ?n14 x / real ?n14 - real_cond_exp M Invariants f x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f ?n14 x / real ?n14 - expectation f)) \<partial>M
(\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - real_cond_exp M Invariants f x)) \<partial>M) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<integral>\<^sup>+ x. ennreal (norm (birkhoff_sum f n x / real n - expectation f)) \<partial>M) \<longlonglongrightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in ergodic_pmpt) birkhoff_sum_small_asymp_pos:
  fixes f::"'a \<Rightarrow> real"
  assumes [measurable]: "integrable M f" and "e>0"
  shows "AE x in M. infinite {n. birkhoff_sum f n x \<in> {n * (\<integral>x. f x \<partial>M) .. n * (\<integral>x. f x \<partial>M) + e}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f..real n * expectation f + e}}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f..real n * expectation f + e}}
[PROOF STEP]
have "AE x in M. infinite {n. birkhoff_sum f n x \<in> {n * real_cond_exp M Invariants f x .. n * real_cond_exp M Invariants f x + e}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x..real n * real_cond_exp M Invariants f x + e}}
[PROOF STEP]
using birkhoff_sum_small_asymp_pos_nonergodic[OF assms]
[PROOF STATE]
proof (prove)
using this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x..real n * real_cond_exp M Invariants f x + e}}

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x..real n * real_cond_exp M Invariants f x + e}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x..real n * real_cond_exp M Invariants f x + e}}

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f..real n * expectation f + e}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x..real n * real_cond_exp M Invariants f x + e}}

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f..real n * expectation f + e}}
[PROOF STEP]
have "AE x in M. real_cond_exp M Invariants f x = (\<integral>x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
using Invariants_cond_exp_is_integral[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f..real n * expectation f + e}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x..real n * real_cond_exp M Invariants f x + e}}
AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x..real n * real_cond_exp M Invariants f x + e}}
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f..real n * expectation f + e}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f..real n * expectation f + e}}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in ergodic_pmpt) birkhoff_sum_small_asymp_neg:
  fixes f::"'a \<Rightarrow> real"
  assumes [measurable]: "integrable M f" and "e>0"
  shows "AE x in M. infinite {n. birkhoff_sum f n x \<in> {n * (\<integral>x. f x \<partial>M) - e .. n * (\<integral>x. f x \<partial>M)}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - e..real n * expectation f}}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - e..real n * expectation f}}
[PROOF STEP]
have "AE x in M. infinite {n. birkhoff_sum f n x \<in> {n * real_cond_exp M Invariants f x - e .. n * real_cond_exp M Invariants f x}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x - e..real n * real_cond_exp M Invariants f x}}
[PROOF STEP]
using birkhoff_sum_small_asymp_neg_nonergodic[OF assms]
[PROOF STATE]
proof (prove)
using this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x - e..real n * real_cond_exp M Invariants f x}}

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x - e..real n * real_cond_exp M Invariants f x}}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x - e..real n * real_cond_exp M Invariants f x}}

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - e..real n * expectation f}}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x - e..real n * real_cond_exp M Invariants f x}}

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - e..real n * expectation f}}
[PROOF STEP]
have "AE x in M. real_cond_exp M Invariants f x = (\<integral>x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
using Invariants_cond_exp_is_integral[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - e..real n * expectation f}}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x - e..real n * real_cond_exp M Invariants f x}}
AE x in M. real_cond_exp M Invariants f x = expectation f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * real_cond_exp M Invariants f x - e..real n * real_cond_exp M Invariants f x}}
AE x in M. real_cond_exp M Invariants f x = expectation f

goal (1 subgoal):
 1. AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - e..real n * expectation f}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - e..real n * expectation f}}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ergodic_pmpt) birkhoff_positive_average:
      fixes f::"'a \<Rightarrow> real"
  assumes [measurable]: "integrable M f" and "AE x in M. (\<lambda>n. birkhoff_sum f n x) \<longlonglongrightarrow> \<infinity>"
  shows "(\<integral> x. f x \<partial>M) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < expectation f
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
assume "\<not>((\<integral> x. f x \<partial>M) > 0)"
[PROOF STATE]
proof (state)
this:
\<not> 0 < expectation f

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 0 < expectation f
[PROOF STEP]
have *: "(\<integral> x. f x \<partial>M) \<le> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < expectation f

goal (1 subgoal):
 1. expectation f \<le> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
expectation f \<le> 0

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
have "AE x in M. (\<lambda>n. birkhoff_sum f n x) \<longlonglongrightarrow> \<infinity> \<and> infinite {n. birkhoff_sum f n x \<in> {n * (\<integral>x. f x \<partial>M) - 1 .. n* (\<integral>x. f x \<partial>M)}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. (\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity> \<and> infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}
[PROOF STEP]
using assms(2) birkhoff_sum_small_asymp_neg[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
AE x in M. (\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity>
0 < ?e \<Longrightarrow> AE x in M. infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - ?e..real n * expectation f}}

goal (1 subgoal):
 1. AE x in M. (\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity> \<and> infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. (\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity> \<and> infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. (\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity> \<and> infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}
[PROOF STEP]
obtain x where x: "(\<lambda>n. birkhoff_sum f n x) \<longlonglongrightarrow> \<infinity>" "infinite {n. birkhoff_sum f n x \<in> {n * (\<integral>x. f x \<partial>M) - 1 .. n* (\<integral>x. f x \<partial>M)}}"
[PROOF STATE]
proof (prove)
using this:
AE x in M. (\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity> \<and> infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>(\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity>; infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using AE_False eventually_elim2
[PROOF STATE]
proof (prove)
using this:
AE x in M. (\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity> \<and> infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}
(AE x in M. False) = False
\<lbrakk>eventually ?P ?F; eventually ?Q ?F; \<And>i. \<lbrakk>?P i; ?Q i\<rbrakk> \<Longrightarrow> ?R i\<rbrakk> \<Longrightarrow> eventually ?R ?F

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>(\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity>; infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity>
infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity>
infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
assume "birkhoff_sum f n x \<in> {n * (\<integral>x. f x \<partial>M) - 1 .. n * (\<integral>x. f x \<partial>M)}"
[PROOF STATE]
proof (state)
this:
birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}
[PROOF STEP]
have "birkhoff_sum f n x \<le> n * (\<integral>x. f x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}

goal (1 subgoal):
 1. birkhoff_sum f n x \<le> real n * expectation f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
birkhoff_sum f n x \<le> real n * expectation f

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
birkhoff_sum f n x \<le> real n * expectation f

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
have "... \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n * expectation f \<le> 0
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
expectation f \<le> 0

goal (1 subgoal):
 1. real n * expectation f \<le> 0
[PROOF STEP]
by (simp add: mult_nonneg_nonpos)
[PROOF STATE]
proof (state)
this:
real n * expectation f \<le> 0

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
birkhoff_sum f n x \<le> 0
[PROOF STEP]
have "birkhoff_sum f n x \<le> 0"
[PROOF STATE]
proof (prove)
using this:
birkhoff_sum f n x \<le> 0

goal (1 subgoal):
 1. birkhoff_sum f n x \<le> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
birkhoff_sum f n x \<le> 0

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
birkhoff_sum f ?n14 x \<in> {real ?n14 * expectation f - 1..real ?n14 * expectation f} \<Longrightarrow> birkhoff_sum f ?n14 x \<le> 0

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
birkhoff_sum f ?n14 x \<in> {real ?n14 * expectation f - 1..real ?n14 * expectation f} \<Longrightarrow> birkhoff_sum f ?n14 x \<le> 0
[PROOF STEP]
have "{n. birkhoff_sum f n x \<in> {n * (\<integral>x. f x \<partial>M) - 1 .. n* (\<integral>x. f x \<partial>M)}} \<subseteq> {n. birkhoff_sum f n x \<le> 0}"
[PROOF STATE]
proof (prove)
using this:
birkhoff_sum f ?n14 x \<in> {real ?n14 * expectation f - 1..real ?n14 * expectation f} \<Longrightarrow> birkhoff_sum f ?n14 x \<le> 0

goal (1 subgoal):
 1. {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}} \<subseteq> {n. birkhoff_sum f n x \<le> 0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}} \<subseteq> {n. birkhoff_sum f n x \<le> 0}

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}} \<subseteq> {n. birkhoff_sum f n x \<le> 0}
[PROOF STEP]
have inf: "infinite {n. birkhoff_sum f n x \<le> 0}"
[PROOF STATE]
proof (prove)
using this:
{n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}} \<subseteq> {n. birkhoff_sum f n x \<le> 0}

goal (1 subgoal):
 1. infinite {n. birkhoff_sum f n x \<le> 0}
[PROOF STEP]
using x(2) finite_subset
[PROOF STATE]
proof (prove)
using this:
{n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}} \<subseteq> {n. birkhoff_sum f n x \<le> 0}
infinite {n. birkhoff_sum f n x \<in> {real n * expectation f - 1..real n * expectation f}}
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. infinite {n. birkhoff_sum f n x \<le> 0}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite {n. birkhoff_sum f n x \<le> 0}

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
have "0 < (\<infinity>::ereal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < \<infinity>

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < \<infinity>
[PROOF STEP]
have "eventually (\<lambda>n. birkhoff_sum f n x > (0::ereal)) sequentially"
[PROOF STATE]
proof (prove)
using this:
0 < \<infinity>

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 0 < ereal (birkhoff_sum f n x)
[PROOF STEP]
using x(1) order_tendsto_iff
[PROOF STATE]
proof (prove)
using this:
0 < \<infinity>
(\<lambda>xa. ereal (birkhoff_sum f xa x)) \<longlonglongrightarrow> \<infinity>
(?f \<longlongrightarrow> ?x) ?F = ((\<forall>l<?x. \<forall>\<^sub>F x in ?F. l < ?f x) \<and> (\<forall>u>?x. \<forall>\<^sub>F x in ?F. ?f x < u))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 0 < ereal (birkhoff_sum f n x)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. 0 < ereal (birkhoff_sum f n x)

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. 0 < ereal (birkhoff_sum f n x)
[PROOF STEP]
obtain N where "\<And>n. n \<ge> N \<Longrightarrow> birkhoff_sum f n x > (0::ereal)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. 0 < ereal (birkhoff_sum f n x)

goal (1 subgoal):
 1. (\<And>N. (\<And>n. N \<le> n \<Longrightarrow> 0 < ereal (birkhoff_sum f n x)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson eventually_at_top_linorder)
[PROOF STATE]
proof (state)
this:
N \<le> ?n12 \<Longrightarrow> 0 < ereal (birkhoff_sum f ?n12 x)

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?n12 \<Longrightarrow> 0 < ereal (birkhoff_sum f ?n12 x)
[PROOF STEP]
have "\<And>n. n \<ge> N \<Longrightarrow> birkhoff_sum f n x > 0"
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n12 \<Longrightarrow> 0 < ereal (birkhoff_sum f ?n12 x)

goal (1 subgoal):
 1. \<And>n. N \<le> n \<Longrightarrow> 0 < birkhoff_sum f n x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
N \<le> ?n12 \<Longrightarrow> 0 < birkhoff_sum f ?n12 x

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?n12 \<Longrightarrow> 0 < birkhoff_sum f ?n12 x
[PROOF STEP]
have "{n. birkhoff_sum f n x \<le> 0} \<subseteq> {..<N}"
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n12 \<Longrightarrow> 0 < birkhoff_sum f ?n12 x

goal (1 subgoal):
 1. {n. birkhoff_sum f n x \<le> 0} \<subseteq> {..<N}
[PROOF STEP]
by (metis (mono_tags, lifting) lessThan_iff linorder_not_less mem_Collect_eq subsetI)
[PROOF STATE]
proof (state)
this:
{n. birkhoff_sum f n x \<le> 0} \<subseteq> {..<N}

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{n. birkhoff_sum f n x \<le> 0} \<subseteq> {..<N}
[PROOF STEP]
have "finite {n. birkhoff_sum f n x \<le> 0}"
[PROOF STATE]
proof (prove)
using this:
{n. birkhoff_sum f n x \<le> 0} \<subseteq> {..<N}

goal (1 subgoal):
 1. finite {n. birkhoff_sum f n x \<le> 0}
[PROOF STEP]
using finite_nat_iff_bounded
[PROOF STATE]
proof (prove)
using this:
{n. birkhoff_sum f n x \<le> 0} \<subseteq> {..<N}
finite ?S = (\<exists>k. ?S \<subseteq> {..<k})

goal (1 subgoal):
 1. finite {n. birkhoff_sum f n x \<le> 0}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
finite {n. birkhoff_sum f n x \<le> 0}

goal (1 subgoal):
 1. \<not> 0 < expectation f \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {n. birkhoff_sum f n x \<le> 0}
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
finite {n. birkhoff_sum f n x \<le> 0}

goal (1 subgoal):
 1. False
[PROOF STEP]
using inf
[PROOF STATE]
proof (prove)
using this:
finite {n. birkhoff_sum f n x \<le> 0}
infinite {n. birkhoff_sum f n x \<le> 0}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed