Theory Transfer_Operator

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    License: BSD
*)

section ‹Transfer Operator›

theory Transfer_Operator
  imports Recurrence
begin

context qmpt begin

text ‹The map $T$ acts on measures by push-forward. In particular, if $f d\mu$ is absolutely continuous
with respect to the reference measure $\mu$, then its push-forward $T_*(f d\mu)$ is absolutely
continuous with respect to $\mu$, and can therefore be written as $g d\mu$ for some function $g$.
The map $f \mapsto g$, representing the action of $T$ on the level of densities, is called the
transfer operator associated to $T$ and often denoted by $\hat T$.

We first define it on nonnegative functions, using Radon-Nikodym derivatives. Then, we extend it
to general real-valued functions by separating it into positive and negative parts.

The theory presents many similarities with the theory of conditional expectations. Indeed, it is
possible to make a theory encompassing the two. When the map is measure preserving,
there is also a direct relationship: $(\hat T f) \circ T$ is the conditional expectation of $f$
with respect to $T^{-1}B$ where $B$ is the sigma-algebra. Instead of building a general theory,
we copy the proofs for conditional expectations and adapt them where needed.›

subsection ‹The transfer operator on nonnegative functions›

definition nn_transfer_operator :: "('a ⇒ ennreal) ⇒ ('a ⇒ ennreal)"
where
  "nn_transfer_operator f = (if f ∈ borel_measurable M then RN_deriv M (distr (density M f) M T)
                              else (λ_. 0))"

lemma borel_measurable_nn_transfer_operator [measurable]:
  "nn_transfer_operator f ∈ borel_measurable M"
unfolding nn_transfer_operator_def by auto

lemma borel_measurable_nn_transfer_operator_iterates [measurable]:
  assumes [measurable]: "f ∈ borel_measurable M"
  shows "(nn_transfer_operator^^n) f ∈ borel_measurable M"
by (cases n, auto)

text ‹The next lemma is arguably the most fundamental property of the transfer operator: it is the
adjoint of the composition by $T$. If one defined it as an abstract adjoint, it would be defined
on the dual of $L^\infty$, which is a large unwieldy space. The point is that it can be defined
on genuine functions, using the push-forward point of view above. However, once we have this
property, we can forget completely about the definition, since this property characterizes
the transfer operator, as the second lemma below shows.
From this point on, we will only work with it, and forget completely about
the definition using Radon-Nikodym derivatives.
›

lemma nn_transfer_operator_intg:
  assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "(∫⇧+ x. f x * nn_transfer_operator g x ∂M) = (∫⇧+ x. f (T x) * g x ∂M)"
proof -
  have *: "density M (RN_deriv M (distr (density M g) M T)) = distr (density M g) M T"
    by (rule density_RN_deriv) (auto intro!: quasi_measure_preserving_absolutely_continuous simp add: Tqm)
  have "(∫⇧+ x. f x * nn_transfer_operator g x ∂M) = (∫⇧+ x. f x ∂(density M (RN_deriv M (distr (density M g) M T))))"
    unfolding nn_transfer_operator_def by (simp add: nn_integral_densityR)
  also have "... = (∫⇧+ x. f x ∂(distr (density M g) M T))"
    unfolding * by simp
  also have "... = (∫⇧+ x. f (T x) ∂(density M g))"
    by (rule nn_integral_distr, auto)
  also have "... = (∫⇧+ x. f (T x) * g x ∂M)"
    by (simp add: nn_integral_densityR)
  finally show ?thesis by auto
qed

lemma nn_transfer_operator_intTn_g:
  assumes "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "(∫⇧+ x. f x * (nn_transfer_operator^^n) g x ∂M) = (∫⇧+ x. f ((T^^n) x) * g x ∂M)"
proof -
  have "⋀f g. f ∈ borel_measurable M ⟹ g ∈ borel_measurable M ⟹ (∫⇧+ x. f x * (nn_transfer_operator^^n) g x ∂M) = (∫⇧+ x. f ((T^^n) x) * g x ∂M)" for n
  proof (induction n)
    case (Suc n)
    have [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" by fact+
    have "(∫⇧+ x. f x * (nn_transfer_operator ^^ Suc n) g x ∂M) = (∫⇧+ x. f x * (nn_transfer_operator ((nn_transfer_operator^^n) g)) x ∂M)"
      apply (rule nn_integral_cong) using funpow.simps(2) unfolding comp_def by auto
    also have "... = (∫⇧+ x. f (T x) * (nn_transfer_operator^^n) g x ∂M)"
      by (rule nn_transfer_operator_intg, auto)
    also have "... = (∫⇧+ x. (λx. f (T x)) ((T^^n) x) * g x ∂M)"
      by (rule Suc.IH, auto)
    also have "... = (∫⇧+ x. f ((T^^(Suc n)) x) * g x ∂M)"
      apply (rule nn_integral_cong) using funpow.simps(2) unfolding comp_def by auto
    finally show ?case by auto
  qed (simp)
  then show ?thesis using assms by auto
qed

lemma nn_transfer_operator_intg_Tn:
  assumes "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "(∫⇧+ x. (nn_transfer_operator^^n) g x * f x ∂M) = (∫⇧+ x. g x * f ((T^^n) x) ∂M)"
using nn_transfer_operator_intTn_g[OF assms, of n] by (simp add: algebra_simps)

lemma nn_transfer_operator_charact:
  assumes "⋀A. A ∈ sets M ⟹ (∫⇧+ x. indicator A x * g x ∂M) = (∫⇧+ x. indicator A (T x) * f x ∂M)" and
          [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "AE x in M. nn_transfer_operator f x = g x"
proof -
  have *:"set_nn_integral M A g = set_nn_integral M A (nn_transfer_operator f)" if [measurable]: "A ∈ sets M" for A
  proof -
    have "set_nn_integral M A g = (∫⇧+ x. indicator A x * g x ∂M)"
      using mult.commute by metis
    also have "... = (∫⇧+ x. indicator A (T x) * f x ∂M)"
      using assms(1) by auto
    also have "... = (∫⇧+ x. indicator A x * nn_transfer_operator f x ∂M)"
      by (rule nn_transfer_operator_intg[symmetric], auto)
    finally show ?thesis
      using mult.commute by (metis (no_types, lifting) nn_integral_cong)
  qed
  show ?thesis
    by (rule sigma_finite_measure.density_unique2, auto simp add: sigma_finite_measure_axioms *)
qed

text ‹When $T$ is measure-preserving, $\hat T(f \circ T) = f$.›

lemma (in mpt) nn_transfer_operator_foT:
  assumes [measurable]: "f ∈ borel_measurable M"
  shows "AE x in M. nn_transfer_operator (f o T) x = f x"
proof -
  have *: "(∫⇧+ x. indicator A x * f x ∂M) = (∫⇧+ x. indicator A (T x) * f (T x) ∂M)" if [measurable]: "A ∈ sets M" for A
    by (subst T_nn_integral_preserving[symmetric]) auto
  show ?thesis
    by (rule nn_transfer_operator_charact) (auto simp add: assms *)
qed

text ‹In general, one only has $\hat T(f\circ T \cdot g) = f \cdot \hat T g$.›
lemma nn_transfer_operator_foT_g:
  assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "AE x in M. nn_transfer_operator (λx. f (T x) * g x) x = f x * nn_transfer_operator g x"
proof -
  have *: "(∫⇧+ x. indicator A x * (f x * nn_transfer_operator g x) ∂M) = (∫⇧+ x. indicator A (T x) * (f (T x) * g x) ∂M)"
    if [measurable]: "A ∈ sets M" for A
    by (simp add: mult.assoc[symmetric] nn_transfer_operator_intg)
  show ?thesis
    by (rule nn_transfer_operator_charact) (auto simp add: assms *)
qed

lemma nn_transfer_operator_cmult:
  assumes [measurable]: "g ∈ borel_measurable M"
  shows "AE x in M. nn_transfer_operator (λx. c * g x) x = c * nn_transfer_operator g x"
apply (rule nn_transfer_operator_foT_g) using assms by auto

lemma nn_transfer_operator_zero:
  "AE x in M. nn_transfer_operator (λx. 0) x = 0"
using nn_transfer_operator_cmult[of "λx. 0" 0] by auto

lemma nn_transfer_operator_sum:
  assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "AE x in M. nn_transfer_operator (λx. f x + g x) x = nn_transfer_operator f x + nn_transfer_operator g x"
proof (rule nn_transfer_operator_charact)
  fix A assume [measurable]: "A ∈ sets M"
  have "(∫⇧+ x. indicator A x * (nn_transfer_operator f x + nn_transfer_operator g x) ∂M) =
        (∫⇧+ x. indicator A x * nn_transfer_operator f x + indicator A x * nn_transfer_operator g x ∂M)"
    by (auto simp add: algebra_simps)
  also have "... = (∫⇧+x. indicator A x * nn_transfer_operator f x ∂M) + (∫⇧+x. indicator A x * nn_transfer_operator g x ∂M)"
    by (rule nn_integral_add, auto)
  also have "... = (∫⇧+x. indicator A (T x) * f x ∂M) + (∫⇧+x. indicator A (T x) * g x ∂M)"
    by (simp add: nn_transfer_operator_intg)
  also have "... = (∫⇧+x. indicator A (T x) * f x + indicator A (T x) * g x ∂M)"
    by (rule nn_integral_add[symmetric], auto)
  also have "... = (∫⇧+x. indicator A (T x) * (f x + g x) ∂M)"
    by (auto simp add: algebra_simps)
  finally show "(∫⇧+ x. indicator A x * (nn_transfer_operator f x + nn_transfer_operator g x) ∂M) = (∫⇧+x. indicator A (T x) * (f x + g x) ∂M)"
    by simp
qed (auto simp add: assms)

lemma nn_transfer_operator_cong:
  assumes "AE x in M. f x = g x"
      and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "AE x in M. nn_transfer_operator f x = nn_transfer_operator g x"
apply (rule nn_transfer_operator_charact)
apply (auto simp add: nn_transfer_operator_intg assms intro!: nn_integral_cong_AE)
using assms by auto

lemma nn_transfer_operator_mono:
  assumes "AE x in M. f x ≤ g x"
      and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "AE x in M. nn_transfer_operator f x ≤ nn_transfer_operator g x"
proof -
  define h where "h = (λx. g x - f x)"
  have [measurable]: "h ∈ borel_measurable M" unfolding h_def by simp
  have *: "AE x in M. g x = f x + h x" unfolding h_def using assms(1) by (auto simp: ennreal_ineq_diff_add)
  have "AE x in M. nn_transfer_operator g x = nn_transfer_operator (λx. f x + h x) x"
    by (rule nn_transfer_operator_cong) (auto simp add: * assms)
  moreover have "AE x in M. nn_transfer_operator (λx. f x + h x) x = nn_transfer_operator f x + nn_transfer_operator h x"
    by (rule nn_transfer_operator_sum) (auto simp add: assms)
  ultimately have "AE x in M. nn_transfer_operator g x = nn_transfer_operator f x + nn_transfer_operator h x" by auto
  then show ?thesis by force
qed

subsection ‹The transfer operator on real functions›

text ‹Once the transfer operator of positive functions is defined, the definition for real-valued
functions follows readily, by taking the difference of positive and negative parts.
›

definition real_transfer_operator :: "('a ⇒ real) ⇒ ('a ⇒ real)" where
  "real_transfer_operator f =
    (λx. enn2real(nn_transfer_operator (λx. ennreal (f x)) x) - enn2real(nn_transfer_operator (λx. ennreal (-f x)) x))"

lemma borel_measurable_transfer_operator [measurable]:
  "real_transfer_operator f ∈ borel_measurable M"
unfolding real_transfer_operator_def by auto

lemma borel_measurable_transfer_operator_iterates [measurable]:
  assumes [measurable]: "f ∈ borel_measurable M"
  shows "(real_transfer_operator^^n) f ∈ borel_measurable M"
by (cases n, auto)

lemma real_transfer_operator_abs:
  assumes [measurable]: "f ∈ borel_measurable M"
  shows "AE x in M. abs (real_transfer_operator f x) ≤ nn_transfer_operator (λx. ennreal (abs(f x))) x"
proof -
  define fp where "fp = (λx. ennreal (f x))"
  define fm where "fm = (λx. ennreal (- f x))"
  have [measurable]: "fp ∈ borel_measurable M" "fm ∈ borel_measurable M" unfolding fp_def fm_def by auto
  have eq: "⋀x. ennreal ¦f x¦ = fp x + fm x" unfolding fp_def fm_def by (simp add: abs_real_def ennreal_neg)

  {
    fix x assume H: "nn_transfer_operator (λx. fp x + fm x) x = nn_transfer_operator fp x + nn_transfer_operator fm x"
    have "¦real_transfer_operator f x¦ ≤ ¦enn2real(nn_transfer_operator fp x)¦ + ¦enn2real(nn_transfer_operator fm x)¦"
      unfolding real_transfer_operator_def fp_def fm_def by (auto intro: abs_triangle_ineq4 simp del: enn2real_nonneg)
    from ennreal_leI[OF this]
    have "abs(real_transfer_operator f x) ≤ nn_transfer_operator fp x + nn_transfer_operator fm x"
      by simp (metis add.commute ennreal_enn2real le_iff_add not_le top_unique)
    also have "... = nn_transfer_operator (λx. fp x + fm x) x" using H by simp
    finally have "abs(real_transfer_operator f x) ≤ nn_transfer_operator (λx. fp x + fm x) x" by simp
  }
  moreover have "AE x in M. nn_transfer_operator (λx. fp x + fm x) x = nn_transfer_operator fp x + nn_transfer_operator fm x"
    by (rule nn_transfer_operator_sum) (auto simp add: fp_def fm_def)
  ultimately have "AE x in M. abs(real_transfer_operator f x) ≤ nn_transfer_operator (λx. fp x + fm x) x"
    by auto
  then show ?thesis using eq by simp
qed

text ‹The next lemma shows that the transfer operator as we have defined it satisfies the basic
duality relation $\int \hat T f \cdot g = \int f \cdot g \circ T$. It follows from the same relation
for nonnegative functions, and splitting into positive and negative parts.

Moreover, this relation characterizes the transfer operator. Hence, once this lemma is proved, we
will never come back to the original definition of the transfer operator.›

lemma real_transfer_operator_intg_fpos:
  assumes "integrable M (λx. f (T x) * g x)" and f_pos[simp]: "⋀x. f x ≥ 0" and
          [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "integrable M (λx. f x * real_transfer_operator g x)"
        "(∫ x. f x * real_transfer_operator g x ∂M) = (∫ x. f (T x) * g x ∂M)"
proof -
  define gp where "gp = (λx. ennreal (g x))"
  define gm where "gm = (λx. ennreal (- g x))"
  have [measurable]: "gp ∈ borel_measurable M" "gm ∈ borel_measurable M" unfolding gp_def gm_def by auto
  define h where "h = (λx. ennreal(abs(g x)))"
  have hgpgm: "⋀x. h x = gp x + gm x" unfolding gp_def gm_def h_def by (simp add: abs_real_def ennreal_neg)
  have [measurable]: "h ∈ borel_measurable M" unfolding h_def by simp
  have pos[simp]: "⋀x. h x ≥ 0" "⋀x. gp x ≥ 0" "⋀x. gm x ≥ 0" unfolding h_def gp_def gm_def by simp_all
  have gp_real: "⋀x. enn2real(gp x) = max (g x) 0"
    unfolding gp_def by (simp add: max_def ennreal_neg)
  have gm_real: "⋀x. enn2real(gm x) = max (-g x) 0"
    unfolding gm_def by (simp add: max_def ennreal_neg)

  have "(∫⇧+ x. norm(f (T x) * max (g x) 0) ∂M) ≤ (∫⇧+ x. norm(f (T x) * g x) ∂M)"
    by (simp add: nn_integral_mono)
  also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded)
  finally have "(∫⇧+ x. norm(f (T x) * max (g x) 0) ∂M) < ∞" by simp
  then have int1: "integrable M (λx. f (T x) * max (g x) 0)" by (simp add: integrableI_bounded)

  have "(∫⇧+ x. norm(f (T x) * max (-g x) 0) ∂M) ≤ (∫⇧+ x. norm(f (T x) * g x) ∂M)"
    by (simp add: nn_integral_mono)
  also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded)
  finally have "(∫⇧+ x. norm(f (T x) * max (-g x) 0) ∂M) < ∞" by simp
  then have int2: "integrable M (λx. f (T x) * max (-g x) 0)" by (simp add: integrableI_bounded)

  have "(∫⇧+x. f x * nn_transfer_operator h x ∂M) = (∫⇧+x. f (T x) * h x ∂M)"
    by (rule nn_transfer_operator_intg) auto
  also have "… = ∫⇧+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) ∂M"
    unfolding h_def
    by (intro nn_integral_cong)(auto simp: ennreal_mult[symmetric] abs_mult split: split_max)
  also have "... < ∞"
    using Bochner_Integration.integrable_add[OF int1 int2, THEN integrableD(2)] by (auto simp add: less_top)
  finally have *: "(∫⇧+x. f x * nn_transfer_operator h x ∂M) < ∞" by simp

  have "(∫⇧+x. norm(f x * real_transfer_operator g x) ∂M) = (∫⇧+x. f x * abs(real_transfer_operator g x) ∂M)"
    by (simp add: abs_mult)
  also have "... ≤ (∫⇧+x. f x * nn_transfer_operator h x ∂M)"
  proof (rule nn_integral_mono_AE)
    {
      fix x assume *: "abs(real_transfer_operator g x) ≤ nn_transfer_operator h x"
      have "ennreal (f x * ¦real_transfer_operator g x¦) = f x * ennreal(¦real_transfer_operator g x¦)"
        by (simp add: ennreal_mult)
      also have "... ≤ f x * nn_transfer_operator h x"
        using * by (auto intro!: mult_left_mono)
      finally have "ennreal (f x * ¦real_transfer_operator g x¦) ≤ f x * nn_transfer_operator h x"
        by simp
    }
    then show "AE x in M. ennreal (f x * ¦real_transfer_operator g x¦) ≤ f x * nn_transfer_operator h x"
      using real_transfer_operator_abs[OF assms(4)] h_def by auto
  qed
  finally have **: "(∫⇧+x. norm(f x * real_transfer_operator g x) ∂M) < ∞" using * by auto
  show "integrable M (λx. f x * real_transfer_operator g x)"
    using ** by (intro integrableI_bounded) auto

  have "(∫⇧+x. f x * nn_transfer_operator gp x ∂M) ≤ (∫⇧+x. f x * nn_transfer_operator h x ∂M)"
  proof (rule nn_integral_mono_AE)
    have "AE x in M. nn_transfer_operator gp x ≤ nn_transfer_operator h x"
      by (rule nn_transfer_operator_mono) (auto simp add: hgpgm)
    then show "AE x in M. f x * nn_transfer_operator gp x ≤ f x * nn_transfer_operator h x"
      by (auto simp: mult_left_mono)
  qed
  then have a: "(∫⇧+x. f x * nn_transfer_operator gp x ∂M) < ∞"
    using * by auto
  have "ennreal(norm(f x * enn2real(nn_transfer_operator gp x))) ≤ f x * nn_transfer_operator gp x" for x
    by (auto simp add: ennreal_mult intro!: mult_left_mono)
       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
  then have "(∫⇧+x. norm(f x * enn2real(nn_transfer_operator gp x)) ∂M) ≤ (∫⇧+x. f x * nn_transfer_operator gp x ∂M)"
    by (simp add: nn_integral_mono)
  then have "(∫⇧+x. norm(f x * enn2real(nn_transfer_operator gp x)) ∂M) < ∞" using a by auto
  then have gp_int: "integrable M (λx. f x * enn2real(nn_transfer_operator gp x))" by (simp add: integrableI_bounded)
  have gp_fin: "AE x in M. f x * nn_transfer_operator gp x ≠ ∞"
    apply (rule nn_integral_PInf_AE) using a by auto

  have "(∫ x. f x * enn2real(nn_transfer_operator gp x) ∂M) = enn2real (∫⇧+ x. f x * enn2real(nn_transfer_operator gp x) ∂M)"
    by (rule integral_eq_nn_integral) auto
  also have "... = enn2real(∫⇧+ x. ennreal(f (T x) * enn2real(gp x)) ∂M)"
  proof -
    {
      fix x assume "f x * nn_transfer_operator gp x ≠ ∞"
      then have "ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x"
        by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
    }
    then have "AE x in M. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x"
      using gp_fin by auto
    then have "(∫⇧+ x. f x * enn2real(nn_transfer_operator gp x) ∂M) = (∫⇧+ x. f x * nn_transfer_operator gp x ∂M)"
      by (rule nn_integral_cong_AE)
    also have "... = (∫⇧+ x. f (T x) * gp x ∂M)"
      by (rule nn_transfer_operator_intg) (auto simp add: gp_def)
    also have "... = (∫⇧+ x. ennreal(f (T x) * enn2real(gp x)) ∂M)"
      by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gp_def)
    finally have "(∫⇧+ x. f x * enn2real(nn_transfer_operator gp x) ∂M) = (∫⇧+ x. ennreal(f (T x) * enn2real(gp x)) ∂M)" by simp
    then show ?thesis by simp
  qed
  also have "... = (∫ x. f (T x) * enn2real(gp x) ∂M)"
    by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gp_def)
  finally have gp_expr: "(∫ x. f x * enn2real(nn_transfer_operator gp x) ∂M) = (∫ x. f (T x) * enn2real(gp x) ∂M)" by simp

  have "(∫⇧+x. f x * nn_transfer_operator gm x ∂M) ≤ (∫⇧+x. f x * nn_transfer_operator h x ∂M)"
  proof (rule nn_integral_mono_AE)
    have "AE x in M. nn_transfer_operator gm x ≤ nn_transfer_operator h x"
      by (rule nn_transfer_operator_mono) (auto simp add: hgpgm)
    then show "AE x in M. f x * nn_transfer_operator gm x ≤ f x * nn_transfer_operator h x"
      by (auto simp: mult_left_mono)
  qed
  then have a: "(∫⇧+x. f x * nn_transfer_operator gm x ∂M) < ∞"
    using * by auto
  have "⋀x. ennreal(norm(f x * enn2real(nn_transfer_operator gm x))) ≤ f x * nn_transfer_operator gm x"
    by (auto simp add: ennreal_mult intro!: mult_left_mono)
       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
  then have "(∫⇧+x. norm(f x * enn2real(nn_transfer_operator gm x)) ∂M) ≤ (∫⇧+x. f x * nn_transfer_operator gm x ∂M)"
    by (simp add: nn_integral_mono)
  then have "(∫⇧+x. norm(f x * enn2real(nn_transfer_operator gm x)) ∂M) < ∞" using a by auto
  then have gm_int: "integrable M (λx. f x * enn2real(nn_transfer_operator gm x))" by (simp add: integrableI_bounded)
  have gm_fin: "AE x in M. f x * nn_transfer_operator gm x ≠ ∞"
    apply (rule nn_integral_PInf_AE) using a by auto

  have "(∫ x. f x * enn2real(nn_transfer_operator gm x) ∂M) = enn2real (∫⇧+ x. f x * enn2real(nn_transfer_operator gm x) ∂M)"
    by (rule integral_eq_nn_integral) auto
  also have "... = enn2real(∫⇧+ x. ennreal(f (T x) * enn2real(gm x)) ∂M)"
  proof -
    {
      fix x assume "f x * nn_transfer_operator gm x ≠ ∞"
      then have "ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x"
        by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
    }
    then have "AE x in M. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x"
      using gm_fin by auto
    then have "(∫⇧+ x. f x * enn2real(nn_transfer_operator gm x) ∂M) = (∫⇧+ x. f x * nn_transfer_operator gm x ∂M)"
      by (rule nn_integral_cong_AE)
    also have "... = (∫⇧+ x. f (T x) * gm x ∂M)"
      by (rule nn_transfer_operator_intg) (auto simp add: gm_def)
    also have "... = (∫⇧+ x. ennreal(f (T x) * enn2real(gm x)) ∂M)"
      by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gm_def)
    finally have "(∫⇧+ x. f x * enn2real(nn_transfer_operator gm x) ∂M) = (∫⇧+ x. ennreal(f (T x) * enn2real(gm x)) ∂M)" by simp
    then show ?thesis by simp
  qed
  also have "... = (∫ x. f (T x) * enn2real(gm x) ∂M)"
    by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gm_def)
  finally have gm_expr: "(∫ x. f x * enn2real(nn_transfer_operator gm x) ∂M) = (∫ x. f (T x) * enn2real(gm x) ∂M)" by simp

  have "(∫ x. f x * real_transfer_operator g x ∂M) = (∫ x. f x * enn2real(nn_transfer_operator gp x) - f x * enn2real(nn_transfer_operator gm x) ∂M)"
    unfolding real_transfer_operator_def gp_def gm_def by (simp add: right_diff_distrib)
  also have "... = (∫ x. f x * enn2real(nn_transfer_operator gp x) ∂M) - (∫ x. f x * enn2real(nn_transfer_operator gm x) ∂M)"
    by (rule Bochner_Integration.integral_diff) (simp_all add: gp_int gm_int)
  also have "... = (∫ x. f (T x) * enn2real(gp x) ∂M) - (∫ x. f (T x) * enn2real(gm x) ∂M)"
    using gp_expr gm_expr by simp
  also have "... = (∫ x. f (T x) * max (g x) 0 ∂M) - (∫ x. f (T x) * max (-g x) 0 ∂M)"
    using gp_real gm_real by simp
  also have "... = (∫ x. f (T x) * max (g x) 0 - f (T x) * max (-g x) 0 ∂M)"
    by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2)
  also have "... = (∫x. f (T x) * g x ∂M)"
    by (metis (mono_tags, opaque_lifting) diff_0 diff_zero eq_iff max.cobounded2 max_def minus_minus neg_le_0_iff_le right_diff_distrib)
  finally show "(∫ x. f x * real_transfer_operator g x ∂M) = (∫x. f (T x) * g x ∂M)"
    by simp
qed

lemma real_transfer_operator_intg:
  assumes "integrable M (λx. f (T x) * g x)" and
          [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "integrable M (λx. f x * real_transfer_operator g x)"
        "(∫ x. f x * real_transfer_operator g x ∂M) = (∫ x. f (T x) * g x ∂M)"
proof -
  define fp where "fp = (λx. max (f x) 0)"
  define fm where "fm = (λx. max (-f x) 0)"
  have [measurable]: "fp ∈ borel_measurable M" "fm ∈ borel_measurable M"
    unfolding fp_def fm_def by simp_all

  have "(∫⇧+ x. norm(fp (T x) * g x) ∂M) ≤ (∫⇧+ x. norm(f (T x) * g x) ∂M)"
    by (simp add: fp_def nn_integral_mono)
  also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded)
  finally have "(∫⇧+ x. norm(fp (T x) * g x) ∂M) < ∞" by simp
  then have intp: "integrable M (λx. fp (T x) * g x)" by (simp add: integrableI_bounded)
  moreover have "⋀x. fp x ≥ 0" unfolding fp_def by simp
  ultimately have Rp: "integrable M (λx. fp x * real_transfer_operator g x)"
    "(∫ x. fp x * real_transfer_operator g x ∂M) = (∫ x. fp (T x) * g x ∂M)"
  using real_transfer_operator_intg_fpos by auto

  have "(∫⇧+ x. norm(fm (T x) * g x) ∂M) ≤ (∫⇧+ x. norm(f (T x) * g x) ∂M)"
    by (simp add: fm_def nn_integral_mono)
  also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded)
  finally have "(∫⇧+ x. norm(fm (T x) * g x) ∂M) < ∞" by simp
  then have intm: "integrable M (λx. fm (T x) * g x)" by (simp add: integrableI_bounded)
  moreover have "⋀x. fm x ≥ 0" unfolding fm_def by simp
  ultimately have Rm: "integrable M (λx. fm x * real_transfer_operator g x)"
    "(∫ x. fm x * real_transfer_operator g x ∂M) = (∫ x. fm (T x) * g x ∂M)"
  using real_transfer_operator_intg_fpos by auto

  have "integrable M (λx. fp x * real_transfer_operator g x - fm x * real_transfer_operator g x)"
    using Rp(1) Rm(1) integrable_diff by simp
  moreover have *: "⋀x. f x * real_transfer_operator g x = fp x * real_transfer_operator g x - fm x * real_transfer_operator g x"
    unfolding fp_def fm_def by (simp add: max_def)
  ultimately show "integrable M (λx. f x * real_transfer_operator g x)"
    by simp

  have "(∫ x. f x * real_transfer_operator g x ∂M) = (∫ x. fp x * real_transfer_operator g x - fm x * real_transfer_operator g x ∂M)"
    using * by simp
  also have "... = (∫ x. fp x * real_transfer_operator g x ∂M) - (∫ x. fm x * real_transfer_operator g x ∂M)"
    using Rp(1) Rm(1) by simp
  also have "... = (∫ x. fp (T x) * g x ∂M) - (∫ x. fm (T x) * g x ∂M)"
    using Rp(2) Rm(2) by simp
  also have "... = (∫ x. fp (T x) * g x - fm (T x) * g x ∂M)"
    using intm intp by simp
  also have "... = (∫ x. f (T x) * g x ∂M)"
    unfolding fp_def fm_def by (metis (no_types, opaque_lifting) diff_0 diff_zero max.commute
    max_def minus_minus mult.commute neg_le_iff_le right_diff_distrib)
  finally show "(∫ x. f x * real_transfer_operator g x ∂M) = (∫ x. f (T x) * g x ∂M)" by simp
qed

lemma real_transfer_operator_int [intro]:
  assumes "integrable M f"
  shows "integrable M (real_transfer_operator f)"
        "(∫x. real_transfer_operator f x ∂M) = (∫x. f x ∂M)"
using real_transfer_operator_intg[where ?f = "λx. 1" and ?g = f] assms by auto

lemma real_transfer_operator_charact:
  assumes "⋀A. A ∈ sets M ⟹ (∫x. indicator A x * g x ∂M) = (∫x. indicator A (T x) * f x ∂M)"
      and [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator f x = g x"
proof (rule AE_symmetric[OF density_unique_real])
  fix A assume [measurable]: "A ∈ sets M"
  have "set_lebesgue_integral M A (real_transfer_operator f) = (∫x. indicator A x * real_transfer_operator f x ∂M)"
    unfolding set_lebesgue_integral_def by auto
  also have "... = (∫x. indicator A (T x) * f x ∂M)"
    apply (rule real_transfer_operator_intg, auto)
    by (rule Bochner_Integration.integrable_bound[of _ "λx. abs(f x)"], auto simp add: assms indicator_def)
  also have "... = set_lebesgue_integral M A g"
    unfolding set_lebesgue_integral_def using assms(1)[OF ‹A ∈ sets M›] by auto
  finally show "set_lebesgue_integral M A g = set_lebesgue_integral M A (real_transfer_operator f)"
    by simp
qed (auto simp add: assms real_transfer_operator_int)

lemma (in mpt) real_transfer_operator_foT:
  assumes "integrable M f"
  shows "AE x in M. real_transfer_operator (f o T) x = f x"
proof -
  have *: "(∫ x. indicator A x * f x ∂M) = (∫x. indicator A (T x) * f (T x) ∂M)" if [measurable]: "A ∈ sets M" for A
    apply (subst T_integral_preserving)
    using integrable_real_mult_indicator[OF that assms] by (auto simp add: mult.commute)
  show ?thesis
    apply (rule real_transfer_operator_charact)
    using assms * by (auto simp add: comp_def T_integral_preserving)
qed

lemma real_transfer_operator_foT_g:
  assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" "integrable M (λx. f (T x) * g x)"
  shows "AE x in M. real_transfer_operator (λx. f (T x) * g x) x = f x * real_transfer_operator g x"
proof -
  have *: "(∫x. indicator A x * (f x * real_transfer_operator g x) ∂M) = (∫x. indicator A (T x) * (f (T x) * g x) ∂M)"
    if [measurable]: "A ∈ sets M" for A
    apply (simp add: mult.assoc[symmetric])
    apply (subst real_transfer_operator_intg)
    apply (rule Bochner_Integration.integrable_bound[of _ "(λx. f (T x) * g x)"])
    by (auto simp add: assms indicator_def)
  show ?thesis
    by (rule real_transfer_operator_charact) (auto simp add: assms * intro!: real_transfer_operator_intg)
qed

lemma real_transfer_operator_add [intro]:
  assumes [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator (λx. f x + g x) x = real_transfer_operator f x + real_transfer_operator g x"
proof (rule real_transfer_operator_charact)
  have "integrable M (real_transfer_operator f)" "integrable M (real_transfer_operator g)"
    using real_transfer_operator_int(1) assms by auto
  then show "integrable M (λx. real_transfer_operator f x + real_transfer_operator g x)"
    by auto

  fix A assume [measurable]: "A ∈ sets M"
  have intAf: "integrable M (λx. indicator A (T x) * f x)"
    apply (rule Bochner_Integration.integrable_bound[OF assms(1)]) unfolding indicator_def by auto
  have intAg: "integrable M (λx. indicator A (T x) * g x)"
    apply (rule Bochner_Integration.integrable_bound[OF assms(2)]) unfolding indicator_def by auto

  have "(∫x. indicator A x * (real_transfer_operator f x + real_transfer_operator g x)∂M)
      = (∫x. indicator A x * real_transfer_operator f x + indicator A x* real_transfer_operator g x ∂M)"
    by (simp add: algebra_simps)
  also have "... = (∫x. indicator A x * real_transfer_operator f x ∂M) + (∫x. indicator A x * real_transfer_operator g x ∂M)"
    apply (rule Bochner_Integration.integral_add)
    using integrable_real_mult_indicator[OF ‹A ∈ sets M› real_transfer_operator_int(1)[OF assms(1)]]
          integrable_real_mult_indicator[OF ‹A ∈ sets M› real_transfer_operator_int(1)[OF assms(2)]]
    by (auto simp add: mult.commute)
  also have "... = (∫x. indicator A (T x) * f x ∂M) + (∫x. indicator A (T x) * g x ∂M)"
    using real_transfer_operator_intg(2) assms ‹A ∈ sets M› intAf intAg by auto
  also have "... = (∫x. indicator A (T x) * f x + indicator A (T x) * g x ∂M)"
    by (rule Bochner_Integration.integral_add[symmetric]) (auto simp add: assms ‹A ∈ sets M› intAf intAg)
  also have "... = ∫x. indicator A (T x) * (f x + g x)∂M"
    by (simp add: algebra_simps)
  finally show "(∫x. indicator A x * (real_transfer_operator f x + real_transfer_operator g x)∂M) = ∫x. indicator A (T x) * (f x + g x)∂M"
    by simp
qed (auto simp add: assms)

lemma real_transfer_operator_cong:
  assumes ae: "AE x in M. f x = g x" and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M"
  shows "AE x in M. real_transfer_operator f x = real_transfer_operator g x"
proof -
  have "AE x in M. nn_transfer_operator (λx. ennreal (f x)) x = nn_transfer_operator (λx. ennreal (g x)) x"
    apply (rule nn_transfer_operator_cong) using assms by auto
  moreover have "AE x in M. nn_transfer_operator (λx. ennreal (-f x)) x = nn_transfer_operator (λx. ennreal(-g x)) x"
    apply (rule nn_transfer_operator_cong) using assms by auto
  ultimately show "AE x in M. real_transfer_operator f x = real_transfer_operator g x"
    unfolding real_transfer_operator_def by auto
qed

lemma real_transfer_operator_cmult [intro, simp]:
  fixes c::real
  assumes "integrable M f"
  shows "AE x in M. real_transfer_operator (λx. c * f x) x = c * real_transfer_operator f x"
by (rule real_transfer_operator_foT_g) (auto simp add: assms borel_measurable_integrable)

lemma real_transfer_operator_cdiv [intro, simp]:
  fixes c::real
  assumes "integrable M f"
  shows "AE x in M. real_transfer_operator (λx. f x / c) x = real_transfer_operator f x / c"
using real_transfer_operator_cmult[of _ "1/c", OF assms] by (auto simp add: divide_simps)

lemma real_transfer_operator_diff [intro, simp]:
  assumes [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator (λx. f x - g x) x = real_transfer_operator f x - real_transfer_operator g x"
proof -
  have "AE x in M. real_transfer_operator (λx. f x + (- g x)) x = real_transfer_operator f x + real_transfer_operator (λx. -g x) x"
    using real_transfer_operator_add[where ?f = f and ?g = "λx. - g x"] assms by auto
  moreover have "AE x in M. real_transfer_operator (λx. -g x) x = - real_transfer_operator g x"
    using real_transfer_operator_cmult[where ?f = g and ?c = "-1"] assms(2) by auto
  ultimately show ?thesis by auto
qed

lemma real_transfer_operator_pos [intro]:
  assumes "AE x in M. f x ≥ 0" and [measurable]: "f ∈ borel_measurable M"
  shows "AE x in M. real_transfer_operator f x ≥ 0"
proof -
  define g where "g = (λx. max (f x) 0)"
  have "AE x in M. f x = g x" using assms g_def by auto
  then have *: "AE x in M. real_transfer_operator f x = real_transfer_operator g x" using real_transfer_operator_cong g_def by auto

  have "⋀x. g x ≥ 0" unfolding g_def by simp
  then have "(λx. ennreal(-g x)) = (λx. 0)"
    by (simp add: ennreal_neg)
  then have "AE x in M. nn_transfer_operator (λx. ennreal(-g x)) x = 0"
    using nn_transfer_operator_zero by simp
  then have "AE x in M. real_transfer_operator g x = enn2real(nn_transfer_operator (λx. ennreal (g x)) x)"
    unfolding real_transfer_operator_def by auto
  then have "AE x in M. real_transfer_operator g x ≥ 0" by auto
  then show ?thesis using * by auto
qed

lemma real_transfer_operator_mono:
  assumes "AE x in M. f x ≤ g x" and [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator f x ≤ real_transfer_operator g x"
proof -
  have "AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (λx. g x - f x) x"
    by (rule AE_symmetric[OF real_transfer_operator_diff], auto simp add: assms)
  moreover have "AE x in M. real_transfer_operator (λx. g x - f x) x ≥ 0"
    by (rule real_transfer_operator_pos, auto simp add: assms(1))
  ultimately have "AE x in M. real_transfer_operator g x - real_transfer_operator f x ≥ 0" by auto
  then show ?thesis by auto
qed

lemma real_transfer_operator_sum [intro, simp]:
  fixes f::"'b ⇒ 'a ⇒ real"
  assumes [measurable]: "⋀i. integrable M (f i)"
  shows "AE x in M. real_transfer_operator (λx. ∑i∈I. f i x) x = (∑i∈I. real_transfer_operator (f i) x)"
proof (rule real_transfer_operator_charact)
  fix A assume [measurable]: "A ∈ sets M"
  have *: "integrable M (λx. indicator A (T x) * f i x)" for i
    apply (rule Bochner_Integration.integrable_bound[of _ "f i"]) by (auto simp add: assms indicator_def)
  have **: "integrable M (λx. indicator A x * real_transfer_operator (f i) x)" for i
    apply (rule Bochner_Integration.integrable_bound[of _ "real_transfer_operator (f i)"]) by (auto simp add: assms indicator_def)
  have inti: "(∫x. indicator A (T x) * f i x ∂M) = (∫x. indicator A x * real_transfer_operator (f i) x ∂M)" for i
    by (rule real_transfer_operator_intg(2)[symmetric], auto simp add: *)

  have "(∫x. indicator A (T x) * (∑i∈I. f i x)∂M) = (∫x. (∑i∈I. indicator A (T x) * f i x)∂M)"
    by (simp add: sum_distrib_left)
  also have "... = (∑i∈I. (∫x. indicator A (T x) * f i x ∂M))"
    by (rule Bochner_Integration.integral_sum, simp add: *)
  also have "... = (∑i∈I. (∫x. indicator A x * real_transfer_operator (f i) x ∂M))"
    using inti by auto
  also have "... = (∫x. (∑i∈I. indicator A x * real_transfer_operator (f i) x)∂M)"
    by (rule Bochner_Integration.integral_sum[symmetric], simp add: **)
  also have "... = (∫x. indicator A x * (∑i∈I. real_transfer_operator (f i) x)∂M)"
    by (simp add: sum_distrib_left)
  finally show "(∫x. indicator A x * (∑i∈I. real_transfer_operator (f i) x)∂M) = (∫x. indicator A (T x) * (∑i∈I. f i x)∂M)" by auto
qed (auto simp add: assms real_transfer_operator_int(1)[OF assms(1)])
end (*of context qmpt*)



subsection ‹Conservativity in terms of transfer operators›

text ‹Conservativity amounts to the fact that $\sum f(T^n x) = \infty$ for almost every $x$
such that $f(x)>0$, if $f$ is nonnegative (see Lemma \verb+recurrent_series_infinite+).
There is a dual formulation, in terms of transfer
operators, asserting that $\sum \hat T^n f(x) = \infty$ for almost every $x$ such that $f(x)>0$.
It is proved by duality, reducing to the previous statement.›

theorem (in conservative) recurrence_series_infinite_transfer_operator:
  assumes [measurable]: "f ∈ borel_measurable M"
  shows "AE x in M. f x > 0 ⟶ (∑n. (nn_transfer_operator^^n) f x) = ∞"
proof -
  define A where "A = {x ∈ space M. f x > 0}"
  have [measurable]: "A ∈ sets M"
    unfolding A_def by auto
  have K: "emeasure M {x ∈ A. (∑n. (nn_transfer_operator^^n) f x) ≤ K} = 0" if "K < ∞" for K
  proof (rule ccontr)
    assume "emeasure M {x ∈ A. (∑n. (nn_transfer_operator^^n) f x) ≤ K} ≠ 0"
    then have *: "emeasure M {x ∈ A. (∑n. (nn_transfer_operator^^n) f x) ≤ K} > 0"
      using not_gr_zero by blast
    obtain B where B [measurable]: "B ∈ sets M" "B ⊆ {x ∈ A. (∑n. (nn_transfer_operator^^n) f x) ≤ K}" "emeasure M B < ∞" "emeasure M B > 0"
      using approx_with_finite_emeasure[OF _ *] by auto
    have "f x > 0" if "x ∈ B" for x
      using B(2) that unfolding A_def by auto
    moreover have "AE x∈B in M. (∑n. indicator B ((T^^n) x)) = (∞::ennreal)"
      using recurrence_series_infinite[of "indicator B"] by (auto simp add: indicator_def)
    ultimately have PInf: "AE x∈B in M. (∑n. indicator B ((T^^n) x)) * f x = ⊤"
      unfolding ennreal_mult_eq_top_iff by fastforce

    have "(∫⇧+x. indicator B x * (∑n. (nn_transfer_operator^^n) f x) ∂M) ≤ (∫⇧+x. indicator B x * K ∂M)"
      apply (rule nn_integral_mono) using B(2) unfolding indicator_def by auto
    also have "... = K * emeasure M B"
      by (simp add: mult.commute nn_integral_cmult_indicator)
    also have "... < ∞" using ‹K < ∞› B(3)
      using ennreal_mult_eq_top_iff top.not_eq_extremum by auto
    finally have *: "(∫⇧+x. indicator B x * (∑n. (nn_transfer_operator^^n) f x) ∂M) < ∞" by auto

    have "(∫⇧+x. indicator B x * (∑n. (nn_transfer_operator^^n) f x) ∂M)
            = (∫⇧+x. (∑n. indicator B x * (nn_transfer_operator^^n) f x) ∂M)"
      by auto
    also have "... = (∑n. (∫⇧+x. indicator B x * (nn_transfer_operator^^n) f x ∂M))"
      by (rule nn_integral_suminf, auto)
    also have "... = (∑n. (∫⇧+x. indicator B ((T^^n) x) * f x ∂M))"
      using nn_transfer_operator_intTn_g by auto
    also have "... = (∫⇧+x. (∑n. indicator B ((T^^n) x) * f x) ∂M)"
      by (rule nn_integral_suminf[symmetric], auto)
    also have "... = (∫⇧+x. (∑n. indicator B ((T^^n) x)) * f x ∂M)"
      by auto
    finally have **: "(∫⇧+x. (∑n. indicator B ((T^^n) x)) * f x ∂M) ≠ ∞"
      using * by simp
    have "AE x in M. (∑n. indicator B ((T^^n) x)) * f x ≠ ∞"
      by (rule nn_integral_noteq_infinite[OF _ **], auto)
    then have "AE x∈B in M. False"
      using PInf by auto
    then have "emeasure M B = 0"
      by (smt AE_E B(1) Collect_mem_eq Collect_mono_iff dual_order.trans emeasure_eq_0 subsetD sets.sets_into_space)
    then show False
      using B by auto
  qed
  have L: "{x ∈ A. (∑n. (nn_transfer_operator^^n) f x) ≤ K} ∈ null_sets M" if "K < ∞" for K
    using K[OF that] by auto
  have P: "AE x in M. x ∈ A ⟶ (∑n. (nn_transfer_operator^^n) f x) ≥ K" if "K < ∞" for K
    using AE_not_in[OF L[OF that]] by auto
  have "AE x in M. ∀N::nat. (x ∈ A ⟶ (∑n. (nn_transfer_operator^^n) f x) ≥ of_nat N)"
    unfolding AE_all_countable by (auto simp add: of_nat_less_top intro!: P)
  then have "AE x in M. f x > 0 ⟶ (∀N::nat. (∑n. (nn_transfer_operator^^n) f x) ≥ of_nat N)"
    unfolding A_def by auto
  then show "AE x in M. 0 < f x ⟶ (∑n. (nn_transfer_operator ^^ n) f x) = ∞"
    using ennreal_ge_nat_imp_PInf by auto
qed


end (*of Transfer_Operator.thy*)