[STATEMENT]
lemma (in ergodic_pmpt) birkhoff_negative_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. expectation f < 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> expectation f < 0 \<Longrightarrow> False
[PROOF STEP]
assume "\<not>((\<integral> x. f x \<partial>M) < 0)"
[PROOF STATE]
proof (state)
this:
\<not> expectation f < 0

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

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

goal (1 subgoal):
 1. \<not> expectation f < 0 \<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) .. n* (\<integral>x. f x \<partial>M) + 1}}"
[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..real n * expectation f + 1}}
[PROOF STEP]
using assms(2) birkhoff_sum_small_asymp_pos[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..real n * expectation f + ?e}}

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..real n * expectation f + 1}}
[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..real n * expectation f + 1}}

goal (1 subgoal):
 1. \<not> expectation f < 0 \<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..real n * expectation f + 1}}
[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) .. n* (\<integral>x. f x \<partial>M) + 1}}"
[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..real n * expectation f + 1}}

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..real n * expectation f + 1}}\<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..real n * expectation f + 1}}
(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..real n * expectation f + 1}}\<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..real n * expectation f + 1}}

goal (1 subgoal):
 1. \<not> expectation f < 0 \<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..real n * expectation f + 1}}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. ereal (birkhoff_sum f n x) < 0
[PROOF STEP]
using x(1) order_tendsto_iff
[PROOF STATE]
proof (prove)
using this:
- \<infinity> < 0
(\<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. ereal (birkhoff_sum f n x) < 0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. ereal (birkhoff_sum f n x) < 0

goal (1 subgoal):
 1. \<not> expectation f < 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. ereal (birkhoff_sum f n x) < 0
[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. ereal (birkhoff_sum f n x) < 0

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

goal (1 subgoal):
 1. \<not> expectation f < 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?n12 \<Longrightarrow> ereal (birkhoff_sum f ?n12 x) < 0
[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> ereal (birkhoff_sum f ?n12 x) < 0

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

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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>(\<lambda>xa. ereal \<bar>birkhoff_sum f xa x\<bar>) \<longlonglongrightarrow> \<infinity>; infinite {n. birkhoff_sum f n x \<in> {0..1}}\<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 \<bar>birkhoff_sum f xa x\<bar>) \<longlonglongrightarrow> \<infinity> \<and> infinite {n. birkhoff_sum f n x \<in> {0..1}}
(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 \<bar>birkhoff_sum f xa x\<bar>) \<longlonglongrightarrow> \<infinity>; infinite {n. birkhoff_sum f n x \<in> {0..1}}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>xa. ereal \<bar>birkhoff_sum f xa x\<bar>) \<longlonglongrightarrow> \<infinity>
infinite {n. birkhoff_sum f n x \<in> {0..1}}

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

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

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 1 < ereal \<bar>birkhoff_sum f n x\<bar>
[PROOF STEP]
using x(1) order_tendsto_iff
[PROOF STATE]
proof (prove)
using this:
1 < \<infinity>
(\<lambda>xa. ereal \<bar>birkhoff_sum f xa x\<bar>) \<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. 1 < ereal \<bar>birkhoff_sum f n x\<bar>
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. 1 < ereal \<bar>birkhoff_sum f n x\<bar>

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

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

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

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

goal (1 subgoal):
 1. \<not> expectation f \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "{n. birkhoff_sum f n x \<in> {0..1}} \<subseteq> {..<N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {n. birkhoff_sum f n x \<in> {0..1}} \<subseteq> {..<N}
[PROOF STEP]
by (auto, metis (full_types) * abs_of_nonneg not_less)
[PROOF STATE]
proof (state)
this:
{n. birkhoff_sum f n x \<in> {0..1}} \<subseteq> {..<N}

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma even_and_odd_parts:
  fixes n::nat
  assumes \<open>n \<noteq> 0\<close>
  shows \<open>\<exists> k q::nat. n = (2::nat)^k*q \<and> odd q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k q. n = 2 ^ k * q \<and> odd q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k q. n = 2 ^ k * q \<and> odd q
[PROOF STEP]
have \<open>prime (2::nat)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 2

goal (1 subgoal):
 1. \<exists>k q. n = 2 ^ k * q \<and> odd q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prime 2

goal (1 subgoal):
 1. \<exists>k q. n = 2 ^ k * q \<and> odd q
[PROOF STEP]
using prime_power_canonical[where p = "2" and m = "n"]
      assms semiring_normalization_rules(7)
[PROOF STATE]
proof (prove)
using this:
prime 2
\<lbrakk>prime 2; 0 < n\<rbrakk> \<Longrightarrow> \<exists>k na. odd na \<and> n = na * 2 ^ k
n \<noteq> 0
?a * ?b = ?b * ?a

goal (1 subgoal):
 1. \<exists>k q. n = 2 ^ k * q \<and> odd q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k q. n = 2 ^ k * q \<and> odd q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma only_one_odd_div_power2:
  fixes n::nat
  assumes \<open>n \<noteq> 0\<close> and  \<open>\<And> x. x dvd n \<Longrightarrow> odd x \<Longrightarrow> x = 1\<close>
  shows \<open>\<exists> k. n = (2::nat)^k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. n = 2 ^ k
[PROOF STEP]
by (metis even_and_odd_parts assms(1) assms(2) dvd_triv_left semiring_normalization_rules(11)
      semiring_normalization_rules(7))


[STATEMENT]
lemma coprime_power2:
  fixes n::nat
  assumes \<open>n \<noteq> 0\<close> and \<open>\<And> x. x < n \<Longrightarrow> (coprime x n \<longleftrightarrow> odd x)\<close>
  shows \<open>\<exists> k. n = (2::nat)^k\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. n = 2 ^ k
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>k. n = 2 ^ k
[PROOF STEP]
have \<open>x dvd n \<Longrightarrow> odd x \<Longrightarrow> x = 1\<close>
    for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x dvd n; odd x\<rbrakk> \<Longrightarrow> x = 1
[PROOF STEP]
by (metis neq0_conv One_nat_def Suc_1 Suc_lessI assms(1) assms(2) coprime_left_2_iff_odd
        dvd_refl linorder_neqE_nat nat_dvd_1_iff_1 nat_dvd_not_less not_coprimeI)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x dvd n; odd ?x\<rbrakk> \<Longrightarrow> ?x = 1

goal (1 subgoal):
 1. \<exists>k. n = 2 ^ k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x dvd n; odd ?x\<rbrakk> \<Longrightarrow> ?x = 1

goal (1 subgoal):
 1. \<exists>k. n = 2 ^ k
[PROOF STEP]
using assms(1) only_one_odd_div_power2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x dvd n; odd ?x\<rbrakk> \<Longrightarrow> ?x = 1
n \<noteq> 0
\<lbrakk>?n \<noteq> 0; \<And>x. \<lbrakk>x dvd ?n; odd x\<rbrakk> \<Longrightarrow> x = 1\<rbrakk> \<Longrightarrow> \<exists>k. ?n = 2 ^ k

goal (1 subgoal):
 1. \<exists>k. n = 2 ^ k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. n = 2 ^ k

goal:
No subgoals!
[PROOF STEP]
qed