(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) 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 real_mult_le_cancel_iff2) 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 (*of Gouezel_Karlsson.thy*)