Theory Gouezel_Karlsson

theory Gouezel_Karlsson
imports Asymptotic_Density Kingman
(*  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*)