Theory Gouezel_Karlsson
section ‹Gouezel-Karlsson›
theory Gouezel_Karlsson
imports Asymptotic_Density Kingman
begin
text ‹This section is devoted to the proof of the main ergodic result of
the article "Subadditive and multiplicative ergodic theorems" by Gouezel and
Karlsson~\<^cite>‹"gouezel_karlsson"›. It is a version of Kingman
theorem ensuring that, for subadditive cocycles, there are almost surely
many times $n$ where the cocycle is nearly additive at \emph{all} times
between $0$ and $n$.
This theorem is then used in this article to construct horofunctions
characterizing the behavior at infinity of compositions
of semi-contractions. This requires too many further notions to be implemented
in current Isabelle/HOL, but the main ergodic result is completely
proved below, in Theorem~\verb+Gouezel_Karlsson+, following the arguments in the paper (but in a
slightly more general setting here as we are not making any ergodicity assumption).
To simplify the exposition, the theorem is proved assuming that the limit of the subcocycle
vanishes almost everywhere, in the locale \verb+Gouezel_Karlsson_Kingman+.
The final result is proved by an easy reduction to this case.
The main steps of the proof are as follows:
\begin{itemize}
\item assume first that the map is invertible, and consider the inverse map and the corresponding
inverse subcocycle. With combinatorial arguments that only work for this inverse subcocycle, we
control the density of bad times given some allowed error $d>0$, in a precise quantitative way, in
Lemmas~\verb+upper_density_all_times+ and~\verb+upper_density_large_k+. We put these estimates
together in Lemma~\verb+upper_density_delta+.
\item These estimates are then transfered to the original time direction and the original subcocycle in
Lemma~\verb+upper_density_good_direction_invertible+. The fact that we have quantitative estimates
in terms of asymptotic densities is central here, just having some infiniteness statement would not be
enough.
\item The invertibility assumption is removed in Lemma~\verb+upper_density_good_direction+ by
using the result in the natural extension.
\item Finally, the main result is deduced in Lemma~\verb+infinite_AE+ (still assuming that the
asymptotic limit vanishes almost everywhere), and in full generality in
Theorem~\verb+Gouezel_Karlsson_Kingman+.
\end{itemize}
›
lemma upper_density_eventually_measure:
fixes a::real
assumes [measurable]: "⋀n. {x ∈ space M. P x n} ∈ sets M"
and "emeasure M {x ∈ space M. upper_asymptotic_density {n. P x n} < a} > b"
shows "∃N. emeasure M {x ∈ space M. ∀n ≥ N. card ({n. P x n} ∩ {..<n}) < a * n} > b"
proof -
define G where "G = {x ∈ space M. upper_asymptotic_density {n. P x n} < a}"
define H where "H = (λN. {x ∈ space M. ∀n ≥ N. card ({n. P x n} ∩ {..<n}) < a * n})"
have [measurable]: "G ∈ sets M" "⋀N. H N ∈ sets M" unfolding G_def H_def by auto
have "G ⊆ (⋃N. H N)"
proof
fix x assume "x ∈ G"
then have "x ∈ space M" unfolding G_def by simp
have "eventually (λn. card({n. P x n} ∩ {..<n}) < a * n) sequentially"
using ‹x ∈ G› unfolding G_def using upper_asymptotic_densityD by auto
then obtain N where "⋀n. n ≥ N ⟹ card({n. P x n} ∩ {..<n}) < a * n"
using eventually_sequentially by auto
then have "x ∈ H N" unfolding H_def using ‹x ∈ space M› by auto
then show "x ∈ (⋃N. H N)" by blast
qed
have "b < emeasure M G" using assms(2) unfolding G_def by simp
also have "... ≤ emeasure M (⋃N. H N)"
apply (rule emeasure_mono) using ‹G ⊆ (⋃N. H N)› by auto
finally have "emeasure M (⋃N. H N) > b" by simp
moreover have "(λN. emeasure M (H N)) ⇢ emeasure M (⋃N. H N)"
apply (rule Lim_emeasure_incseq) unfolding H_def incseq_def by auto
ultimately have "eventually (λN. emeasure M (H N) > b) sequentially"
by (simp add: order_tendsto_iff)
then obtain N where "emeasure M (H N) > b"
using eventually_False_sequentially eventually_mono by blast
then show ?thesis unfolding H_def by blast
qed
locale Gouezel_Karlsson_Kingman = pmpt +
fixes u::"nat ⇒ 'a ⇒ real"
assumes subu: "subcocycle u"
and subu_fin: "subcocycle_avg_ereal u > -∞"
and subu_0: "AE x in M. subcocycle_lim u x = 0"
begin
lemma int_u [measurable]:
"integrable M (u n)"
using subu unfolding subcocycle_def by auto
text ‹Next lemma is Lemma 2.1 in~\<^cite>‹"gouezel_karlsson"›.›
lemma upper_density_all_times:
assumes "d > (0::real)"
shows "∃c> (0::real).
emeasure M {x ∈ space M. upper_asymptotic_density {n. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - c * l} < d} > 1 - d"
proof -
define f where "f = (λx. abs (u 1 x))"
have [measurable]: "f ∈ borel_measurable M" unfolding f_def by auto
define G where "G = {x ∈ space M. (λn. birkhoff_sum f n x / n) ⇢ real_cond_exp M Invariants f x
∧ (λn. u n x / n) ⇢ 0}"
have [measurable]: "G ∈ sets M" unfolding G_def by auto
have "AE x in M. (λn. birkhoff_sum f n x / n) ⇢ real_cond_exp M Invariants f x"
apply (rule birkhoff_theorem_AE_nonergodic) using subu unfolding f_def subcocycle_def by auto
moreover have "AE x in M. (λn. u n x / n) ⇢ 0"
using subu_0 kingman_theorem_nonergodic(1)[OF subu subu_fin] by auto
ultimately have "AE x in M. x ∈ G" unfolding G_def by auto
then have "emeasure M G = 1" by (simp add: emeasure_eq_1_AE)
define V where "V = (λc x. {n. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - c * l})"
define Good where "Good = (λc. {x ∈ G. upper_asymptotic_density (V c x) < d})"
have [measurable]: "Good c ∈ sets M" for c unfolding Good_def V_def by auto
have I: "upper_asymptotic_density (V c x) ≤ real_cond_exp M Invariants f x / c" if "c>0" "x ∈ G" for c x
proof -
have [simp]: "c>0" "c ≠ 0" "c ≥ 0" using ‹c>0› by auto
define U where "U = (λn. abs(u 0 x) + birkhoff_sum f n x - c * card (V c x ∩ {1..n}))"
have main: "u n x ≤ U n" for n
proof (rule nat_less_induct)
fix n assume H: "∀m<n. u m x ≤ U m"
consider "n = 0" | "n≥1 ∧ n ∉ V c x" | "n≥1 ∧ n ∈ V c x" by linarith
then show "u n x ≤ U n"
proof (cases)
assume "n = 0"
then show ?thesis unfolding U_def by auto
next
assume A: "n≥1 ∧ n ∉ V c x"
then have "n ≥ 1" by simp
then have "n-1<n" by simp
have "{1..n} = {1..n-1} ∪ {n}" using ‹1 ≤ n› atLeastLessThanSuc by auto
then have *: "card (V c x ∩ {1..n}) = card (V c x ∩ {1..n-1})" using A by auto
have "u n x ≤ u (n-1) x + u 1 ((T^^(n-1)) x)"
using ‹n≥1› subu unfolding subcocycle_def by (metis le_add_diff_inverse2)
also have "... ≤ U (n-1) + f ((T^^(n-1)) x)" unfolding f_def using H ‹n-1<n› by auto
also have "... = abs(u 0 x) + birkhoff_sum f (n-1) x + f ((T^^(n-1)) x) - c * card (V c x ∩ {1..n-1})"
unfolding U_def by auto
also have "... = abs(u 0 x) + birkhoff_sum f n x - c * card (V c x ∩ {1..n})"
using * birkhoff_sum_cocycle[of f "n-1" 1 x] ‹1 ≤ n› by auto
also have "... = U n" unfolding U_def by simp
finally show ?thesis by auto
next
assume B: "n≥1 ∧ n ∈ V c x"
then obtain l where l: "l∈{1..n}" "u n x - u (n-l) x ≤ - c * l" unfolding V_def by blast
then have "n-l < n" by simp
have m: "- (r * ra) - r * rb = - (r * (rb + ra))" for r ra rb::real
by (simp add: algebra_simps)
have "card(V c x ∩ {1..n}) ≤ card ((V c x ∩ {1..n-l}) ∪ {n-l+1..n})"
by (rule card_mono, auto)
also have "... ≤ card (V c x ∩ {1..n-l}) + card {n-l+1..n}"
by (rule card_Un_le)
also have "... ≤ card (V c x ∩ {1..n-l}) + l" by auto
finally have "card(V c x ∩ {1..n}) ≤ card (V c x ∩ {1..n-l}) + real l" by auto
then have *: "-c * card (V c x ∩ {1..n-l}) - c * l ≤ -c * card(V c x ∩ {1..n})"
using m by auto
have "birkhoff_sum f ((n-l) + l) x = birkhoff_sum f (n-l) x + birkhoff_sum f l ((T^^(n-l))x)"
by (rule birkhoff_sum_cocycle)
moreover have "birkhoff_sum f l ((T^^(n-l))x) ≥ 0"
unfolding f_def birkhoff_sum_def using sum_nonneg by auto
ultimately have **: "birkhoff_sum f (n-l) x ≤ birkhoff_sum f n x" using l(1) by auto
have "u n x ≤ u (n-l) x - c * l" using l by simp
also have "... ≤ U (n-l) - c* l" using H ‹n-l < n› by auto
also have "... = abs(u 0 x) + birkhoff_sum f (n-l) x - c * card (V c x ∩ {1..n-l}) - c*l"
unfolding U_def by auto
also have "... ≤ abs(u 0 x) + birkhoff_sum f n x - c * card (V c x ∩ {1..n})"
using * ** by simp
finally show ?thesis unfolding U_def by auto
qed
qed
have "(λn. abs(u 0 x) * (1/n) + birkhoff_sum f n x / n - u n x / n) ⇢ abs(u 0 x) * 0 + real_cond_exp M Invariants f x - 0"
apply (intro tendsto_intros) using ‹x ∈ G› unfolding G_def by auto
moreover have "(abs(u 0 x) + birkhoff_sum f n x - u n x)/n = abs(u 0 x) * (1/n) + birkhoff_sum f n x / n - u n x / n" for n
by (auto simp add: add_divide_distrib diff_divide_distrib)
ultimately have "(λn. (abs(u 0 x) + birkhoff_sum f n x - u n x)/n) ⇢ real_cond_exp M Invariants f x"
by auto
then have a: "limsup (λn. (abs(u 0 x) + birkhoff_sum f n x - u n x)/n) = real_cond_exp M Invariants f x"
by (simp add: assms lim_imp_Limsup)
have "c * card (V c x ∩ {1..n})/n ≤ (abs(u 0 x) + birkhoff_sum f n x - u n x)/n" for n
using main[of n] unfolding U_def by (simp add: divide_right_mono)
then have "limsup (λn. c * card (V c x ∩ {1..n})/n) ≤ limsup (λn. (abs(u 0 x) + birkhoff_sum f n x - u n x)/n)"
by (simp add: Limsup_mono)
then have b: "limsup (λn. c * card (V c x ∩ {1..n})/n) ≤ real_cond_exp M Invariants f x"
using a by simp
have "ereal(upper_asymptotic_density (V c x)) = limsup (λn. card (V c x ∩ {1..n})/n)"
using upper_asymptotic_density_shift[of "V c x" 1 0] by auto
also have "... = limsup (λn. ereal(1/c) * ereal(c * card (V c x ∩ {1..n})/n))"
by auto
also have "... = (1/c) * limsup (λn. c * card (V c x ∩ {1..n})/n)"
by (rule limsup_ereal_mult_left, auto)
also have "... ≤ ereal (1/c) * real_cond_exp M Invariants f x"
by (rule ereal_mult_left_mono[OF b], auto)
finally show "upper_asymptotic_density (V c x) ≤ real_cond_exp M Invariants f x / c"
by auto
qed
{
fix r::real
obtain c::nat where "r / d < c" using reals_Archimedean2 by auto
then have "r/d < real c+1" by auto
then have "r / (real c+1) < d" using ‹d>0› by (simp add: divide_less_eq mult.commute)
then have "∃c::nat. r / (real c+1) < d" by auto
}
then have unG: "(⋃c::nat. {x ∈ G. real_cond_exp M Invariants f x / (c+1) < d}) = G"
by auto
have *: "r < d * (real n + 1)" if "m ≤ n" "r < d * (real m + 1)" for m n r
proof -
have "d * (real m + 1) ≤ d * (real n + 1)" using ‹d>0› ‹m ≤ n› by auto
then show ?thesis using ‹r < d * (real m + 1)› by auto
qed
have "(λc. emeasure M {x ∈ G. real_cond_exp M Invariants f x / (real c+1) < d})
⇢ emeasure M (⋃c::nat. {x ∈ G. real_cond_exp M Invariants f x / (c+1) < d})"
apply (rule Lim_emeasure_incseq) unfolding incseq_def by (auto simp add: divide_simps *)
then have "(λc. emeasure M {x ∈ G. real_cond_exp M Invariants f x / (real c+1) < d}) ⇢ emeasure M G"
using unG by auto
then have "(λc. emeasure M {x ∈ G. real_cond_exp M Invariants f x / (real c+1) < d}) ⇢ 1"
using ‹emeasure M G = 1› by simp
then have "eventually (λc. emeasure M {x ∈ G. real_cond_exp M Invariants f x / (real c+1) < d} > 1 - d) sequentially"
apply (rule order_tendstoD)
apply (insert ‹0<d›, auto simp add: ennreal_1[symmetric] ennreal_lessI simp del: ennreal_1)
done
then obtain c0 where c0: "emeasure M {x ∈ G. real_cond_exp M Invariants f x / (real c0+1) < d} > 1 - d"
using eventually_sequentially by auto
define c where "c = real c0 + 1"
then have "c > 0" by auto
have *: "emeasure M {x ∈ G. real_cond_exp M Invariants f x / c < d} > 1 - d"
unfolding c_def using c0 by auto
have "{x ∈ G. real_cond_exp M Invariants f x / c < d} ⊆ {x ∈ space M. upper_asymptotic_density (V c x) < d}"
apply auto
using G_def apply blast
using I[OF ‹c>0›] by fastforce
then have "emeasure M {x ∈ G. real_cond_exp M Invariants f x / c < d} ≤ emeasure M {x ∈ space M. upper_asymptotic_density (V c x) < d}"
apply (rule emeasure_mono) unfolding V_def by auto
then have "emeasure M {x ∈ space M. upper_asymptotic_density (V c x) < d} > 1 - d" using * by auto
then show ?thesis unfolding V_def using ‹c>0› by auto
qed
text ‹Next lemma is Lemma 2.2 in~\<^cite>‹"gouezel_karlsson"›.›
lemma upper_density_large_k:
assumes "d > (0::real)" "d ≤ 1"
shows "∃k::nat.
emeasure M {x ∈ space M. upper_asymptotic_density {n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - d * l} < d} > 1 - d"
proof -
have [simp]: "d>0" "d ≠ 0" "d ≥ 0" using ‹d>0› by auto
define rho where "rho = d * d * d / 4"
have [simp]: "rho > 0" "rho ≠ 0" "rho ≥ 0" unfolding rho_def using assms by auto
text ‹First step: choose a time scale $s$ at which all the computations will be done. the
integral of $u_s$ should be suitably small -- how small precisely is given by $\rho$.›
have "ennreal(∫x. abs(u n x / n) ∂M) = (∫⇧+x. abs(u n x /n - subcocycle_lim u x) ∂M)" for n
proof -
have "ennreal(∫x. abs(u n x / n) ∂M) = (∫⇧+x. abs(u n x /n) ∂M)"
apply (rule nn_integral_eq_integral[symmetric]) using int_u by auto
also have "... = (∫⇧+x. abs(u n x /n - subcocycle_lim u x) ∂M)"
apply (rule nn_integral_cong_AE) using subu_0 by auto
finally show ?thesis by simp
qed
moreover have "(λn. ∫⇧+x. abs(u n x /n - subcocycle_lim u x) ∂M) ⇢ 0"
by (rule kingman_theorem_nonergodic(3)[OF subu subu_fin])
ultimately have "(λn. ennreal(∫x. abs(u n x / n) ∂M)) ⇢ 0"
by auto
then have "(λn. (∫x. abs(u n x / n) ∂M)) ⇢ 0"
by (simp add: ennreal_0[symmetric] del: ennreal_0)
then have "eventually (λn. (∫x. abs(u n x / n) ∂M) < rho) sequentially"
by (rule order_tendstoD(2), auto)
then obtain s::nat where [simp]: "s>0" and s_int: "(∫x. abs(u s x / s) ∂M) < rho"
by (metis (mono_tags, lifting) neq0_conv eventually_sequentially gr_implies_not0
linorder_not_le of_nat_0_eq_iff order_refl zero_neq_one)
text ‹Second step: a truncation argument, to decompose $|u_1|$ as a sum of a constant (its
contribution will be small if $k$ is large at the end of the argument) and of a function with
small integral).›
have "(λn. (∫x. abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ n} x ∂M)) ⇢ (∫x. 0 ∂M)"
proof (rule integral_dominated_convergence[where ?w = "λx. abs(u 1 x)"])
show "AE x in M. norm (abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ n} x) ≤ abs(u 1 x)" for n
unfolding indicator_def by auto
{
fix x
have "abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ n} x = (0::real)" if "n > abs(u 1 x)" for n::nat
unfolding indicator_def using that by auto
then have "eventually (λn. abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ n} x = 0) sequentially"
by (metis (mono_tags, lifting) eventually_at_top_linorder reals_Archimedean2 less_le_trans of_nat_le_iff)
then have "(λn. abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ n} x) ⇢ 0"
by (rule tendsto_eventually)
}
then show "AE x in M. (λn. abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ n} x) ⇢ 0"
by simp
qed (auto simp add: int_u)
then have "eventually (λn. (∫x. abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ n} x ∂M) < rho) sequentially"
by (rule order_tendstoD(2), auto)
then obtain Knat::nat where Knat: "Knat > 0" "(∫x. abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ Knat} x ∂M) < rho"
by (metis (mono_tags, lifting) eventually_sequentially gr_implies_not0 neq0_conv
linorder_not_le of_nat_0_eq_iff order_refl zero_neq_one)
define K where "K = real Knat"
then have [simp]: "K ≥ 0" "K>0" and K: "(∫x. abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ K} x ∂M) < rho"
using Knat by auto
define F where "F = (λx. abs(u 1 x) * indicator {x. abs(u 1 x) ≥ K} x)"
have int_F [measurable]: "integrable M F"
unfolding F_def apply (rule Bochner_Integration.integrable_bound[where ?f = "λx. abs(u 1 x)"])
unfolding indicator_def by (auto simp add: int_u)
have "(∫x. F x ∂M) = (∫x. abs(u 1 x) * indicator {x ∈ space M. abs(u 1 x) ≥ K} x ∂M)"
apply (rule integral_cong_AE) unfolding F_def by (auto simp add: indicator_def)
then have F_int: "(∫x. F x ∂M) < rho" using K by auto
have F_pos: "F x ≥ 0" for x unfolding F_def by auto
have u1_bound: "abs(u 1 x) ≤ K + F x" for x
unfolding F_def indicator_def apply (cases "x ∈ {x ∈ space M. K ≤ ¦u 1 x¦}") by auto
define F2 where "F2 = (λx. F x + abs(u s x/s))"
have int_F2 [measurable]: "integrable M F2"
unfolding F2_def using int_F int_u[of s] by auto
have F2_pos: "F2 x ≥ 0" for x unfolding F2_def using F_pos by auto
have "(∫x. F2 x ∂M) = (∫x. F x ∂M) + (∫x. abs(u s x/s) ∂M)"
unfolding F2_def apply (rule Bochner_Integration.integral_add) using int_F int_u by auto
then have F2_int: "(∫x. F2 x ∂M) < 2 * rho"
using F_int s_int by auto
text ‹We can now choose $k$, large enough. The reason for our choice will only appear
at the end of the proof.›
define k where "k = max (2 * s + 1) (nat(ceiling((2 * d * s + 2 * K * s)/(d/2))))"
have "k > 2 * s" unfolding k_def by auto
have "k ≥ (2 * d * s + 2 * K * s)/(d/2)"
unfolding k_def by linarith
then have "(2 * d * s + 2 * K * s)/k ≤ d/2"
using ‹k > 2 * s› by (simp add: divide_simps mult.commute)
text ‹Third step: definition of a good set $G$ where everything goes well.›
define G where "G = {x ∈ space M. (λn. u n x / n) ⇢ 0
∧ (λn. birkhoff_sum (λx. abs(u s x / s)) n x / n) ⇢ real_cond_exp M Invariants (λx. abs(u s x / s)) x
∧ (λn. birkhoff_sum F n x / n) ⇢ real_cond_exp M Invariants F x
∧ real_cond_exp M Invariants F x + real_cond_exp M Invariants (λx. abs(u s x / s)) x = real_cond_exp M Invariants F2 x}"
have [measurable]: "G ∈ sets M" unfolding G_def by auto
have "AE x in M. (λn. u n x / n) ⇢ 0"
using kingman_theorem_nonergodic(1)[OF subu subu_fin] subu_0 by auto
moreover have "AE x in M.(λn. birkhoff_sum (λx. abs(u s x / s)) n x / n) ⇢ real_cond_exp M Invariants (λx. abs(u s x / s)) x"
apply (rule birkhoff_theorem_AE_nonergodic) using int_u[of s] by auto
moreover have "AE x in M. (λn. birkhoff_sum F n x / n) ⇢ real_cond_exp M Invariants F x"
by (rule birkhoff_theorem_AE_nonergodic[OF int_F])
moreover have "AE x in M. real_cond_exp M Invariants F x + real_cond_exp M Invariants (λx. abs(u s x / s)) x = real_cond_exp M Invariants F2 x"
unfolding F2_def apply (rule AE_symmetric[OF real_cond_exp_add]) using int_u[of s] int_F int_u[of s] by auto
ultimately have "AE x in M. x ∈ G" unfolding G_def by auto
then have "emeasure M G = 1" by (simp add: emeasure_eq_1_AE)
text ‹Estimation of asymptotic densities of bad times, for points in $G$.
There is a trivial part, named $U$ below, that has to be treated separately because it creates
problematic boundary effects.›
define U where "U = (λx. {n. ∃l ∈ {n-s<..n}. u n x - u (n-l) x ≤ - d * l})"
define V where "V = (λx. {n. ∃l ∈ {k..n-s}. u n x - u (n-l) x ≤ - d * l})"
text ‹Trivial estimate for $U(x)$: this set is finite for $x\in G$.›
have densU: "upper_asymptotic_density (U x) = 0" if "x ∈ G" for x
proof -
define C where "C = Max {abs(u m x) |m. m<s} + d * s"
have *: "U x ⊆ {n. u n x ≤ C - d * n}"
proof (auto)
fix n assume "n ∈ U x"
then obtain l where l: "l∈ {n-s <..n}" "u n x - u (n-l) x ≤ - d * l" unfolding U_def by auto
define m where "m = n-l"
have "m < s" unfolding m_def using l by auto
have "u n x ≤ u m x - d * l" using l m_def by auto
also have "... ≤ abs(u m x) - d * n + d * m" unfolding m_def using l
by (simp add: algebra_simps of_nat_diff)
also have "... ≤ Max {abs(u m x) |m. m<s} - d * n + d * m"
using ‹m < s› apply (auto) by (rule Max_ge, auto)
also have "... ≤ Max {abs(u m x) |m. m<s} + d * s - d * n"
using ‹m < s› ‹d>0› by auto
finally show "u n x ≤ C - d * n"
unfolding C_def by auto
qed
have "eventually (λn. u n x / n > -d/2) sequentially"
apply (rule order_tendstoD(1)) using ‹x ∈ G› ‹d>0› unfolding G_def by auto
then obtain N where N: "⋀n. n ≥ N ⟹ u n x / n > - d/2"
using eventually_sequentially by auto
{
fix n assume *: "u n x ≤ C - d * n" "n > N"
then have "n ≥ N" "n > 0" by auto
have "2 * u n x ≤ 2 * C - 2 * d * n" using * by auto
moreover have "2 * u n x ≥ - d * n" using N[OF ‹n ≥ N›] ‹n > 0› by (simp add: divide_simps)
ultimately have "- d * n ≤ 2 * C - 2 * d * n" by auto
then have "d * n ≤ 2 * C" by auto
then have "n ≤ 2 * C / d" using ‹d>0› by (simp add: mult.commute divide_simps)
}
then have "{n. u n x ≤ C - d * n} ⊆ {..max (nat (floor(2*C/d))) N}"
by (auto, meson le_max_iff_disj le_nat_floor not_le)
then have "finite {n. u n x ≤ C - d * n}"
using finite_subset by blast
then have "finite (U x)" using * finite_subset by blast
then show ?thesis using upper_asymptotic_density_finite by auto
qed
text ‹Main step: control of $u$ along the sequence $ns+t$, with a term
$-(d/2) Card(V(x) \cap [1,ns+t])$ on the right.
Then, after averaging in $t$, Birkhoff theorem will imply that
$Card(V(x) \cap [1,n])$ is suitably small.›
define Z where "Z = (λt n x. Max {u i x|i. i< s} + (∑i<n. abs(u s ((T^^(i * s + t))x)))
+ birkhoff_sum F (n * s + t) x - (d/2) * card(V x ∩ {1..n * s + t}))"
have Main: "u (n * s + t) x ≤ Z t n x" if "t < s" for n x t
proof (rule nat_less_induct[where ?n = n])
fix n assume H: "∀m<n. u (m * s + t) x ≤ Z t m x"
consider "n = 0"|"n>0 ∧ V x ∩ {(n-1) * s+t<..n * s+t} = {}"|"n>0 ∧ V x ∩ {(n-1) * s+t<..n * s+t} ≠ {}" by auto
then show "u (n * s+t) x ≤ Z t n x"
proof (cases)
assume "n = 0"
then have "V x ∩ {1..n * s + t} = {}" unfolding V_def using ‹t<s› ‹k>2* s› by auto
then have *: "card(V x ∩ {1..n * s+t}) = 0" by simp
have **: "0 ≤ (∑i<t. F ((T ^^ i) x))" by (rule sum_nonneg, simp add: F_pos)
have "u (n * s + t) x = u t x" using ‹n = 0› by auto
also have "... ≤ Max {u i x|i. i< s}" by (rule Max_ge, auto simp add: ‹t<s›)
also have "... ≤ Z t n x"
unfolding Z_def birkhoff_sum_def using ‹n = 0› * ** by auto
finally show ?thesis by simp
next
assume A: "n>0 ∧ V x ∩ {(n-1) * s+t<..n * s+t} = {}"
then have "n≥1" by simp
have "n * s + t = (n-1) * s + t + s" using ‹n≥1› by (simp add: add.commute add.left_commute mult_eq_if)
have "V x ∩ {1..n * s + t} = V x ∩ {1..(n-1) * s + t} ∪ V x ∩ {(n-1) * s + t<..n * s + t}"
using ‹n≥1› by (auto, simp add: mult_eq_if)
then have *: "card(V x ∩ {1..n * s+t}) = card(V x ∩ {1..(n-1) * s+t})" using A by auto
have **: "birkhoff_sum F ((n-1) * s + t) x ≤ birkhoff_sum F (n * s + t) x"
unfolding birkhoff_sum_def apply (rule sum_mono2)
using ‹n * s+t = (n-1) * s+t + s› F_pos by auto
have "(∑i<n-1. abs(u s ((T^^(i * s+t))x))) + u s ((T^^((n-1) * s+t)) x)
≤ (∑i<n-1. abs(u s ((T^^(i * s+t))x))) + abs(u s ((T^^((n-1) * s+t)) x))" by auto
also have "... ≤ (∑i<n. abs(u s ((T^^(i* s+t))x)))"
using ‹n≥1› lessThan_Suc_atMost sum.lessThan_Suc[of "λi. abs(u s ((T^^(i* s+t))x))" "n-1", symmetric] by auto
finally have ***: "(∑i<n-1. abs(u s ((T^^(i* s+t))x))) + u s ((T^^((n-1) * s+t)) x) ≤ (∑i<n. abs(u s ((T^^(i* s+t))x)))"
by simp
have "u (n * s+t) x = u ((n-1) * s+t + s) x"
using ‹n≥1› by (simp add: add.commute add.left_commute mult_eq_if)
also have "... ≤ u ((n-1) * s+t) x + u s ((T^^((n-1) * s+t)) x)"
using subcocycle_ineq[OF subu, of "(n-1) * s+t" s x] by simp
also have "... ≤ Max {u i x|i. i< s} + (∑i<n-1. abs(u s ((T^^(i* s+t))x)))
+ birkhoff_sum F ((n-1) * s+t) x - (d/2) * card(V x ∩ {1..(n-1) * s+t}) + u s ((T^^((n-1) * s+t)) x)"
using H ‹n≥1› unfolding Z_def by auto
also have "... ≤ Max {u i x|i. i< s} + (∑i<n. abs(u s ((T^^(i* s+t))x)))
+ birkhoff_sum F (n * s+t) x - (d/2) * card(V x ∩ {1..n * s+t})"
using * ** *** by auto
also have "... ≤ Z t n x" unfolding Z_def by (auto simp add: divide_simps)
finally show ?thesis by simp
next
assume B: "n>0 ∧ V x ∩ {(n-1) * s+t<..n * s+t} ≠ {}"
then have [simp]: "n>0" "n≥1" "n ≠ 0" by auto
obtain m where m: "m ∈ V x ∩ {(n-1) * s + t<..n * s + t}" using B by blast
then obtain l where l: "l ∈ {k..m-s}" "u m x - u (m-l) x ≤ - d * l" unfolding V_def by auto
then have "m-s>0" using ‹k>2* s› by auto
then have "m-l ≥ s" using l by auto
define p where "p = (m-l-t) div s"
have p1: "m-l ≥ p * s + t"
unfolding p_def using ‹m-l ≥ s› ‹s>t› minus_mod_eq_div_mult [symmetric, of "m - l - t" s]
by simp
have p2: "m-l < p* s + t + s"
unfolding p_def using ‹m-l ≥ s› ‹s>t›
div_mult_mod_eq[of "m-l-t" s] mod_less_divisor[OF ‹s>0›, of "m-l-t"] by linarith
then have "l ≥ m - p * s - t -s" by auto
then have "l ≥ (n-1) * s + t -p * s - t- s" using m by auto
then have "l + 2 * s≥ (n * s + t) - (p * s+t)" by (simp add: diff_mult_distrib)
have "(p+1) * s + t ≤ (n-1) * s + t"
using ‹k> 2 * s› m l(1) p1 by (auto simp add: algebra_simps)
then have "p+1 ≤ n-1"
using ‹s>0› by (meson add_le_cancel_right mult_le_cancel2)
then have "p ≤ n-1" "p<n" by auto
have "(p* s + t) + k ≤ (n * s + t)"
using m l(1) p1 by (auto simp add: algebra_simps)
then have "(1::real) ≤ ((n * s + t) - (p* s + t)) / k"
using ‹k > 2* s› by auto
have In: "u (n * s + t) x ≤ u m x + (∑i ∈ {(n-1) * s + t..<n * s + t}. abs(u 1 ((T^^i) x)))"
proof (cases "m = n * s + t")
case True
have "(∑i ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x))) ≥ 0"
by (rule sum_nonneg, auto)
then show ?thesis using True by auto
next
case False
then have m2: "n * s + t - m >0" "(n-1) * s+t ≤ m" using m by auto
have "birkhoff_sum (u 1) (n * s+t-m) ((T^^m) x) = (∑i<n * s+t-m. u 1 ((T^^i)((T^^m) x)))"
unfolding birkhoff_sum_def by auto
also have "... = (∑i<n * s+t-m. u 1 ((T^^(i+m)) x))"
by (simp add: funpow_add)
also have "... = (∑j ∈ {m..<n * s+t}. u 1 ((T^^j) x))"
by (rule sum.reindex_bij_betw, rule bij_betw_byWitness[where ?f' = "λi. i - m"], auto)
also have "... ≤ (∑j ∈ {m..<n * s+t}. abs(u 1 ((T^^j) x)))"
by (rule sum_mono, auto)
also have "... ≤ (∑j ∈ {(n-1) * s+t..<m}. abs(u 1 ((T^^j) x))) + (∑j ∈ {m..<n * s+t}. abs(u 1 ((T^^j) x)))"
by auto
also have "... = (∑j ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^j) x)))"
apply (rule sum.atLeastLessThan_concat) using m2 by auto
finally have *: "birkhoff_sum (u 1) (n * s+t-m) ((T^^m) x) ≤ (∑j ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^j) x)))"
by auto
have "u (n * s+t) x ≤ u m x + u (n * s+t-m) ((T^^m) x)"
using subcocycle_ineq[OF subu, of m "n * s+t-m"] m2 by auto
also have "... ≤ u m x + birkhoff_sum (u 1) (n * s+t-m) ((T^^m) x)"
using subcocycle_bounded_by_birkhoff1[OF subu ‹n * s+t - m >0›, of "(T^^m)x"] by simp
finally show ?thesis using * by auto
qed
have Ip: "u (m-l) x ≤ u (p* s+t) x + (∑i ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^i) x)))"
proof (cases "m-l = p* s+t")
case True
have "(∑i ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^i) x))) ≥ 0"
by (rule sum_nonneg, auto)
then show ?thesis using True by auto
next
case False
then have "m-l - (p* s+t) > 0" using p1 by auto
have I: "p * s + t + (m - l - (p * s + t)) = m - l" using p1 by auto
have "birkhoff_sum (u 1) (m-l - (p* s+t)) ((T^^(p* s+t)) x) = (∑i<m-l - (p* s+t). u 1 ((T^^i) ((T^^(p* s+t)) x)))"
unfolding birkhoff_sum_def by auto
also have "... = (∑i<m-l - (p* s+t). u 1 ((T^^(i+p* s+t)) x))"
by (simp add: funpow_add)
also have "... = (∑j ∈ {p* s+t..<m-l}. u 1 ((T^^j) x))"
by (rule sum.reindex_bij_betw, rule bij_betw_byWitness[where ?f' = "λi. i - (p* s+t)"], auto)
also have "... ≤ (∑j ∈ {p* s+t..<m-l}. abs(u 1 ((T^^j) x)))"
by (rule sum_mono, auto)
also have "... ≤ (∑j ∈ {p* s+t..<m-l}. abs(u 1 ((T^^j) x))) + (∑j ∈ {m-l..<(p+1)* s+t}. abs(u 1 ((T^^j) x)))"
by auto
also have "... = (∑j ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^j) x)))"
apply (rule sum.atLeastLessThan_concat) using p1 p2 by auto
finally have *: "birkhoff_sum (u 1) (m-l - (p* s+t)) ((T^^(p* s+t)) x)
≤ (∑j ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^j) x)))"
by auto
have "u (m-l) x ≤ u (p* s+t) x + u (m-l - (p* s+t)) ((T^^(p* s+t)) x)"
using subcocycle_ineq[OF subu, of "p* s+t" "m-l - (p* s+t)" x] I by auto
also have "... ≤ u (p* s+t) x + birkhoff_sum (u 1) (m-l - (p* s+t)) ((T^^(p* s+t)) x)"
using subcocycle_bounded_by_birkhoff1[OF subu ‹m-l - (p* s+t) > 0›, of "(T^^(p* s+t)) x"] by simp
finally show ?thesis using * by auto
qed
have "(∑i ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^i) x))) ≤ (∑i ∈ {p* s+t..<(p+1)* s+t}. K + F ((T^^i) x))"
apply (rule sum_mono) using u1_bound by auto
moreover have "(∑i ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x))) ≤ (∑i ∈ {(n-1) * s+t..<n * s+t}. K + F ((T^^i) x))"
apply (rule sum_mono) using u1_bound by auto
ultimately have "(∑i ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^i) x))) + (∑i ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x)))
≤ (∑i ∈ {p* s+t..<(p+1)* s+t}. K + F ((T^^i) x)) + (∑i ∈ {(n-1) * s+t..<n * s+t}. K + F ((T^^i) x))"
by auto
also have "... = 2* K* s + (∑i ∈ {p* s+t..<(p+1)* s+t}. F ((T^^i) x)) + (∑i ∈{(n-1) * s+t..<n * s+t}. F ((T^^i) x))"
by (auto simp add: mult_eq_if sum.distrib)
also have "... ≤ 2* K * s + (∑i ∈ {p* s+t..<(n-1) * s+t}. F ((T^^i) x)) + (∑i ∈{(n-1) * s+t..<n * s+t}. F ((T^^i) x))"
apply (auto, rule sum_mono2) using ‹(p+1)* s+t≤(n-1) * s+t› F_pos by auto
also have "... = 2* K * s + (∑i ∈ {p* s+t..<n * s+t}. F ((T^^i) x))"
apply (auto, rule sum.atLeastLessThan_concat) using ‹p≤n-1› by auto
finally have A0: "(∑i ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^i) x))) + (∑i ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x)))
≤ 2* K * s + (∑i ∈ {p* s+t..<n * s+t}. F ((T^^i) x))"
by simp
have "card(V x ∩ {p * s + t<.. n * s+t}) ≤ card {p * s + t<.. n * s+t}" by (rule card_mono, auto)
have "2 * d * s + 2 * K * s > 0" using ‹K>0› ‹s>0› ‹d>0›
by (metis add_pos_pos mult_2 mult_zero_left of_nat_0_less_iff pos_divide_less_eq times_divide_eq_right)
then have "2 * d * s + 2 * K * s ≤ ((n * s + t) - (p* s + t)) * ((2 * d * s + 2 * K * s) / k)"
using ‹1 ≤ ((n * s + t) - (p* s + t)) / k› by (simp add: le_divide_eq_1 pos_le_divide_eq)
also have "... ≤ ((n * s + t) - (p* s + t)) * (d/2)"
apply (rule mult_left_mono) using ‹(2 * d * s + 2 * K * s)/k ≤ d/2› by auto
finally have "2 * d * s + 2 * K * s ≤ ((n * s + t) - (p* s + t)) * (d/2)"
by auto
then have "-d * ((n * s+t) - (p* s+t)) + 2 * d * s + 2 * K * s ≤ -d * ((n * s+t) - (p* s+t)) + ((n * s + t) - (p* s + t)) * (d/2)"
by linarith
also have "... = (-d/2) * card {p * s + t<.. n * s+t}"
by auto
also have "... ≤ (-d/2) * card(V x ∩ {p * s + t<.. n * s+t})"
using ‹card(V x ∩ {p * s + t<.. n * s+t}) ≤ card {p * s + t<.. n * s+t}› by auto
finally have A1: "-d * ((n * s+t) - (p* s+t)) + 2 * d * s + 2 * K * s ≤ (-d/2) * card(V x ∩ {p * s + t<.. n * s+t})"
by simp
have "V x ∩ {1.. n * s+t} = V x ∩ {1..p * s + t} ∪ V x ∩ {p * s + t<.. n * s+t}"
using ‹p * s + t + k ≤ n * s + t› by auto
then have "card (V x ∩ {1.. n * s+t}) = card(V x ∩ {1..p * s + t} ∪ V x ∩ {p * s + t<.. n * s+t})"
by auto
also have "... = card (V x ∩ {1..p * s + t}) + card (V x ∩ {p * s + t<.. n * s+t})"
by (rule card_Un_disjoint, auto)
finally have A2: "card (V x ∩ {1..p * s + t}) + card (V x ∩ {p * s + t<.. n * s+t}) = card (V x ∩ {1.. n * s+t})"
by simp
have A3: "(∑i<p. abs(u s ((T ^^ (i * s + t)) x))) ≤ (∑i<n. abs(u s ((T ^^ (i * s + t)) x)))"
apply (rule sum_mono2) using ‹p≤n-1› by auto
have A4: "birkhoff_sum F (p * s + t) x + (∑i ∈ {p* s+t..<n * s+t}. F ((T^^i) x)) = birkhoff_sum F (n * s + t) x"
unfolding birkhoff_sum_def apply (subst atLeast0LessThan[symmetric])+ apply (rule sum.atLeastLessThan_concat)
using ‹p≤n-1› by auto
have "u (n * s+t) x ≤ u m x + (∑i ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x)))"
using In by simp
also have "... ≤ (u m x - u (m-l) x) + u (m-l) x + (∑i ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x)))"
by simp
also have "... ≤ - d * l + u (p* s+t) x + (∑i ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^i) x))) + (∑i ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x)))"
using Ip l by auto
also have "... ≤ - d * ((n * s+t) - (p* s+t)) + 2*d* s + u (p* s+t) x + (∑i ∈ {p* s+t..<(p+1)* s+t}. abs(u 1 ((T^^i) x))) + (∑i ∈ {(n-1) * s+t..<n * s+t}. abs(u 1 ((T^^i) x)))"
using ‹l + 2* s≥ (n * s+t) - (p* s+t)› apply (auto simp add: algebra_simps)
by (metis assms(1) distrib_left mult.commute mult_2 of_nat_add of_nat_le_iff mult_le_cancel_left_pos)
also have "... ≤ -d * ((n * s+t) - (p* s+t)) + 2*d* s + Z t p x + 2* K * s + (∑i ∈ {p* s+t..<n * s+t}. F ((T^^i) x))"
using A0 H ‹p<n› by auto
also have "... ≤ Z t p x - d/2 * card(V x ∩ {p * s + t<.. n * s+t}) + (∑i ∈ {p* s+t..<n * s+t}. F ((T^^i) x))"
using A1 by auto
also have "... = Max {u i x |i. i < s} + (∑i<p. abs(u s ((T ^^ (i * s + t)) x))) + birkhoff_sum F (p * s + t) x
- d / 2 * card (V x ∩ {1..p * s + t}) - d/2 * card(V x ∩ {p * s + t<.. n * s+t}) + (∑i ∈ {p* s+t..<n * s+t}. F ((T^^i) x))"
unfolding Z_def by auto
also have "... ≤ Max {u i x |i. i < s} + (∑i<n. abs(u s ((T ^^ (i * s + t)) x)))
+ (birkhoff_sum F (p * s + t) x + (∑i ∈ {p* s+t..<n * s+t}. F ((T^^i) x)))
- d/2 * card (V x ∩ {1..p * s + t}) - d/2 * card(V x ∩ {p * s + t<.. n * s+t})"
using A3 by auto
also have "... = Z t n x"
unfolding Z_def using A2 A4 by (auto simp add: algebra_simps, metis distrib_left of_nat_add)
finally show ?thesis by simp
qed
qed
have Main2: "(d/2) * card(V x ∩ {1..n}) ≤ Max {u i x|i. i< s} + birkhoff_sum (λx. abs(u s x/ s)) (n+2* s) x
+ birkhoff_sum F (n + 2 * s) x + (1/s) * (∑i< 2 * s. abs(u (n+i) x))" for n x
proof -
define N where "N = (n div s) + 1"
then have "n ≤ N * s"
using ‹s > 0› dividend_less_div_times less_or_eq_imp_le by auto
have "N * s ≤ n + s"
by (auto simp add: N_def)
have eq_t: "(d/2) * card(V x ∩ {1..n}) ≤ abs(u(N* s+t) x) + (Max {u i x|i. i< s} + birkhoff_sum F (n + 2* s) x)
+ (∑i<N. abs(u s ((T^^(i * s+t))x)))"
if "t<s" for t
proof -
have *: "birkhoff_sum F (N * s+t) x ≤ birkhoff_sum F (n+ 2* s) x"
unfolding birkhoff_sum_def apply (rule sum_mono2) using F_pos ‹N * s ≤ n + s› ‹t<s› by auto
have "card(V x ∩ {1..n}) ≤ card(V x ∩ {1..N* s+t})"
apply (rule card_mono) using ‹n ≤ N * s› by auto
then have "(d/2) * card(V x ∩ {1..n}) ≤ (d/2) * card(V x ∩ {1..N* s+t})"
by auto
also have "... ≤ - u (N* s+t) x + Max {u i x|i. i< s} + (∑i<N. abs(u s ((T^^(i* s+t))x))) + birkhoff_sum F (N * s+t) x"
using Main[OF ‹t < s›, of N x] unfolding Z_def by auto
also have "... ≤ abs(u(N* s+t) x) + Max {u i x|i. i< s} + birkhoff_sum F (n + 2* s) x + (∑i<N. abs(u s ((T^^(i* s+t))x)))"
using * by auto
finally show ?thesis by simp
qed
have "(∑t<s. abs(u(N* s+t) x)) = (∑i∈{N* s..<N* s+s}. abs (u i x))"
by (rule sum.reindex_bij_betw, rule bij_betw_byWitness[where ?f' = "λi. i - N* s"], auto)
also have "... ≤ (∑i∈{n..<n + 2* s}. abs (u i x))"
apply (rule sum_mono2) using ‹n ≤ N * s› ‹N * s ≤ n + s› by auto
also have "... = (∑i<2* s. abs (u (n+i) x))"
by (rule sum.reindex_bij_betw[symmetric], rule bij_betw_byWitness[where ?f' = "λi. i - n"], auto)
finally have **: "(∑t<s. abs(u(N* s+t) x)) ≤ (∑i<2* s. abs (u (n+i) x))"
by simp
have "(∑t<s. (∑i<N. abs(u s ((T^^(i* s+t))x)))) = (∑i<N* s. abs(u s ((T^^i) x)))"
by (rule sum_arith_progression)
also have "... ≤ (∑i<n + 2* s. abs(u s ((T^^i) x)))"
apply (rule sum_mono2) using ‹N * s ≤ n + s› by auto
finally have ***: "(∑t<s. (∑i<N. abs(u s ((T^^(i* s+t))x)))) ≤ s * birkhoff_sum (λx. abs(u s x/ s)) (n+2* s) x"
unfolding birkhoff_sum_def using ‹s>0› by (auto simp add: sum_divide_distrib[symmetric])
have ****: "s * (∑i<n + 2* s. abs(u s ((T^^i) x)) /s) = (∑i<n + 2* s. abs(u s ((T^^i) x)))"
by (auto simp add: sum_divide_distrib[symmetric])
have "s * (d/2) * card(V x ∩ {1..n}) = (∑t<s. (d/2) * card(V x ∩ {1..n}))"
by auto
also have "... ≤ (∑t<s. abs(u(N* s+t) x) + (Max {u i x|i. i< s} + birkhoff_sum F (n + 2* s) x)
+ (∑i<N. abs(u s ((T^^(i* s+t))x))))"
apply (rule sum_mono) using eq_t by auto
also have "... = (∑t<s. abs(u(N* s+t) x)) + (∑t<s. Max {u i x|i. i< s} + birkhoff_sum F (n + 2* s) x) + (∑t<s. (∑i<N. abs(u s ((T^^(i* s+t))x))))"
by (auto simp add: sum.distrib)
also have "... ≤ (∑i<2* s. abs (u (n+i) x)) + s * (Max {u i x|i. i< s} + birkhoff_sum F (n + 2* s) x) + s * birkhoff_sum (λx. abs(u s x/ s)) (n+2* s) x"
using ** *** by auto
also have "... = s * ((1/s) * (∑i<2* s. abs (u (n+i) x)) + Max {u i x|i. i< s} + birkhoff_sum F (n + 2* s) x + birkhoff_sum (λx. abs(u s x/ s)) (n+2* s) x)"
by (auto simp add: divide_simps mult.commute distrib_left)
finally show ?thesis
by auto
qed
have densV: "upper_asymptotic_density (V x) ≤ (2/d) * real_cond_exp M Invariants F2 x" if "x ∈ G" for x
proof -
have *: "(λn. abs(u n x/n)) ⇢ 0"
apply (rule tendsto_rabs_zero) using ‹x∈G› unfolding G_def by auto
define Bound where "Bound = (λn. (Max {u i x|i. i< s}*(1/n) + birkhoff_sum (λx. abs(u s x/ s)) (n+2* s) x / n
+ birkhoff_sum F (n + 2* s) x / n + (1/s) * (∑i<2* s. abs(u (n+i) x) / n)))"
have "Bound ⇢ (Max {u i x|i. i< s} * 0 + real_cond_exp M Invariants (λx. abs(u s x/s)) x
+ real_cond_exp M Invariants F x + (1/s) * (∑i < 2 * s. 0))"
unfolding Bound_def apply (intro tendsto_intros)
using ‹x∈G› * unfolding G_def by auto
moreover have "real_cond_exp M Invariants (λx. abs(u s x/s)) x + real_cond_exp M Invariants F x = real_cond_exp M Invariants F2 x"
using ‹x ∈ G› unfolding G_def by auto
ultimately have B_conv: "Bound ⇢ real_cond_exp M Invariants F2 x" by simp
have *: "(d/2) * card(V x ∩ {1..n}) / n ≤ Bound n" for n
proof -
have "(d/2) * card(V x ∩ {1..n}) / n ≤ (Max {u i x|i. i< s} + birkhoff_sum (λx. abs(u s x/ s)) (n+2* s) x
+ birkhoff_sum F (n + 2* s) x + (1/s) * (∑i<2* s. abs(u (n+i) x)))/n"
using Main2[of x n] using divide_right_mono of_nat_0_le_iff by blast
also have "... = Bound n"
unfolding Bound_def by (auto simp add: add_divide_distrib sum_divide_distrib[symmetric])
finally show ?thesis by simp
qed
have "ereal(d/2 * upper_asymptotic_density (V x)) = ereal(d/2) * ereal(upper_asymptotic_density (V x))"
by auto
also have "... = ereal (d/2) * limsup(λn. card(V x ∩ {1..n}) / n)"
using upper_asymptotic_density_shift[of "V x" 1 0] by auto
also have "... = limsup(λn. ereal (d/2) * (card(V x ∩ {1..n}) / n))"
by (rule limsup_ereal_mult_left[symmetric], auto)
also have "... ≤ limsup Bound"
apply (rule Limsup_mono) using * not_eventuallyD by auto
also have "... = ereal(real_cond_exp M Invariants F2 x)"
using B_conv convergent_limsup_cl convergent_def convergent_real_imp_convergent_ereal limI by force
finally have "d/2 * upper_asymptotic_density (V x) ≤ real_cond_exp M Invariants F2 x"
by auto
then show ?thesis
by (simp add: divide_simps mult.commute)
qed
define epsilon where "epsilon = 2 * rho / d"
have [simp]: "epsilon > 0" "epsilon ≠ 0" "epsilon ≥ 0" unfolding epsilon_def by auto
have "emeasure M {x∈space M. real_cond_exp M Invariants F2 x ≥ epsilon} ≤ (1/epsilon) * (∫x. real_cond_exp M Invariants F2 x ∂M)"
apply (intro integral_Markov_inequality real_cond_exp_pos real_cond_exp_int(1))
by (auto simp add: int_F2 F2_pos)
also have "... = (1/epsilon) * (∫x. F2 x ∂M)"
apply (intro arg_cong[where f = ennreal])
by (simp, rule real_cond_exp_int(2), simp add: int_F2)
also have "... < (1/epsilon) * 2 * rho"
using F2_int by (intro ennreal_lessI) (auto simp add: divide_simps)
also have "... = d"
unfolding epsilon_def by auto
finally have *: "emeasure M {x∈space M. real_cond_exp M Invariants F2 x ≥ epsilon} < d"
by simp
define G2 where "G2 = {x ∈ G. real_cond_exp M Invariants F2 x < epsilon}"
have [measurable]: "G2 ∈ sets M" unfolding G2_def by simp
have "1 = emeasure M G"
using ‹emeasure M G = 1› by simp
also have "... ≤ emeasure M (G2 ∪ {x∈space M. real_cond_exp M Invariants F2 x ≥ epsilon})"
apply (rule emeasure_mono) unfolding G2_def using sets.sets_into_space[OF ‹G ∈ sets M›] by auto
also have "... ≤ emeasure M G2 + emeasure M {x∈space M. real_cond_exp M Invariants F2 x ≥ epsilon}"
by (rule emeasure_subadditive, auto)
also have "... < emeasure M G2 + d"
using * by auto
finally have "1 - d < emeasure M G2"
using emeasure_eq_measure ‹d ≤ 1› by (auto intro!: ennreal_less_iff[THEN iffD2] simp del: ennreal_plus simp add: ennreal_plus[symmetric])
have "upper_asymptotic_density {n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - d * l} < d"
if "x ∈ G2" for x
proof -
have "x ∈ G" using ‹x ∈ G2› unfolding G2_def by auto
have "{n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - d * l} ⊆ U x ∪ V x"
unfolding U_def V_def by fastforce
then have "upper_asymptotic_density {n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - d * l} ≤ upper_asymptotic_density (U x ∪ V x)"
by (rule upper_asymptotic_density_subset)
also have "... ≤ upper_asymptotic_density (U x) + upper_asymptotic_density (V x)"
by (rule upper_asymptotic_density_union)
also have "... ≤ (2/d) * real_cond_exp M Invariants F2 x"
using densU[OF ‹x ∈ G›] densV[OF ‹x ∈ G›] by auto
also have "... < (2/d) * epsilon"
using ‹x ∈ G2› unfolding G2_def by (simp add: divide_simps)
text ‹This is where the choice of $\rho$ at the beginning of the proof is relevant:
we choose it so that the above term is at most $d$.›
also have "... = d" unfolding epsilon_def rho_def by auto
finally show ?thesis by simp
qed
then have "G2 ⊆ {x ∈ space M. upper_asymptotic_density {n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - d * l} < d}"
using sets.sets_into_space[OF ‹G2 ∈ sets M›] by blast
then have "emeasure M G2 ≤ emeasure M {x ∈ space M. upper_asymptotic_density {n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - d * l} < d}"
by (rule emeasure_mono, auto)
then have "emeasure M {x ∈ space M. upper_asymptotic_density {n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - d * l} < d} > 1 -d"
using ‹emeasure M G2 > 1 - d› by auto
then show ?thesis by blast
qed
text ‹The two previous lemmas are put together in the following lemma,
corresponding to Lemma 2.3 in~\<^cite>‹"gouezel_karlsson"›.›
lemma upper_density_delta:
fixes d::real
assumes "d > 0" "d ≤ 1"
shows "∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
emeasure M {x ∈ space M. ∀(N::nat). card {n ∈{..<N}. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - delta l * l} ≤ d * N} > 1 - d"
proof -
define d2 where "d2 = d/2"
have [simp]: "d2 > 0" unfolding d2_def using assms by simp
then have "¬ d2 < 0" using not_less [of d2 0] by (simp add: less_le)
have "d2/2 > 0" by simp
obtain c0 where c0: "c0> (0::real)" "emeasure M {x ∈ space M. upper_asymptotic_density {n. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - c0 * l} < d2/2} > 1 - (d2/2)"
using upper_density_all_times[OF ‹d2/2 > 0›] by blast
have "∃N. emeasure M {x ∈ space M. ∀n ≥ N. card ({n. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - c0 * l} ∩ {..<n}) < (d2/2) * n} > 1 - (d2/2)"
apply (rule upper_density_eventually_measure) using c0(2) by auto
then obtain N1 where N1: "emeasure M {x ∈ space M. ∀B ≥ N1. card ({n. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - c0 * l} ∩ {..<B}) < (d2/2) * B} > 1 - (d2/2)"
by blast
define O1 where "O1 = {x ∈ space M. ∀B ≥ N1. card ({n. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - c0 * l} ∩ {..<B}) < (d2/2) * B}"
have [measurable]: "O1 ∈ sets M" unfolding O1_def by auto
have "emeasure M O1 > 1 - (d2/2)" unfolding O1_def using N1 by auto
have *: "∃N. emeasure M {x ∈ space M. ∀B ≥ N. card({n. ∃l ∈ {N..n}. u n x - u (n-l) x ≤ - e * l} ∩ {..<B}) < e * B} > 1 - e"
if "e>0" "e ≤ 1" for e::real
proof -
obtain k where k: "emeasure M {x ∈ space M. upper_asymptotic_density {n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - e * l} < e} > 1 - e"
using upper_density_large_k[OF ‹e>0› ‹e ≤ 1›] by blast
then obtain N0 where N0: "emeasure M {x ∈ space M. ∀B ≥ N0. card({n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - e * l} ∩ {..<B}) < e * B} > 1 - e"
using upper_density_eventually_measure[OF _ k] by auto
define N where "N = max k N0"
have "emeasure M {x ∈ space M. ∀B ≥ N0. card({n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ - e * l} ∩ {..<B}) < e * B}
≤ emeasure M {x ∈ space M. ∀B ≥ N. card({n. ∃l ∈ {N..n}. u n x - u (n-l) x ≤ - e * l} ∩ {..<B}) < e * B}"
proof (rule emeasure_mono, auto)
fix x B assume H: "x ∈ space M" "∀B≥N0. card ({n. ∃l∈{k..n}. u n x - u (n - l) x ≤ - (e * real l)} ∩ {..<B}) < e * B" "N ≤ B"
have "card({n. ∃l ∈ {N..n}. u n x - u (n-l) x ≤ - (e * real l)} ∩ {..<B}) ≤ card({n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ -(e * real l)} ∩ {..<B})"
unfolding N_def by (rule card_mono, auto)
then have "real(card({n. ∃l ∈ {N..n}. u n x - u (n-l) x ≤ - (e * real l)} ∩ {..<B})) ≤ card({n. ∃l ∈ {k..n}. u n x - u (n-l) x ≤ -(e * real l)} ∩ {..<B})"
by simp
also have "... < e * B" using H(2) ‹B≥N› unfolding N_def by auto
finally show "card ({n. ∃l∈{N..n}. u n x - u (n - l) x ≤ - (e * real l)} ∩ {..<B}) < e * B"
by auto
qed
then have "emeasure M {x ∈ space M. ∀B ≥ N. card({n. ∃l ∈ {N..n}. u n x - u (n-l) x ≤ - e * l} ∩ {..<B}) < e * B} > 1 - e"
using N0 by simp
then show ?thesis by auto
qed
define Ne where "Ne = (λ(e::real). SOME N. emeasure M {x ∈ space M. ∀B ≥ N. card({n. ∃l ∈ {N..n}. u n x - u (n-l) x ≤ - e * l} ∩ {..<B}) < e * B} > 1 - e)"
have Ne: "emeasure M {x ∈ space M. ∀B ≥ Ne e. card({n. ∃l ∈ {Ne e..n}. u n x - u (n-l) x ≤ - e * l} ∩ {..<B}) < e * B} > 1 - e"
if "e>0" "e ≤ 1" for e::real
unfolding Ne_def by (rule someI_ex[OF *[OF that]])
define eps where "eps = (λ(n::nat). d2 * (1/2)^n)"
have [simp]: "eps n > 0" for n unfolding eps_def by auto
then have [simp]: "eps n ≥ 0" for n by (rule less_imp_le)
have "eps n ≤ (1 / 2) * 1" for n
unfolding eps_def d2_def
using ‹d ≤ 1› by (intro mult_mono power_le_one) auto
also have "… < 1" by auto
finally have [simp]: "eps n < 1" for n by simp
then have [simp]: "eps n ≤ 1" for n by (rule less_imp_le)
have "(λn. d2 * (1/2)^n) ⇢ d2 * 0"
by (rule tendsto_mult, auto simp add: LIMSEQ_realpow_zero)
then have "eps ⇢ 0" unfolding eps_def by auto
define Nf where "Nf = (λN. (if (N = 0) then 0
else if (N = 1) then N1 + 1
else max (N1+1) (Max {Ne(eps n)|n. n ≤ N}) + N))"
have "Nf N < Nf (N+1)" for N
proof -
consider "N = 0" | "N = 1" | "N>1" by fastforce
then show ?thesis
proof (cases)
assume "N>1"
have "Max {Ne (eps n) |n. n ≤ N} ≤ Max {Ne (eps n) |n. n ≤ Suc N}"
by (rule Max_mono, auto)
then show ?thesis unfolding Nf_def by auto
qed (auto simp add: Nf_def)
qed
then have "strict_mono Nf"
using strict_mono_Suc_iff by auto
define On where "On = (λ(N::nat).
(if (N = 1) then O1
else {x ∈ space M. ∀B ≥ Nf N. card({n. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N) * l} ∩ {..<B}) < (eps N) * B}))"
have [measurable]: "On N ∈ sets M" for N unfolding On_def by auto
have "emeasure M (On N) > 1 - eps N" if "N>0" for N
proof -
consider "N = 1" | "N>1" using ‹N>0› by linarith
then show ?thesis
proof (cases)
case 1
then show ?thesis unfolding On_def eps_def using ‹emeasure M O1 > 1 - (d2/2)› by auto
next
case 2
have "Ne (eps N) ≤ Max {Ne(eps n)|n. n ≤ N}"
by (rule Max.coboundedI, auto)
also have "... ≤ Nf N" unfolding Nf_def using ‹N>1› by auto
finally have "Ne (eps N) ≤ Nf N" by simp
have "1 - eps N < emeasure M {x ∈ space M. ∀B ≥ Ne(eps N). card({n. ∃l ∈ {Ne(eps N)..n}. u n x - u (n-l) x ≤ - (eps N) * l} ∩ {..<B}) < (eps N) * B}"
by (rule Ne) simp_all
also have "... ≤ emeasure M {x ∈ space M. ∀B ≥ Nf N. card({n. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N) * l} ∩ {..<B}) < (eps N) * B}"
proof (rule emeasure_mono, auto)
fix x n assume H: "x ∈ space M"
"∀n≥Ne (eps N). card ({n. ∃l∈{Ne (eps N)..n}. u n x - u (n - l) x ≤ - (eps N * l)} ∩ {..<n}) < eps N * n"
"Nf N ≤ n"
have "card({n. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<n}) ≤ card({n. ∃l ∈ {Ne(eps N)..n}. u n x - u (n-l) x ≤ -(eps N) * l} ∩ {..<n})"
apply (rule card_mono) using ‹Ne (eps N) ≤ Nf N› by auto
then have "real(card({n. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<n})) ≤ card({n. ∃l ∈ {Ne(eps N)..n}. u n x - u (n-l) x ≤ -(eps N) * l} ∩ {..<n})"
by simp
also have "... < (eps N) * n" using H(2) ‹n ≥ Nf N› ‹Ne (eps N) ≤ Nf N› by auto
finally show "real (card ({n. ∃l∈{Nf N..n}. u n x - u (n - l) x ≤ - (eps N * l)} ∩ {..<n})) < eps N * real n"
by auto
qed
also have "... = emeasure M (On N)"
unfolding On_def using ‹N>1› by auto
finally show ?thesis by simp
qed
qed
then have *: "emeasure M (On (N+1)) > 1 - eps (N+1)" for N by simp
define Ogood where "Ogood = (⋂N. On (N+1))"
have [measurable]: "Ogood ∈ sets M" unfolding Ogood_def by auto
have "emeasure M Ogood ≥ 1 - (∑N. eps(N+1))"
unfolding Ogood_def
apply (intro emeasure_intersection, auto)
using * by (auto simp add: eps_def summable_mult summable_divide summable_geometric less_imp_le)
moreover have "(∑N. eps(N+1)) = d2"
unfolding eps_def apply (subst suminf_mult)
using sums_unique[OF power_half_series, symmetric] by (auto intro!: summable_divide summable_geometric)
finally have "emeasure M Ogood ≥ 1 - d2" by simp
then have "emeasure M Ogood > 1 - d" unfolding d2_def using ‹d>0› ‹d ≤ 1›
by (simp add: emeasure_eq_measure field_sum_of_halves ennreal_less_iff)
have Ogood_union: "Ogood = (⋃(K::nat). Ogood ∩ {x ∈ space M. ∀n ∈ {1..Nf 1}. ∀l ∈ {1..n}. u n x - u (n-l) x > - (real K * l)})"
apply auto using sets.sets_into_space[OF ‹Ogood ∈ sets M›] apply blast
proof -
fix x
define M where "M = Max {abs(u n x - u (n-l) x)/l | n l. n ∈ {1..Nf 1} ∧ l ∈ {1..n}}"
obtain N::nat where "N > M" using reals_Archimedean2 by blast
have "finite { (n, l) | n l. n ∈ {1..Nf 1} ∧ l ∈ {1..n}}"
by (rule finite_subset[where ?B = "{1.. Nf 1} × {1..Nf 1}"], auto)
moreover have "{abs(u n x - u (n-l) x)/l | n l. n ∈ {1..Nf 1} ∧ l ∈ {1..n}}
= (λ (n, l). abs(u n x - u (n-l) x)/l)` { (n, l) | n l. n ∈ {1..Nf 1} ∧ l ∈ {1..n}}"
by auto
ultimately have fin: "finite {abs(u n x - u (n-l) x)/l | n l. n ∈ {1..Nf 1} ∧ l ∈ {1..n}}"
by auto
{
fix n l assume nl: "n ∈ {1..Nf 1} ∧ l ∈ {1..n}"
then have "real l>0" by simp
have "abs(u n x - u (n-l) x)/l ≤ M"
unfolding M_def apply (rule Max_ge) using fin nl by auto
then have "abs(u n x - u (n-l) x)/l < real N" using ‹N>M› by simp
then have "abs(u n x - u (n-l) x)< real N * l" using ‹0 < real l› pos_divide_less_eq by blast
then have "u n x - u (n-l) x > - (real N * l)" by simp
}
then have "∀n∈{Suc 0..Nf (Suc 0)}. ∀l∈{Suc 0..n}. - (real N * real l) < u n x - u (n - l) x"
by auto
then show "∃N. ∀n∈{Suc 0..Nf (Suc 0)}. ∀l∈{Suc 0..n}. - (real N * real l) < u n x - u (n - l) x"
by auto
qed
have "(λK. emeasure M (Ogood ∩ {x ∈ space M. ∀n ∈ {1..Nf 1}. ∀l ∈ {1..n}. u n x - u (n-l) x > - (real K * l)}))
⇢ emeasure M (⋃(K::nat). Ogood ∩ {x ∈ space M. ∀n ∈ {1..Nf 1}. ∀l ∈ {1..n}. u n x - u (n-l) x > - (real K * l)})"
apply (rule Lim_emeasure_incseq, auto)
unfolding incseq_def apply auto
proof -
fix m n x na l
assume "m ≤ (n::nat)" "∀n∈{Suc 0..Nf (Suc 0)}. ∀l∈{Suc 0..n}. - (real m * real l) < u n x - u (n - l) x"
"Suc 0 ≤ l" "l ≤ na" "na ≤ Nf (Suc 0)"
then have "- (real m * real l) < u na x - u (na - l) x" by auto
moreover have "- (real n * real l) ≤ - (real m * real l)" using ‹m ≤ n› by (simp add: mult_mono)
ultimately show "- (real n * real l) < u na x - u (na - l) x" by auto
qed
moreover have "emeasure M (⋃(K::nat). Ogood ∩ {x ∈ space M. ∀n ∈ {1..Nf 1}. ∀l ∈ {1..n}. u n x - u (n-l) x > - (real K * l)}) > 1 - d"
using Ogood_union ‹emeasure M Ogood > 1 - d› by auto
ultimately have a: "eventually (λK. emeasure M (Ogood ∩ {x ∈ space M. ∀n ∈ {1..Nf 1}. ∀l ∈ {1..n}. u n x - u (n-l) x > - (real K * l)}) > 1 - d) sequentially"
by (rule order_tendstoD(1))
have b: "eventually (λK. K ≥ max c0 d2) sequentially"
using eventually_at_top_linorder nat_ceiling_le_eq by blast
have "eventually (λK. K ≥ max c0 d2 ∧ emeasure M (Ogood ∩ {x ∈ space M. ∀n ∈ {1..Nf 1}. ∀l ∈ {1..n}. u n x - u (n-l) x > - (real K * l)}) > 1 - d) sequentially"
by (rule eventually_elim2[OF a b], auto)
then obtain K where K: "K≥max c0 d2" "emeasure M (Ogood ∩ {x ∈ space M. ∀n ∈ {1..Nf 1}. ∀l ∈ {1..n}. u n x - u (n-l) x > - (real K * l)}) > 1 - d"
using eventually_False_sequentially eventually_elim2 by blast
define Og where "Og = Ogood ∩ {x ∈ space M. ∀n ∈ {1..Nf 1}. ∀l ∈ {1..n}. u n x - u (n-l) x > - (real K * l)}"
have [measurable]: "Og ∈ sets M" unfolding Og_def by simp
have "emeasure M Og > 1 - d" unfolding Og_def using K by simp
have fin: "finite {N. Nf N ≤ n}" for n
using pseudo_inverse_finite_set[OF filterlim_subseq[OF ‹strict_mono Nf›]] by auto
define prev_N where "prev_N = (λn. Max {N. Nf N ≤ n})"
define delta where "delta = (λl. if (prev_N l ≤ 1) then K else eps (prev_N l))"
have "∀l. delta l > 0"
unfolding delta_def using ‹K≥max c0 d2› ‹c0>0› by auto
have "LIM n sequentially. prev_N n :> at_top"
unfolding prev_N_def apply (rule tendsto_at_top_pseudo_inverse2)
using ‹strict_mono Nf› by (simp add: filterlim_subseq)
then have "eventually (λl. prev_N l > 1) sequentially"
by (simp add: filterlim_iff)
then have "eventually (λl. delta l = eps(prev_N l)) sequentially"
unfolding delta_def by (simp add: eventually_mono)
moreover have "(λl. eps(prev_N l)) ⇢ 0"
by (rule filterlim_compose[OF ‹eps ⇢ 0› ‹LIM n sequentially. prev_N n :> at_top›])
ultimately have "delta ⇢ 0" by (simp add: filterlim_cong)
have "delta n ≤ K" for n
proof -
have *: "d2 * (1 / 2) ^ prev_N n ≤ real K * 1"
apply (rule mult_mono') using ‹K ≥ max c0 d2› ‹d2>0› by (auto simp add: power_le_one less_imp_le)
then show ?thesis unfolding delta_def apply auto unfolding eps_def using * by auto
qed
define bad_times where "bad_times = (λx. {n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∪
(⋃N∈{2..}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)}))"
have card_bad_times: "card (bad_times x ∩ {..<B}) ≤ d2 * B" if "x ∈ Og" for x B
proof -
have "(∑N∈{..<B}. (1/(2::real))^N) ≤ (∑N. (1/2)^N)"
by (rule sum_le_suminf, auto simp add: summable_geometric)
also have "... = 2" using suminf_geometric[of "1/(2::real)"] by auto
finally have *: "(∑N∈{..<B}. (1/(2::real))^N) ≤ 2" by simp
have "(∑ N ∈ {2..<B}. eps N * B) ≤ (∑ N ∈ {2..<B+2}. eps N * B)"
by (rule sum_mono2, auto)
also have "... = (∑N∈{2..<B+2}. d2 * (1/2)^N * B)"
unfolding eps_def by auto
also have "... = (∑N∈{..<B}. d2 * (1/2)^(N+2) * B)"
by (rule sum.reindex_bij_betw[symmetric],rule bij_betw_byWitness[where ?f' = "λi. i-2"], auto)
also have "... = (∑N∈{..<B}. (d2 * (1/4) * B) * (1/2)^N)"
by (auto, metis (lifting) mult.commute mult.left_commute)
also have "... = (d2 * (1/4) * B) * (∑N∈{..<B}. (1/2)^N)"
by (rule sum_distrib_left[symmetric])
also have "... ≤ (d2 * (1/4) * B) * 2"
apply (rule mult_left_mono) using * ‹d2 > 0› apply auto
by (metis ‹0 < d2› mult_eq_0_iff mult_le_0_iff not_le of_nat_eq_0_iff of_nat_le_0_iff)
finally have I: "(∑ N ∈ {2..<B}. eps N * B) ≤ d2/2 * B"
by auto
have "x ∈ On 1" using ‹x ∈ Og› unfolding Og_def Ogood_def by auto
then have "x ∈ O1" unfolding On_def by auto
have B1: "real(card({n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B})) ≤ (d2/2) * B" for B
proof (cases "B ≥ N1")
case True
have "card({n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B})
≤ card({n. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B})"
by (rule card_mono, auto)
also have "... ≤ (d2/2) * B"
using ‹x ∈ O1› unfolding O1_def using True by auto
finally show ?thesis by auto
next
case False
then have "B < Nf 1" unfolding Nf_def by auto
then have "{n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B} = {}"
by auto
then have "card ({n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B}) = 0"
by auto
also have "... ≤ (d2/2) * B"
using ‹¬ d2 < 0› by simp
finally show ?thesis by simp
qed
have BN: "real(card ({n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})) ≤ eps N * B" if "N ≥ 2" for N B
proof -
have "x ∈ On ((N-1) + 1)" using ‹x ∈ Og› unfolding Og_def Ogood_def by auto
then have "x ∈ On N" using ‹N≥2› by auto
show ?thesis
proof (cases "B ≥ Nf N")
case True
have "card ({n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B}) ≤
card ({n. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})"
by (rule card_mono, auto)
also have "... ≤ eps N * B"
using ‹x ∈ On N› ‹N≥2› True unfolding On_def by auto
finally show ?thesis by simp
next
case False
then have "{n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B} = {}"
by auto
then have "card ({n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B}) = 0"
by auto
also have "... ≤ eps N * B"
by (metis ‹⋀n. 0 < eps n› le_less mult_eq_0_iff mult_pos_pos of_nat_0 of_nat_0_le_iff)
finally show ?thesis by simp
qed
qed
{
fix N assume "N ≥ B"
have "Nf N ≥ B" using seq_suble[OF ‹strict_mono Nf›, of N] ‹N ≥ B› by simp
then have "{Nf N..} ∩ {..<B} = {}" by auto
then have "{n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B} = {}" by auto
}
then have *: "(⋃N∈{B..}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B}) = {}"
by auto
have "{2..} ⊆ {2..<B} ∪ {B..}" by auto
then have "(⋃N∈{2..}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})
⊆ (⋃N∈{2..<B}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})
∪ (⋃N∈{B..}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})"
by auto
also have "... = (⋃N∈{2..<B}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})"
using * by auto
finally have *: "bad_times x ∩ {..<B} ⊆ {n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B}
∪ (⋃N∈{2..<B}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})"
unfolding bad_times_def by auto
have "card(bad_times x ∩ {..<B}) ≤ card({n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B}
∪ (⋃N∈{2..<B}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B}))"
by (rule card_mono[OF _ *], auto)
also have "... ≤ card({n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B}) +
card (⋃N∈{2..<B}. {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})"
by (rule card_Un_le)
also have "... ≤ card({n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B}) +
(∑ N∈{2..<B}. card ({n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B}))"
by (simp del: UN_simps, rule card_UN_le, auto)
finally have "real (card(bad_times x ∩ {..<B})) ≤
real(card({n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B})
+ (∑ N∈{2..<B}. card ({n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})))"
by (subst of_nat_le_iff, simp)
also have "... = real(card({n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)} ∩ {..<B}))
+ (∑ N∈{2..<B}. real(card ({n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})))"
by auto
also have "... ≤ (d2/2 * B) + (∑ N∈{2..<B}. real(card ({n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)} ∩ {..<B})))"
using B1 by simp
also have "... ≤ (d2/2 * B) + (∑ N ∈ {2..<B}. eps N * B)"
apply (simp, rule sum_mono) using BN by auto
also have "... ≤ (d2/2 * B) + (d2/2*B)"
using I by auto
finally show ?thesis by simp
qed
have ineq_on_Og: "u n x - u (n-l) x > - delta l * l" if "l ∈ {1..n}" "n ∉ bad_times x" "x ∈ Og" for n x l
proof -
consider "n < Nf 1" | "n ≥ Nf 1 ∧ prev_N l ≤ 1" | "n ≥ Nf 1 ∧ prev_N l ≥ 2" by linarith
then show ?thesis
proof (cases)
assume "n < Nf 1"
then have "{N. Nf N ≤ n} = {0}"
apply auto using ‹strict_mono Nf› unfolding strict_mono_def
apply (metis le_trans less_Suc0 less_imp_le_nat linorder_neqE_nat not_less)
unfolding Nf_def by auto
then have "prev_N n = 0" unfolding prev_N_def by auto
moreover have "prev_N l ≤ prev_N n"
unfolding prev_N_def apply (rule Max_mono) using ‹l ∈ {1..n}› fin apply auto
unfolding Nf_def by auto
ultimately have "prev_N l = 0" using ‹prev_N l ≤ prev_N n› by auto
then have "delta l = K" unfolding delta_def by auto
have "1 ∉ {N. Nf N ≤ n}" using fin[of n]
by (metis (full_types) Max_ge ‹prev_N n = 0› fin not_one_le_zero prev_N_def)
then have "n < Nf 1" by auto
moreover have "n ≥ 1" using ‹l ∈ {1..n}› by auto
ultimately have "n ∈ {1..Nf 1}" by auto
then have "u n x - u (n-l) x > - (real K * l)" using ‹x ∈ Og› unfolding Og_def using ‹l ∈ {1..n}› by auto
then show ?thesis using ‹delta l = K› by auto
next
assume H: "n ≥ Nf 1 ∧ prev_N l ≤ 1"
then have "delta l = K" unfolding delta_def by auto
have "n ∉ {n ∈ {Nf 1..}. ∃l∈{1..n}. u n x - u (n-l) x ≤ - (c0 * l)}"
using ‹n ∉ bad_times x› unfolding bad_times_def by auto
then have "u n x - u (n-l) x > - (c0 * l)"
using H ‹l ∈ {1..n}› by force
moreover have "- (c0 * l) ≥ - (real K * l)" using K(1) by (simp add: mult_mono)
ultimately show ?thesis using ‹delta l = K› by auto
next
assume H: "n ≥ Nf 1 ∧ prev_N l ≥ 2"
define N where "N = prev_N l"
have "N ≥ 2" unfolding N_def using H by auto
have "prev_N l ∈ {N. Nf N ≤ l}"
unfolding prev_N_def apply (rule Max_in, auto simp add: fin)
unfolding Nf_def by auto
then have "Nf N ≤ l" unfolding N_def by auto
then have "Nf N ≤ n" using ‹l ∈ {1..n}› by auto
have "n ∉ {n ∈ {Nf N..}. ∃l ∈ {Nf N..n}. u n x - u (n-l) x ≤ - (eps N * l)}"
using ‹n ∉ bad_times x› ‹N≥2› unfolding bad_times_def by auto
then have "u n x - u (n-l) x > - (eps N * l)"
using ‹Nf N ≤ n› ‹Nf N ≤ l› ‹l ∈ {1..n}› by force
moreover have "eps N = delta l" unfolding delta_def N_def using H by auto
ultimately show ?thesis by auto
qed
qed
have "Og ⊆ {x ∈ space M. ∀(B::nat). card {n ∈{..<B}. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - delta l * l} ≤ d * B}"
proof (auto)
fix x assume "x ∈ Og"
then show "x ∈ space M" unfolding Og_def by auto
next
fix x B assume "x ∈ Og"
have *: "{n. n < B ∧ (∃l∈{Suc 0..n}. u n x - u (n - l) x ≤ - (delta l * real l))} ⊆ bad_times x ∩ {..<B}"
using ineq_on_Og ‹x∈Og› by force
have "card {n. n < B ∧ (∃l∈{Suc 0..n}. u n x - u (n - l) x ≤ - (delta l * real l))} ≤ card (bad_times x ∩ {..<B})"
apply (rule card_mono, simp) using * by auto
also have "... ≤ d2 * B" using card_bad_times ‹x ∈ Og› by auto
also have "... ≤ d * B" unfolding d2_def using ‹d>0› by auto
finally show "card {n. n < B ∧ (∃l∈{Suc 0..n}. u n x - u (n - l) x ≤ - (delta l * real l))} ≤ d * B"
by simp
qed
then have "emeasure M Og ≤ emeasure M {x ∈ space M. ∀(B::nat). card {n ∈{..<B}. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - delta l * l} ≤ d * B}"
by (rule emeasure_mono, auto)
then have "emeasure M {x ∈ space M. ∀(B::nat). card {n ∈{..<B}. ∃l ∈ {1..n}. u n x - u (n-l) x ≤ - delta l * l} ≤ d * B} > 1-d"
using ‹emeasure M Og > 1 - d› by auto
then show ?thesis using ‹delta ⇢ 0› ‹∀l. delta l > 0› by auto
qed
text ‹We go back to the natural time direction, by using the previous result for the inverse map
and the inverse subcocycle, and a change of variables argument. The price to pay is that the
estimates we get are weaker: we have a control on a set of upper asymptotic density close to $1$, while
having a set of lower asymptotic density close to $1$ as before would be stronger. This will
nevertheless be sufficient for our purposes below.›
lemma upper_density_good_direction_invertible:
assumes "invertible_qmpt"
"d>(0::real)" "d ≤ 1"
shows "∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
emeasure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} ≥ 1-d} ≥ ennreal(1-d)"
proof -
interpret I: Gouezel_Karlsson_Kingman M Tinv "(λn x. u n ((Tinv^^n) x))"
proof
show "Tinv ∈ quasi_measure_preserving M M"
using Tinv_qmpt[OF ‹invertible_qmpt›] unfolding qmpt_def qmpt_axioms_def by simp
show "Tinv ∈ measure_preserving M M"
using Tinv_mpt[OF ‹invertible_qmpt›] unfolding mpt_def mpt_axioms_def by simp
show "mpt.subcocycle M Tinv (λn x. u n ((Tinv ^^ n) x))"
using subcocycle_u_Tinv[OF subu ‹invertible_qmpt›] by simp
show "- ∞ < subcocycle_avg_ereal (λn x. u n ((Tinv ^^ n) x))"
using subcocycle_avg_ereal_Tinv[OF subu ‹invertible_qmpt›] subu_fin by simp
show "AE x in M. fmpt.subcocycle_lim M Tinv (λn x. u n ((Tinv ^^ n) x)) x = 0"
using subcocycle_lim_Tinv[OF subu ‹invertible_qmpt›] subu_0 by auto
qed
have bij: "bij T" using ‹invertible_qmpt› unfolding invertible_qmpt_def by simp
define e where "e = d * d / 2"
have "e>0" "e≤1" unfolding e_def using ‹d>0› ‹d ≤ 1›
by (auto, meson less_imp_le mult_left_le one_le_numeral order_trans)
obtain delta::"nat ⇒ real" where d: "⋀l. delta l > 0"
"delta ⇢ 0"
"emeasure M {x ∈ space M. ∀N.
card {n ∈ {..<N}. ∃l∈{1..n}. u n ((Tinv ^^ n) x) - u (n - l) ((Tinv ^^ (n - l)) x) ≤ - delta l * real l} ≤ e * real N}
> 1-e"
using I.upper_density_delta[OF ‹e>0› ‹e≤1›] by blast
define S where "S = {x ∈ space M. ∀N.
card {n ∈ {..<N}. ∃l∈{1..n}. u n ((Tinv ^^ n) x) - u (n - l) ((Tinv ^^ (n - l)) x) ≤ - delta l * real l} ≤ e * real N}"
have [measurable]: "S ∈ sets M" unfolding S_def by auto
have "emeasure M S > 1 - e" unfolding S_def using d(3) by simp
define Og where "Og = (λn. {x ∈ space M. ∀l∈{1..n}. u n ((Tinv ^^ n) x) - u (n - l) ((Tinv ^^ (n - l)) x) > - delta l * real l})"
have [measurable]: "Og n ∈ sets M" for n unfolding Og_def by auto
define Pg where "Pg = (λn. {x ∈ space M. ∀l∈{1..n}. u n x - u (n - l) ((T^^l) x) > - delta l * real l})"
have [measurable]: "Pg n ∈ sets M" for n unfolding Pg_def by auto
define Bad where "Bad = (λi::nat. {x ∈ space M. ∀N≥i. card {n ∈ {..<N}. x ∈ Pg n} ≤ (1-d) * real N})"
have [measurable]: "Bad i ∈ sets M" for i unfolding Bad_def by auto
then have "range Bad ⊆ sets M" by auto
have "incseq Bad"
unfolding Bad_def incseq_def by auto
have inc: "{x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} < 1-d}
⊆ (⋃i. Bad i)"
proof
fix x assume H: "x ∈ {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} < 1-d}"
then have "x ∈ space M" by simp
define A where "A = {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l}"
have "upper_asymptotic_density A < 1-d" using H unfolding A_def by simp
then have "∃i. ∀N≥i. card (A ∩ {..<N}) ≤ (1-d)* real N"
using upper_asymptotic_densityD[of A "1-d"] by (metis (no_types, lifting) eventually_sequentially less_imp_le)
then obtain i where "card (A ∩ {..<N}) ≤ (1-d)* real N" if "N≥i" for N by blast
moreover have "A ∩ {..<N} = {n. n<N ∧ (∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l)}" for N
unfolding A_def by auto
ultimately have "x ∈ Bad i" unfolding Bad_def Pg_def using ‹x ∈ space M›
by auto
then show "x ∈ (⋃i. Bad i)" by blast
qed
have "emeasure M (Og n) ≤ emeasure M (Pg n)" for n
proof -
have *: "(T^^n)-`(Og n) ∩ space M ⊆ Pg n" for n
proof
fix x assume x: "x ∈ (T^^n)-`(Og n) ∩ space M"
define y where "y = (T^^n) x"
then have "y ∈ Og n" using x by auto
have "y ∈ space M" using sets.sets_into_space[OF ‹Og n ∈ sets M›] ‹y ∈ Og n› by auto
have "x = (Tinv^^n) y"
unfolding y_def Tinv_def using inv_fn_o_fn_is_id[OF bij, of n] by (metis comp_apply)
{
fix l assume "l ∈ {1..n}"
have "(T^^l) x = (T^^l) ((Tinv^^l) ((Tinv^^(n-l))y))"
apply (subst ‹x = (Tinv^^n) y›) using funpow_add[of l "n-l" Tinv] ‹l ∈ {1..n}› by fastforce
then have *: "(T^^l) x = (Tinv^^(n-l)) y"
unfolding Tinv_def using fn_o_inv_fn_is_id[OF bij] by (metis comp_apply)
then have "u n x - u (n-l) ((T^^l) x) = u n ((Tinv^^n) y) - u (n-l) ((Tinv^^(n-l)) y)"
using ‹x = (Tinv^^n) y› by auto
also have "... > - delta l * real l"
using ‹y ∈ Og n› ‹l ∈ {1..n}› unfolding Og_def by auto
finally have "u n x - u (n-l) ((T^^l) x) > - delta l * real l" by simp
}
then show "x ∈ Pg n"
unfolding Pg_def using x by auto
qed
have "emeasure M (Og n) = emeasure M ((T^^n)-`(Og n) ∩ space M)"
using T_vrestr_same_emeasure(2) unfolding vimage_restr_def by auto
also have "... ≤ emeasure M (Pg n)"
apply (rule emeasure_mono) using * by auto
finally show ?thesis by simp
qed
{
fix N::nat assume "N ≥ 1"
have I: "card {n∈{..<N}. x ∈ Og n} ≥ (1-e) * real N" if "x ∈ S" for x
proof -
have "x ∈ space M" using ‹x ∈ S› sets.sets_into_space[OF ‹S ∈ sets M›] by auto
have a: "real (card {n. n < N ∧ (∃l∈{Suc 0..n}. u n ((Tinv ^^ n) x) - u (n - l) ((Tinv ^^ (n - l)) x) ≤ - (delta l * real l))}) ≤ e * real N"
using ‹x ∈ S› unfolding S_def by auto
have *: "{n. n < N} = {n. n < N ∧ (∃l∈{Suc 0..n}. u n ((Tinv ^^ n) x) - u (n - l) ((Tinv ^^ (n - l)) x) ≤ - (delta l * real l))}
∪ {n. n < N ∧ x ∈ Og n}" unfolding Og_def using ‹x ∈ space M›
by (auto, meson atLeastAtMost_iff linorder_not_le)
have "N = card {n. n < N}" by auto
also have "... = card {n. n < N ∧ (∃l∈{Suc 0..n}. u n ((Tinv ^^ n) x) - u (n - l) ((Tinv ^^ (n - l)) x) ≤ - (delta l * real l))}
+ card {n. n < N ∧ x ∈ Og n}"
apply (subst *, rule card_Un_disjoint) unfolding Og_def by auto
ultimately have "real N ≤ e * real N + card {n. n < N ∧ x ∈ Og n}"
using a by auto
then show ?thesis
by (auto simp add: algebra_simps)
qed
define m where "m = measure M (Bad N)"
have "m ≥ 0" "1-m ≥ 0" unfolding m_def by auto
have *: "1-e ≤ emeasure M S" using ‹emeasure M S > 1 - e› by auto
have "ennreal((1-e) * ((1-e) * real N)) = ennreal(1-e) * ennreal((1-e) * real N)"
apply (rule ennreal_mult) using ‹e ≤ 1› by auto
also have "... ≤ emeasure M S * ennreal((1-e) * real N)"
using mult_right_mono[OF *] by simp
also have "... = (∫⇧+ x∈S. ((1-e) * real N) ∂M)"
by (metis ‹S ∈ events› mult.commute nn_integral_cmult_indicator)
also have "... ≤ (∫⇧+x ∈ S. ennreal(card {n∈{..<N}. x ∈ Og n}) ∂M)"
apply (rule nn_integral_mono) using I unfolding indicator_def by (simp)
also have "... ≤ (∫⇧+x ∈ space M. ennreal(card {n∈{..<N}. x ∈ Og n}) ∂M)"
by (rule nn_set_integral_set_mono, simp only: sets.sets_into_space[OF ‹S ∈ sets M›])
also have "... = (∫⇧+x. ennreal(card {n∈{..<N}. x ∈ Og n}) ∂M)"
by (rule nn_set_integral_space)
also have "... = (∫⇧+x. ennreal (∑n∈{..<N}. ((indicator (Og n) x)::nat)) ∂M)"
apply (rule nn_integral_cong) using sum_indicator_eq_card2[of "{..<N}" Og] by auto
also have "... = (∫⇧+x. (∑n∈{..<N}. indicator (Og n) x) ∂M)"
apply (rule nn_integral_cong, auto, simp only: sum_ennreal[symmetric])
by (metis ennreal_0 ennreal_eq_1 indicator_eq_1_iff indicator_simps(2) real_of_nat_indicator)
also have "... = (∑n ∈{..<N}. (∫⇧+x. (indicator (Og n) x) ∂M))"
by (rule nn_integral_sum, simp)
also have "... = (∑n ∈{..<N}. emeasure M (Og n))"
by simp
also have "... ≤ (∑n ∈{..<N}. emeasure M (Pg n))"
apply (rule sum_mono) using ‹⋀n. emeasure M (Og n) ≤ emeasure M (Pg n)› by simp
also have "... = (∑n ∈{..<N}. (∫⇧+x. (indicator (Pg n) x) ∂M))"
by simp
also have "... = (∫⇧+x. (∑n∈{..<N}. indicator (Pg n) x) ∂M)"
by (rule nn_integral_sum[symmetric], simp)
also have "... = (∫⇧+x. ennreal (∑n∈{..<N}. ((indicator (Pg n) x)::nat)) ∂M)"
apply (rule nn_integral_cong, auto, simp only: sum_ennreal[symmetric])
by (metis ennreal_0 ennreal_eq_1 indicator_eq_1_iff indicator_simps(2) real_of_nat_indicator)
also have "... = (∫⇧+x. ennreal(card {n∈{..<N}. x ∈ Pg n}) ∂M)"
apply (rule nn_integral_cong) using sum_indicator_eq_card2[of "{..<N}" Pg] by auto
also have "... = (∫⇧+x ∈ space M. ennreal(card {n∈{..<N}. x ∈ Pg n}) ∂M)"
by (rule nn_set_integral_space[symmetric])
also have "... = (∫⇧+x ∈ Bad N ∪ (space M - Bad N). ennreal(card {n∈{..<N}. x ∈ Pg n}) ∂M)"
apply (rule nn_integral_cong) unfolding indicator_def by auto
also have "... = (∫⇧+x ∈ Bad N. ennreal(card {n∈{..<N}. x ∈ Pg n}) ∂M)
+ (∫⇧+x ∈ space M - Bad N. ennreal(card {n∈{..<N}. x ∈ Pg n}) ∂M)"
by (rule nn_integral_disjoint_pair, auto)
also have "... ≤ (∫⇧+x ∈ Bad N. ennreal((1-d) * real N) ∂M) + (∫⇧+x ∈ space M - Bad N. ennreal(real N) ∂M)"
apply (rule add_mono)
apply (rule nn_integral_mono, simp add: Bad_def indicator_def, auto)
apply (rule nn_integral_mono, simp add: indicator_def, auto)
using card_Collect_less_nat[of N] card_mono[of "{n. n < N}"] by (simp add: Collect_mono_iff)
also have "... = ennreal((1-d) * real N) * emeasure M (Bad N) + ennreal(real N) * emeasure M (space M - Bad N)"
by (simp add: nn_integral_cmult_indicator)
also have "... = ennreal((1-d) * real N) * ennreal(m) + ennreal(real N) * ennreal(1-m)"
unfolding m_def by (simp add: emeasure_eq_measure prob_compl)
also have "... = ennreal((1-d) * real N * m + real N * (1-m))"
using ‹m ≥ 0› ‹1-m ≥ 0› ‹d ≤ 1› ennreal_plus ennreal_mult by auto
finally have "ennreal((1-e) * ((1-e) * real N)) ≤ ennreal((1-d) * real N * m + real N * (1-m))"
by simp
moreover have "(1-d) * real N * m + real N * (1-m) ≥ 0"
using ‹m ≥ 0› ‹1-m ≥ 0› ‹d ≤ 1› by auto
ultimately have "(1-e) * ((1-e) * real N) ≤ (1-d) * real N * m + real N * (1-m)"
using ennreal_le_iff by auto
then have "0 ≤ (e * 2 - d * m - e * e) * real N"
by (auto simp add: algebra_simps)
then have "0 ≤ e * 2 - d * m - e * e"
using ‹N ≥ 1› by (simp add: zero_le_mult_iff)
also have "... ≤ e * 2 - d * m"
using ‹e > 0› by auto
finally have "m ≤ e * 2 / d"
using ‹d>0› by (auto simp add: algebra_simps divide_simps)
then have "m ≤ d"
unfolding e_def using ‹d>0› by (auto simp add: divide_simps)
then have "emeasure M (Bad N) ≤ d"
unfolding m_def by (simp add: emeasure_eq_measure ennreal_leI)
}
then have "emeasure M (⋃i. Bad i) ≤ d"
using LIMSEQ_le_const2[OF Lim_emeasure_incseq[OF ‹range Bad ⊆ sets M› ‹incseq Bad›]] by auto
then have "emeasure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} < 1-d} ≤ d"
using emeasure_mono[OF inc, of M] by auto
then have *: "measure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} < 1-d} ≤ d"
using emeasure_eq_measure ‹d>0› by fastforce
have "{x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} ≥ 1-d}
= space M - {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} < 1-d}"
by auto
then have "measure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} ≥ 1-d}
= measure M (space M - {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} < 1-d})"
by simp
also have "... = measure M (space M)
- measure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} < 1-d}"
by (rule measure_Diff, auto)
also have "... ≥ 1 - d"
using * prob_space by linarith
finally have "emeasure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} ≥ 1-d} ≥ 1 - d"
using emeasure_eq_measure by auto
then show ?thesis using d(1) d(2) by blast
qed
text ‹Now, we want to remove the invertibility assumption in the previous lemma. The idea is to
go to the natural extension of the system, use the result there and project it back.
However, if the system is not defined on a polish space, there is no reason why it should have
a natural extension, so we have first to project the original system on a polish space on which
the subcocycle is defined. This system is obtained by considering the joint distribution of the
subcocycle and all its iterates (this is indeed a polish system, as a space of functions from
$\mathbb{N}^2$ to $\mathbb{R}$).›
lemma upper_density_good_direction:
assumes "d>(0::real)" "d ≤ 1"
shows "∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
emeasure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l} ≥ 1-d} ≥ ennreal(1-d)"
proof -
define U where "U = (λx. (λn. u n x))"
define projJ where "projJ = (λx. (λn. U ((T^^n)x)))"
define MJ where "MJ = (distr M borel (λx. (λn. U ((T^^n)x))))"
define TJ::"(nat ⇒ nat ⇒ real) ⇒ (nat ⇒ nat ⇒ real)" where "TJ = nat_left_shift"
have *: "mpt_factor projJ MJ TJ"
unfolding projJ_def MJ_def TJ_def apply (rule fmpt_factor_projection)
unfolding U_def by (rule measurable_coordinatewise_then_product, simp)
interpret J: polish_pmpt MJ TJ
unfolding projJ_def polish_pmpt_def apply (auto)
apply (rule pmpt_factor) using * apply simp
unfolding polish_pmpt_axioms_def MJ_def by auto
have [simp]: "projJ ∈ measure_preserving M MJ" using mpt_factorE(1)[OF *] by simp
then have [measurable]: "projJ ∈ measurable M MJ" by (simp add: measure_preservingE(1))
text ‹We define a subcocycle $uJ$ in the projection corresponding to the original
subcocycle $u$ above. (With the natural definition, it is only a subcocycle almost
everywhere.) We check that it shares most properties of $u$.›
define uJ::"nat ⇒ (nat ⇒ nat ⇒ real) ⇒ real" where "uJ = (λn x. x 0 n)"
have [measurable]: "uJ n ∈ borel_measurable borel" for n
unfolding uJ_def by (metis measurable_product_coordinates measurable_product_then_coordinatewise)
moreover have "measurable borel borel = measurable MJ borel"
apply (rule measurable_cong_sets) unfolding MJ_def by auto
ultimately have [measurable]: "uJ n ∈ borel_measurable MJ" for n by fast
have uJ_proj: "u n x = uJ n (projJ x)" for n x
unfolding uJ_def projJ_def U_def by auto
have uJ_int: "integrable MJ (uJ n)" for n
apply (rule measure_preserving_preserves_integral'(1)[OF ‹projJ ∈ measure_preserving M MJ›])
apply (subst uJ_proj[of n, symmetric]) using int_u[of n] by auto
have uJ_int2: "(∫x. uJ n x ∂MJ) = (∫x. u n x ∂M)" for n
unfolding uJ_proj
apply (rule measure_preserving_preserves_integral'(2)[OF ‹projJ ∈ measure_preserving M MJ›])
apply (subst uJ_proj[of n, symmetric]) using int_u[of n] by auto
have uJ_AE: "AE x in MJ. uJ (n+m) x ≤ uJ n x + uJ m ((TJ^^n) x)" for m n
proof -
have "AE x in M. uJ (n+m) (projJ x) ≤ uJ n (projJ x) + uJ m (projJ ((T^^n) x))"
unfolding uJ_proj[symmetric] using subcocycle_ineq[OF subu] by auto
moreover have "AE x in M. projJ ((T^^n) x) = (TJ^^n) (projJ x)"
using qmpt_factor_iterates[OF mpt_factor_is_qmpt_factor[OF *]] by auto
ultimately have *: "AE x in M. uJ (n+m) (projJ x) ≤ uJ n (projJ x) + uJ m ((TJ^^n) (projJ x))"
by auto
show ?thesis
apply (rule quasi_measure_preserving_AE'[OF measure_preserving_is_quasi_measure_preserving[OF ‹projJ ∈ measure_preserving M MJ›], OF *])
by auto
qed
have uJ_0: "AE x in MJ. (λn. uJ n x / n) ⇢ 0"
proof -
have "AE x in M. (λn. u n x / n) ⇢ subcocycle_lim u x"
by (rule kingman_theorem_nonergodic(1)[OF subu subu_fin])
moreover have "AE x in M. subcocycle_lim u x = 0"
using subu_0 by simp
ultimately have *: "AE x in M. (λn. uJ n (projJ x) / n) ⇢ 0"
unfolding uJ_proj by auto
show ?thesis
apply (rule quasi_measure_preserving_AE'[OF measure_preserving_is_quasi_measure_preserving[OF ‹projJ ∈ measure_preserving M MJ›], OF *])
by auto
qed
text ‹Then, we go to the natural extension of $TJ$, to have an invertible system.›
define MI where "MI = J.natural_extension_measure"
define TI where "TI = J.natural_extension_map"
define projI where "projI = J.natural_extension_proj"
interpret I: pmpt MI TI unfolding MI_def TI_def by (rule J.natural_extension(1))
have "I.mpt_factor projI MJ TJ" unfolding projI_def
using I.mpt_factorE(1) J.natural_extension(3) MI_def TI_def by auto
then have [simp]: "projI ∈ measure_preserving MI MJ" using I.mpt_factorE(1) by auto
then have [measurable]: "projI ∈ measurable MI MJ" by (simp add: measure_preservingE(1))
have "I.invertible_qmpt"
using J.natural_extension(2) MI_def TI_def by auto
text ‹We define a natural subcocycle $uI$ there, and check its properties.›
define uI where uI_proj: "uI = (λn x. uJ n (projI x))"
have [measurable]: "uI n ∈ borel_measurable MI" for n unfolding uI_proj by auto
have uI_int: "integrable MI (uI n)" for n
unfolding uI_proj by (rule measure_preserving_preserves_integral(1)[OF ‹projI ∈ measure_preserving MI MJ› uJ_int])
have "(∫x. uJ n x ∂MJ) = (∫x. uI n x ∂MI)" for n
unfolding uI_proj by (rule measure_preserving_preserves_integral(2)[OF ‹projI ∈ measure_preserving MI MJ› uJ_int])
then have uI_int2: "(∫x. uI n x ∂MI) = (∫x. u n x ∂M)" for n
using uJ_int2 by simp
have uI_AE: "AE x in MI. uI (n+m) x ≤ uI n x + uI m (((TI)^^n) x)" for m n
proof -
have "AE x in MI. uJ (n+m) (projI x) ≤ uJ n (projI x) + uJ m (((TJ)^^n) (projI x))"
apply (rule quasi_measure_preserving_AE[OF measure_preserving_is_quasi_measure_preserving[OF ‹projI ∈ measure_preserving MI MJ›]])
using uJ_AE by auto
moreover have "AE x in MI. ((TJ)^^n) (projI x) = projI (((TI)^^n) x)"
using I.qmpt_factor_iterates[OF I.mpt_factor_is_qmpt_factor[OF ‹I.mpt_factor projI MJ TJ›]]
by auto
ultimately show ?thesis unfolding uI_proj by auto
qed
have uI_0: "AE x in MI. (λn. uI n x / n) ⇢ 0"
unfolding uI_proj
apply (rule quasi_measure_preserving_AE[OF measure_preserving_is_quasi_measure_preserving[OF ‹projI ∈ measure_preserving MI MJ›]])
using uJ_0 by simp
text ‹As $uI$ is only a subcocycle almost everywhere, we correct it to get a genuine subcocycle,
to which we will apply Lemma \verb+upper_density_good_direction_invertible+.›
obtain vI where H: "I.subcocycle vI" "AE x in MI. ∀n. vI n x = uI n x"
using I.subcocycle_AE[OF uI_AE uI_int] by blast
have [measurable]: "⋀n. vI n ∈ borel_measurable MI" "⋀n. integrable MI (vI n)"
using I.subcocycle_integrable[OF H(1)] by auto
have "(∫x. vI n x ∂MI) = (∫x. uI n x ∂MI)" for n
apply (rule integral_cong_AE) using H(2) by auto
then have "(∫x. vI n x ∂MI) = (∫x. u n x ∂M)" for n
using uI_int2 by simp
then have "I.subcocycle_avg_ereal vI = subcocycle_avg_ereal u"
unfolding I.subcocycle_avg_ereal_def subcocycle_avg_ereal_def by auto
then have vI_fin: "I.subcocycle_avg_ereal vI > -∞" using subu_fin by simp
have "AE x in MI. (λn. vI n x / n) ⇢ 0"
using uI_0 H(2) by auto
moreover have "AE x in MI. (λn. vI n x / n) ⇢ I.subcocycle_lim vI x"
by (rule I.kingman_theorem_nonergodic(1)[OF H(1) vI_fin])
ultimately have vI_0: "AE x in MI. I.subcocycle_lim vI x = 0"
using LIMSEQ_unique by auto
interpret GKK: Gouezel_Karlsson_Kingman MI TI vI
apply standard
using H(1) vI_fin vI_0 by auto
obtain delta where delta: "⋀l. delta l > 0" "delta ⇢ 0"
"emeasure MI {x ∈ space MI. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < vI n x - vI (n - l) ((TI ^^ l) x)} ≥ 1 - d } ≥ 1 - d"
using GKK.upper_density_good_direction_invertible[OF ‹I.invertible_qmpt› ‹d>0› ‹d≤1›] by blast
text ‹Then, we need to go back to the original system, showing that the estimates for $TI$ carry
over. First, we go to $TJ$.›
have BJ: "emeasure MJ {x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d } ≥ 1 - d"
proof -
have *: "AE x in MI. uJ n (projI x) = vI n x" for n
using uI_proj H(2) by auto
have **: "AE x in MI. ∀n. uJ n (projI x) = vI n x"
by (subst AE_all_countable, auto intro: *)
have "AE x in MI. ∀m n. uJ n (projI ((TI^^m) x)) = vI n ((TI^^m) x)"
by (rule I.T_AE_iterates[OF **])
then have "AE x in MI. (∀m n. uJ n (projI ((TI^^m) x)) = vI n ((TI^^m) x)) ∧ (∀n. projI ((TI^^n) x) = (TJ^^n) (projI x))"
using I.qmpt_factor_iterates[OF I.mpt_factor_is_qmpt_factor[OF ‹I.mpt_factor projI MJ TJ›]] by auto
then obtain ZI where ZI: "⋀x. x ∈ space MI - ZI ⟹ (∀m n. uJ n (projI ((TI^^m) x)) = vI n ((TI^^m) x)) ∧ (∀n. projI ((TI^^n) x) = (TJ^^n) (projI x))"
"ZI ∈ null_sets MI"
using AE_E3 by blast
have *: "uJ n (projI x) - uJ (n - l) ((TJ ^^ l) (projI x)) = vI n x - vI (n - l) ((TI ^^ l) x)" if "x ∈ space MI - ZI" for x n l
proof -
have "(TI^^0) x = x" "(TJ^^0) (projI x) = (projI x)" by auto
then show ?thesis using ZI(1)[OF that] by metis
qed
have "projI-`{x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d} ∩ space MI - ZI
= {x ∈ space MI - ZI. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n (projI x) - uJ (n - l) ((TJ ^^ l) (projI x))} ≥ 1 - d}"
by (auto simp add: measurable_space[OF ‹projI ∈ measurable MI MJ›])
also have "... = {x ∈ space MI - ZI. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < vI n x - vI (n - l) ((TI ^^ l) x)} ≥ 1 - d}"
using * by auto
also have "... = {x ∈ space MI. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < vI n x - vI (n - l) ((TI ^^ l) x)} ≥ 1 - d} - ZI"
by auto
finally have *: "projI-`{x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d} ∩ space MI - ZI
= {x ∈ space MI. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < vI n x - vI (n - l) ((TI ^^ l) x)} ≥ 1 - d} - ZI"
by simp
have "emeasure MJ {x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d}
= emeasure MI (projI-`{x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d} ∩ space MI)"
by (rule measure_preservingE(2)[symmetric], auto)
also have "... = emeasure MI ((projI-`{x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d} ∩ space MI) - ZI)"
by (rule emeasure_Diff_null_set[OF ‹ZI ∈ null_sets MI›, symmetric], measurable)
also have "... = emeasure MI ({x ∈ space MI. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < vI n x - vI (n - l) ((TI ^^ l) x)} ≥ 1 - d} - ZI)"
using * by simp
also have "... = emeasure MI {x ∈ space MI. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < vI n x - vI (n - l) ((TI ^^ l) x)} ≥ 1 - d}"
by (rule emeasure_Diff_null_set[OF ‹ZI ∈ null_sets MI›], measurable)
also have "... ≥ 1-d"
using delta(3) by simp
finally show ?thesis by simp
qed
text ‹Then, we go back to $T$ with virtually the same argument.›
have "emeasure M {x ∈ space M. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < u n x - u (n - l) ((T ^^ l) x)} ≥ 1 - d } ≥ 1 - d"
proof -
obtain Z where Z: "⋀x. x ∈ space M - Z ⟹ (∀n. projJ ((T^^n) x) = (TJ^^n) (projJ x))"
"Z ∈ null_sets M"
using AE_E3[OF qmpt_factor_iterates[OF mpt_factor_is_qmpt_factor[OF ‹mpt_factor projJ MJ TJ›]]] by blast
have *: "uJ n (projJ x) - uJ (n - l) ((TJ ^^ l) (projJ x)) = u n x - u (n - l) ((T^^ l) x)" if "x ∈ space M - Z" for x n l
proof -
have "(T^^0) x = x" "(TJ^^0) (projJ x) = (projJ x)" by auto
then show ?thesis using Z(1)[OF that] uJ_proj by metis
qed
have "projJ-`{x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d} ∩ space M - Z
= {x ∈ space M - Z. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n (projJ x) - uJ (n - l) ((TJ ^^ l) (projJ x))} ≥ 1 - d}"
by (auto simp add: measurable_space[OF ‹projJ ∈ measurable M MJ›])
also have "... = {x ∈ space M - Z. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < u n x - u (n - l) ((T ^^ l) x)} ≥ 1 - d}"
using * by auto
also have "... = {x ∈ space M. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < u n x - u (n - l) ((T ^^ l) x)} ≥ 1 - d} - Z"
by auto
finally have *: "projJ-`{x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d} ∩ space M - Z
= {x ∈ space M. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < u n x - u (n - l) ((T ^^ l) x)} ≥ 1 - d} - Z"
by simp
have "emeasure MJ {x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d}
= emeasure M (projJ-`{x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d} ∩ space M)"
by (rule measure_preservingE(2)[symmetric], auto)
also have "... = emeasure M ((projJ-`{x ∈ space MJ. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < uJ n x - uJ (n - l) ((TJ ^^ l) x)} ≥ 1 - d} ∩ space M) - Z)"
by (rule emeasure_Diff_null_set[OF ‹Z ∈ null_sets M›, symmetric], measurable)
also have "... = emeasure M ({x ∈ space M. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < u n x - u (n - l) ((T ^^ l) x)} ≥ 1 - d} - Z)"
using * by simp
also have "... = emeasure M {x ∈ space M. upper_asymptotic_density {n. ∀l∈{1..n}. - delta l * real l < u n x - u (n - l) ((T ^^ l) x)} ≥ 1 - d}"
by (rule emeasure_Diff_null_set[OF ‹Z ∈ null_sets M›], measurable)
finally show ?thesis using BJ by simp
qed
then show ?thesis using delta(1) delta(2) by auto
qed
text ‹From the quantitative lemma above, we deduce the qualitative statement we are after,
still in the setting of the locale.›
lemma infinite_AE:
shows "AE x in M. ∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l})"
proof -
have "∃deltaf::real ⇒ nat ⇒ real. ∀d. ((d > 0 ∧ d ≤ 1) ⟶ ((∀l. deltaf d l > 0) ∧ (deltaf d ⇢ 0) ∧
emeasure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - (deltaf d l) * l} ≥ 1-d} ≥ ennreal(1-d)))"
apply (subst choice_iff'[symmetric]) using upper_density_good_direction by auto
then obtain deltaf::"real ⇒ nat ⇒ real" where H: "⋀d. d > 0 ∧ d ≤1 ⟹ (∀l. deltaf d l > 0) ∧ (deltaf d ⇢ 0) ∧
emeasure M {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - (deltaf d l) * l} ≥ 1-d} ≥ ennreal(1-d)"
by blast
define U where "U = (λd. {x ∈ space M. upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - (deltaf d l) * l} ≥ 1-d})"
have [measurable]: "U d ∈ sets M" for d
unfolding U_def by auto
have *: "emeasure M (U d) ≥ 1 - d" if "d>0 ∧ d≤ 1" for d
unfolding U_def using H that by auto
define V where "V = (⋃n::nat. U (1/(n+2)))"
have [measurable]: "V ∈ sets M"
unfolding V_def by auto
have a: "emeasure M V ≥ 1 - 1 / (n + 2)" for n::nat
proof -
have "1 - 1 / (n + 2) = 1 - 1 / (real n + 2)"
by auto
also have "... ≤ emeasure M (U (1/(real n+2)))"
using *[of "1 / (real n + 2)"] by auto
also have "... ≤ emeasure M V"
apply (rule Measure_Space.emeasure_mono) unfolding V_def by auto
finally show ?thesis by simp
qed
have b: "(λn::nat. 1 - 1 / (n + 2)) ⇢ ennreal(1 - 0)"
by (intro tendsto_intros LIMSEQ_ignore_initial_segment)
have "emeasure M V ≥ 1 - 0"
apply (rule Lim_bounded) using a b by auto
then have "emeasure M V = 1"
by (simp add: emeasure_ge_1_iff)
then have "AE x in M. x ∈ V"
by (simp add: emeasure_eq_measure prob_eq_1)
moreover
{
fix x assume "x ∈ V"
then obtain n::nat where "x ∈ U (1/(real n+2))" unfolding V_def by blast
define d where "d = 1/(real n + 2)"
have "0 < d" "d≤1" unfolding d_def by auto
have "0 < 1-d" unfolding d_def by auto
also have "... ≤ upper_asymptotic_density {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - (deltaf d l) * l}"
using ‹x ∈ U (1/(real n+2))› unfolding U_def d_def by auto
finally have "infinite {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - (deltaf d l) * l}"
using upper_asymptotic_density_finite by force
then have "∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) > - delta l * l})"
using H ‹0 < d› ‹d≤1› by auto
}
ultimately show ?thesis by auto
qed
end
text ‹Finally, we obtain the full statement, by reducing to the previous situation where the
asymptotic average vanishes.›
theorem (in pmpt) Gouezel_Karlsson_Kingman:
assumes "subcocycle u" "subcocycle_avg_ereal u > -∞"
shows "AE x in M. ∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x > - delta l * l})"
proof -
have [measurable]: "integrable M (u n)" "u n ∈ borel_measurable M" for n
using subcocycle_integrable[OF assms(1)] by auto
define v where "v = birkhoff_sum (λx. -subcocycle_lim u x)"
have int [measurable]: "integrable M (λx. -subcocycle_lim u x)"
using kingman_theorem_nonergodic(2)[OF assms] by auto
have "subcocycle v" unfolding v_def
apply (rule subcocycle_birkhoff)
using assms ‹integrable M (λx. -subcocycle_lim u x)› unfolding subcocycle_def by auto
have "subcocycle_avg_ereal v > - ∞"
unfolding v_def using subcocycle_avg_ereal_birkhoff[OF int] kingman_theorem_nonergodic(2)[OF assms] by auto
have "AE x in M. subcocycle_lim v x = real_cond_exp M Invariants (λx. -subcocycle_lim u x) x"
unfolding v_def by (rule subcocycle_lim_birkhoff[OF int])
moreover have "AE x in M. real_cond_exp M Invariants (λx. - subcocycle_lim u x) x = - subcocycle_lim u x"
by (rule real_cond_exp_F_meas[OF int], auto)
ultimately have AEv: "AE x in M. subcocycle_lim v x = - subcocycle_lim u x"
by auto
define w where "w = (λn x. u n x + v n x)"
have a: "subcocycle w"
unfolding w_def by (rule subcocycle_add[OF assms(1) ‹subcocycle v›])
have b: "subcocycle_avg_ereal w > -∞"
unfolding w_def by (rule subcocycle_avg_add(1)[OF assms(1) ‹subcocycle v› assms(2) ‹subcocycle_avg_ereal v > - ∞›])
have "AE x in M. subcocycle_lim w x = subcocycle_lim u x + subcocycle_lim v x"
unfolding w_def by (rule subcocycle_lim_add[OF assms(1) ‹subcocycle v› assms(2) ‹subcocycle_avg_ereal v > - ∞›])
then have c: "AE x in M. subcocycle_lim w x = 0"
using AEv by auto
interpret Gouezel_Karlsson_Kingman M T w
apply standard using a b c by auto
have "AE x in M. ∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. w n x - w (n-l) ((T^^l) x) > - delta l * l})"
using infinite_AE by auto
moreover
{
fix x assume H: "∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. w n x - w (n-l) ((T^^l) x) > - delta l * l})"
"x ∈ space M"
have *: "v n x = - n * subcocycle_lim u x" for n
unfolding v_def using birkhoff_sum_of_invariants[OF _ ‹x ∈ space M›] by auto
have **: "v n ((T^^l) x) = - n * subcocycle_lim u x" for n l
proof -
have "v n ((T^^l) x) = - n * subcocycle_lim u ((T^^l) x)"
unfolding v_def using birkhoff_sum_of_invariants[OF _ T_spaceM_stable(2)[OF ‹x ∈ space M›]] by auto
also have "... = - n * subcocycle_lim u x"
using Invariants_func_is_invariant_n[OF subcocycle_lim_meas_Inv(2) ‹x ∈ space M›] by auto
finally show ?thesis by simp
qed
have "w n x - w (n-l) ((T^^l) x) = u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x" if "l ∈ {1..n}" for n l
unfolding w_def using *[of n] **[of "n-l" l] that apply (auto simp add: algebra_simps)
by (metis comm_semiring_class.distrib diff_add_inverse nat_le_iff_add of_nat_add)
then have "∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x > - delta l * l})"
using H(1) by auto
}
ultimately show ?thesis by auto
qed
text ‹The previous theorem only contains a lower bound. The corresponding upper bound follows
readily from Kingman's theorem. The next statement combines both upper and lower bounds.›
theorem (in pmpt) Gouezel_Karlsson_Kingman':
assumes "subcocycle u" "subcocycle_avg_ereal u > -∞"
shows "AE x in M. ∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. abs(u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x) < delta l * l})"
proof -
{
fix x assume x: "∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x > - delta l * l})"
"(λl. u l x/l) ⇢ subcocycle_lim u x"
then obtain alpha::"nat ⇒ real" where a: "⋀l. alpha l > 0" "alpha ⇢ 0"
"infinite {n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x > - alpha l * l}"
by auto
define delta::"nat ⇒ real" where "delta = (λl. alpha l + norm(u l x / l - subcocycle_lim u x))"
{
fix n assume *: "∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x > - alpha l * l"
have H: "x > -a ⟹ x < a ⟹ abs x < a" for a x::real by simp
have "abs(u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x) < delta l * l" if "l∈{1..n}" for l
proof (rule H)
have "u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x ≤ u l x - l * subcocycle_lim u x"
using assms(1) subcocycle_ineq[OF assms(1), of l "n-l" x] that by auto
also have "... ≤ l * norm(u l x/l - subcocycle_lim u x)"
using that by (auto simp add: algebra_simps divide_simps)
also have "... < delta l * l"
unfolding delta_def using a(1)[of l] that by auto
finally show "u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x < delta l * l" by simp
have "- (delta l * l) ≤ -alpha l * l"
unfolding delta_def by (auto simp add: algebra_simps)
also have "... < u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x"
using * that by auto
finally show "u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x > -(delta l * l)"
by simp
qed
then have "∀l ∈ {1..n}. abs(u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x) < delta l * l"
by auto
}
then have "{n. ∀l ∈ {1..n}. u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x > - alpha l * l}
⊆ {n. ∀l ∈ {1..n}. abs(u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x) < delta l * l}"
by auto
then have "infinite {n. ∀l ∈ {1..n}. abs(u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x) < delta l * l}"
using a(3) finite_subset by blast
moreover have "delta ⇢ 0 + 0"
unfolding delta_def using x(2) by (intro tendsto_intros a(2) tendsto_norm_zero LIM_zero)
moreover have "delta l > 0" for l unfolding delta_def using a(1)[of l] by auto
ultimately have "∃delta::nat⇒real. (∀l. delta l > 0) ∧ (delta ⇢ 0) ∧
(infinite {n. ∀l ∈ {1..n}. abs(u n x - u (n-l) ((T^^l) x) - l * subcocycle_lim u x) < delta l * l})"
by auto
}
then show ?thesis
using Gouezel_Karlsson_Kingman[OF assms] kingman_theorem_nonergodic(1)[OF assms] by auto
qed
end