(* 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, hide_lams) 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, hide_lams) 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*)