[STATEMENT]
lemma real_transfer_operator_intg_fpos:
  assumes "integrable M (\<lambda>x. f (T x) * g x)" and f_pos[simp]: "\<And>x. f x \<ge> 0" and
          [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
  shows "integrable M (\<lambda>x. f x * real_transfer_operator g x)"
        "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral> x. f (T x) * g x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x) &&& LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
define gp where "gp = (\<lambda>x. ennreal (g x))"
[PROOF STATE]
proof (state)
this:
gp = (\<lambda>x. ennreal (g x))

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
define gm where "gm = (\<lambda>x. ennreal (- g x))"
[PROOF STATE]
proof (state)
this:
gm = (\<lambda>x. ennreal (- g x))

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have [measurable]: "gp \<in> borel_measurable M" "gm \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gp \<in> borel_measurable M &&& gm \<in> borel_measurable M
[PROOF STEP]
unfolding gp_def gm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. ennreal (g x)) \<in> borel_measurable M &&& (\<lambda>x. ennreal (- g x)) \<in> borel_measurable M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gp \<in> borel_measurable M
gm \<in> borel_measurable M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
define h where "h = (\<lambda>x. ennreal(abs(g x)))"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>x. ennreal \<bar>g x\<bar>)

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have hgpgm: "\<And>x. h x = gp x + gm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. h x = gp x + gm x
[PROOF STEP]
unfolding gp_def gm_def h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ennreal \<bar>g x\<bar> = ennreal (g x) + ennreal (- g x)
[PROOF STEP]
by (simp add: abs_real_def ennreal_neg)
[PROOF STATE]
proof (state)
this:
h ?x3 = gp ?x3 + gm ?x3

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have [measurable]: "h \<in> borel_measurable M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<in> borel_measurable M
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. ennreal \<bar>g x\<bar>) \<in> borel_measurable M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h \<in> borel_measurable M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have pos[simp]: "\<And>x. h x \<ge> 0" "\<And>x. gp x \<ge> 0" "\<And>x. gm x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. 0 \<le> h x) &&& (\<And>x. 0 \<le> gp x) &&& (\<And>x. 0 \<le> gm x)
[PROOF STEP]
unfolding h_def gp_def gm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. 0 \<le> ennreal \<bar>g x\<bar>) &&& (\<And>x. 0 \<le> ennreal (g x)) &&& (\<And>x. 0 \<le> ennreal (- g x))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> h ?x3
0 \<le> gp ?x3
0 \<le> gm ?x3

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have gp_real: "\<And>x. enn2real(gp x) = max (g x) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. enn2real (gp x) = max (g x) 0
[PROOF STEP]
unfolding gp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. enn2real (ennreal (g x)) = max (g x) 0
[PROOF STEP]
by (simp add: max_def ennreal_neg)
[PROOF STATE]
proof (state)
this:
enn2real (gp ?x3) = max (g ?x3) 0

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have gm_real: "\<And>x. enn2real(gm x) = max (-g x) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. enn2real (gm x) = max (- g x) 0
[PROOF STEP]
unfolding gm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. enn2real (ennreal (- g x)) = max (- g x) 0
[PROOF STEP]
by (simp add: max_def ennreal_neg)
[PROOF STATE]
proof (state)
this:
enn2real (gm ?x3) = max (- g ?x3) 0

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral>\<^sup>+ x. norm(f (T x) * max (g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f (T x) * g x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M
[PROOF STEP]
by (simp add: nn_integral_mono)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M < \<infinity>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. f (T x) * g x)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M < \<infinity>
[PROOF STEP]
by (simp add: integrable_iff_bounded)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M < \<infinity>

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M < \<infinity>
[PROOF STEP]
have "(\<integral>\<^sup>+ x. norm(f (T x) * max (g x) 0) \<partial>M) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M < \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M < \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M < \<infinity>

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M < \<infinity>
[PROOF STEP]
have int1: "integrable M (\<lambda>x. f (T x) * max (g x) 0)"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (g x) 0)) \<partial>M < \<infinity>

goal (1 subgoal):
 1. integrable M (\<lambda>x. f (T x) * max (g x) 0)
[PROOF STEP]
by (simp add: integrableI_bounded)
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. f (T x) * max (g x) 0)

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral>\<^sup>+ x. norm(f (T x) * max (-g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f (T x) * g x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M
[PROOF STEP]
by (simp add: nn_integral_mono)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M < \<infinity>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. f (T x) * g x)

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M < \<infinity>
[PROOF STEP]
by (simp add: integrable_iff_bounded)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * g x)) \<partial>M < \<infinity>

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M < \<infinity>
[PROOF STEP]
have "(\<integral>\<^sup>+ x. norm(f (T x) * max (-g x) 0) \<partial>M) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M < \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M < \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M < \<infinity>

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M < \<infinity>
[PROOF STEP]
have int2: "integrable M (\<lambda>x. f (T x) * max (-g x) 0)"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f (T x) * max (- g x) 0)) \<partial>M < \<infinity>

goal (1 subgoal):
 1. integrable M (\<lambda>x. f (T x) * max (- g x) 0)
[PROOF STEP]
by (simp add: integrableI_bounded)
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. f (T x) * max (- g x) 0)

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M) = (\<integral>\<^sup>+x. f (T x) * h x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * h x \<partial>M
[PROOF STEP]
by (rule nn_transfer_operator_intg) auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * h x \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * h x \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "\<dots> = \<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f (T x)) * h x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f (T x)) * ennreal \<bar>g x\<bar> \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M
[PROOF STEP]
by (intro nn_integral_cong)(auto simp: ennreal_mult[symmetric] abs_mult split: split_max)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f (T x)) * h x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f (T x)) * h x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... < \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M < \<infinity>
[PROOF STEP]
using Bochner_Integration.integrable_add[OF int1 int2, THEN integrableD(2)]
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M \<noteq> \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M < \<infinity>
[PROOF STEP]
by (auto simp add: less_top)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f (T x) * max (g x) 0 + f (T x) * max (- g x) 0) \<partial>M < \<infinity>

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M < \<infinity>
[PROOF STEP]
have *: "(\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M < \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M < \<infinity>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M < \<infinity>

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral>\<^sup>+x. norm(f x * real_transfer_operator g x) \<partial>M) = (\<integral>\<^sup>+x. f x * abs(real_transfer_operator g x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<partial>M
[PROOF STEP]
by (simp add: abs_mult)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
[PROOF STEP]
proof (rule nn_integral_mono_AE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
assume *: "abs(real_transfer_operator g x) \<le> nn_transfer_operator h x"
[PROOF STATE]
proof (state)
this:
ennreal \<bar>real_transfer_operator g x\<bar> \<le> nn_transfer_operator h x

goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
have "ennreal (f x * \<bar>real_transfer_operator g x\<bar>) = f x * ennreal(\<bar>real_transfer_operator g x\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) = ennreal (f x) * ennreal \<bar>real_transfer_operator g x\<bar>
[PROOF STEP]
by (simp add: ennreal_mult)
[PROOF STATE]
proof (state)
this:
ennreal (f x * \<bar>real_transfer_operator g x\<bar>) = ennreal (f x) * ennreal \<bar>real_transfer_operator g x\<bar>

goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ennreal (f x * \<bar>real_transfer_operator g x\<bar>) = ennreal (f x) * ennreal \<bar>real_transfer_operator g x\<bar>

goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
have "... \<le> f x * nn_transfer_operator h x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (f x) * ennreal \<bar>real_transfer_operator g x\<bar> \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
ennreal \<bar>real_transfer_operator g x\<bar> \<le> nn_transfer_operator h x

goal (1 subgoal):
 1. ennreal (f x) * ennreal \<bar>real_transfer_operator g x\<bar> \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
by (auto intro!: mult_left_mono)
[PROOF STATE]
proof (state)
this:
ennreal (f x) * ennreal \<bar>real_transfer_operator g x\<bar> \<le> ennreal (f x) * nn_transfer_operator h x

goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
have "ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> f x * nn_transfer_operator h x"
[PROOF STATE]
proof (prove)
using this:
ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x

goal (1 subgoal):
 1. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x

goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ennreal \<bar>real_transfer_operator g ?x5\<bar> \<le> nn_transfer_operator h ?x5 \<Longrightarrow> ennreal (f ?x5 * \<bar>real_transfer_operator g ?x5\<bar>) \<le> ennreal (f ?x5) * nn_transfer_operator h ?x5

goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal \<bar>real_transfer_operator g ?x5\<bar> \<le> nn_transfer_operator h ?x5 \<Longrightarrow> ennreal (f ?x5 * \<bar>real_transfer_operator g ?x5\<bar>) \<le> ennreal (f ?x5) * nn_transfer_operator h ?x5
[PROOF STEP]
show "AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> f x * nn_transfer_operator h x"
[PROOF STATE]
proof (prove)
using this:
ennreal \<bar>real_transfer_operator g ?x5\<bar> \<le> nn_transfer_operator h ?x5 \<Longrightarrow> ennreal (f ?x5 * \<bar>real_transfer_operator g ?x5\<bar>) \<le> ennreal (f ?x5) * nn_transfer_operator h ?x5

goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
using real_transfer_operator_abs[OF assms(4)] h_def
[PROOF STATE]
proof (prove)
using this:
ennreal \<bar>real_transfer_operator g ?x5\<bar> \<le> nn_transfer_operator h ?x5 \<Longrightarrow> ennreal (f ?x5 * \<bar>real_transfer_operator g ?x5\<bar>) \<le> ennreal (f ?x5) * nn_transfer_operator h ?x5
AE x in M. ennreal \<bar>real_transfer_operator g x\<bar> \<le> nn_transfer_operator (\<lambda>x. ennreal \<bar>g x\<bar>) x
h = (\<lambda>x. ennreal \<bar>g x\<bar>)

goal (1 subgoal):
 1. AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<le> ennreal (f x) * nn_transfer_operator h x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x * \<bar>real_transfer_operator g x\<bar>) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
[PROOF STEP]
have **: "(\<integral>\<^sup>+x. norm(f x * real_transfer_operator g x) \<partial>M) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M < \<infinity>
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M < \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M < \<infinity>

goal (2 subgoals):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
 2. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
show "integrable M (\<lambda>x. f x * real_transfer_operator g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
[PROOF STEP]
using **
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * real_transfer_operator g x)) \<partial>M < \<infinity>

goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * real_transfer_operator g x)
[PROOF STEP]
by (intro integrableI_bounded) auto
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. f x * real_transfer_operator g x)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral>\<^sup>+x. f x * nn_transfer_operator gp x \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
[PROOF STEP]
proof (rule nn_integral_mono_AE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. ennreal (f x) * nn_transfer_operator gp x \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
have "AE x in M. nn_transfer_operator gp x \<le> nn_transfer_operator h x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. nn_transfer_operator gp x \<le> nn_transfer_operator h x
[PROOF STEP]
by (rule nn_transfer_operator_mono) (auto simp add: hgpgm)
[PROOF STATE]
proof (state)
this:
AE x in M. nn_transfer_operator gp x \<le> nn_transfer_operator h x

goal (1 subgoal):
 1. AE x in M. ennreal (f x) * nn_transfer_operator gp x \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. nn_transfer_operator gp x \<le> nn_transfer_operator h x
[PROOF STEP]
show "AE x in M. f x * nn_transfer_operator gp x \<le> f x * nn_transfer_operator h x"
[PROOF STATE]
proof (prove)
using this:
AE x in M. nn_transfer_operator gp x \<le> nn_transfer_operator h x

goal (1 subgoal):
 1. AE x in M. ennreal (f x) * nn_transfer_operator gp x \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
by (auto simp: mult_left_mono)
[PROOF STATE]
proof (state)
this:
AE x in M. ennreal (f x) * nn_transfer_operator gp x \<le> ennreal (f x) * nn_transfer_operator h x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
[PROOF STEP]
have a: "(\<integral>\<^sup>+x. f x * nn_transfer_operator gp x \<partial>M) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M < \<infinity>
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M < \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M < \<infinity>

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "ennreal(norm(f x * enn2real(nn_transfer_operator gp x))) \<le> f x * nn_transfer_operator gp x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<le> ennreal (f x) * nn_transfer_operator gp x
[PROOF STEP]
by (auto simp add: ennreal_mult intro!: mult_left_mono)
       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
[PROOF STATE]
proof (state)
this:
ennreal (norm (f ?x3 * enn2real (nn_transfer_operator gp ?x3))) \<le> ennreal (f ?x3) * nn_transfer_operator gp ?x3

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (norm (f ?x3 * enn2real (nn_transfer_operator gp ?x3))) \<le> ennreal (f ?x3) * nn_transfer_operator gp ?x3
[PROOF STEP]
have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_transfer_operator gp x)) \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator gp x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
ennreal (norm (f ?x3 * enn2real (nn_transfer_operator gp ?x3))) \<le> ennreal (f ?x3) * nn_transfer_operator gp ?x3

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M
[PROOF STEP]
by (simp add: nn_integral_mono)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M
[PROOF STEP]
have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_transfer_operator gp x)) \<partial>M) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M < \<infinity>
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M < \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M < \<infinity>

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M < \<infinity>
[PROOF STEP]
have gp_int: "integrable M (\<lambda>x. f x * enn2real(nn_transfer_operator gp x))"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gp x))) \<partial>M < \<infinity>

goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * enn2real (nn_transfer_operator gp x))
[PROOF STEP]
by (simp add: integrableI_bounded)
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. f x * enn2real (nn_transfer_operator gp x))

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have gp_fin: "AE x in M. f x * nn_transfer_operator gp x \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. ennreal (f x) * nn_transfer_operator gp x \<noteq> \<infinity>
[PROOF STEP]
apply (rule nn_integral_PInf_AE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<lambda>x. ennreal (f x) * nn_transfer_operator gp x) \<in> borel_measurable M
 2. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M \<noteq> \<infinity>
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M < \<infinity>

goal (2 subgoals):
 1. (\<lambda>x. ennreal (f x) * nn_transfer_operator gp x) \<in> borel_measurable M
 2. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M \<noteq> \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. ennreal (f x) * nn_transfer_operator gp x \<noteq> \<infinity>

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral> x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) = enn2real (\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gp x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * enn2real (nn_transfer_operator gp x) = enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M)
[PROOF STEP]
by (rule integral_eq_nn_integral) auto
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * enn2real (nn_transfer_operator gp x) = enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * enn2real (nn_transfer_operator gp x) = enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gp x)) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
assume "f x * nn_transfer_operator gp x \<noteq> \<infinity>"
[PROOF STATE]
proof (state)
this:
ennreal (f x) * nn_transfer_operator gp x \<noteq> \<infinity>

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (f x) * nn_transfer_operator gp x \<noteq> \<infinity>
[PROOF STEP]
have "ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x"
[PROOF STATE]
proof (prove)
using this:
ennreal (f x) * nn_transfer_operator gp x \<noteq> \<infinity>

goal (1 subgoal):
 1. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x
[PROOF STEP]
by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
[PROOF STATE]
proof (state)
this:
ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ennreal (f ?x5) * nn_transfer_operator gp ?x5 \<noteq> \<infinity> \<Longrightarrow> ennreal (f ?x5 * enn2real (nn_transfer_operator gp ?x5)) = ennreal (f ?x5) * nn_transfer_operator gp ?x5

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (f ?x5) * nn_transfer_operator gp ?x5 \<noteq> \<infinity> \<Longrightarrow> ennreal (f ?x5 * enn2real (nn_transfer_operator gp ?x5)) = ennreal (f ?x5) * nn_transfer_operator gp ?x5
[PROOF STEP]
have "AE x in M. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x"
[PROOF STATE]
proof (prove)
using this:
ennreal (f ?x5) * nn_transfer_operator gp ?x5 \<noteq> \<infinity> \<Longrightarrow> ennreal (f ?x5 * enn2real (nn_transfer_operator gp ?x5)) = ennreal (f ?x5) * nn_transfer_operator gp ?x5

goal (1 subgoal):
 1. AE x in M. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x
[PROOF STEP]
using gp_fin
[PROOF STATE]
proof (prove)
using this:
ennreal (f ?x5) * nn_transfer_operator gp ?x5 \<noteq> \<infinity> \<Longrightarrow> ennreal (f ?x5 * enn2real (nn_transfer_operator gp ?x5)) = ennreal (f ?x5) * nn_transfer_operator gp ?x5
AE x in M. ennreal (f x) * nn_transfer_operator gp x \<noteq> \<infinity>

goal (1 subgoal):
 1. AE x in M. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x
[PROOF STEP]
have "(\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) = (\<integral>\<^sup>+ x. f x * nn_transfer_operator gp x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
AE x in M. ennreal (f x * enn2real (nn_transfer_operator gp x)) = ennreal (f x) * nn_transfer_operator gp x

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M
[PROOF STEP]
by (rule nn_integral_cong_AE)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
have "... = (\<integral>\<^sup>+ x. f (T x) * gp x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * gp x \<partial>M
[PROOF STEP]
by (rule nn_transfer_operator_intg) (auto simp add: gp_def)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * gp x \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gp x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * gp x \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
have "... = (\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gp x)) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f (T x)) * gp x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M
[PROOF STEP]
by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gp_def)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f (T x)) * gp x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M
[PROOF STEP]
have "(\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gp x)) \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gp x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = (\<integral> x. f (T x) * enn2real(gp x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M) = LINT x|M. f (T x) * enn2real (gp x)
[PROOF STEP]
by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gp_def)
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gp x)) \<partial>M) = LINT x|M. f (T x) * enn2real (gp x)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. f x * enn2real (nn_transfer_operator gp x) = LINT x|M. f (T x) * enn2real (gp x)
[PROOF STEP]
have gp_expr: "(\<integral> x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) = (\<integral> x. f (T x) * enn2real(gp x) \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
LINT x|M. f x * enn2real (nn_transfer_operator gp x) = LINT x|M. f (T x) * enn2real (gp x)

goal (1 subgoal):
 1. LINT x|M. f x * enn2real (nn_transfer_operator gp x) = LINT x|M. f (T x) * enn2real (gp x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * enn2real (nn_transfer_operator gp x) = LINT x|M. f (T x) * enn2real (gp x)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral>\<^sup>+x. f x * nn_transfer_operator gm x \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator h x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
[PROOF STEP]
proof (rule nn_integral_mono_AE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. ennreal (f x) * nn_transfer_operator gm x \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
have "AE x in M. nn_transfer_operator gm x \<le> nn_transfer_operator h x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. nn_transfer_operator gm x \<le> nn_transfer_operator h x
[PROOF STEP]
by (rule nn_transfer_operator_mono) (auto simp add: hgpgm)
[PROOF STATE]
proof (state)
this:
AE x in M. nn_transfer_operator gm x \<le> nn_transfer_operator h x

goal (1 subgoal):
 1. AE x in M. ennreal (f x) * nn_transfer_operator gm x \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. nn_transfer_operator gm x \<le> nn_transfer_operator h x
[PROOF STEP]
show "AE x in M. f x * nn_transfer_operator gm x \<le> f x * nn_transfer_operator h x"
[PROOF STATE]
proof (prove)
using this:
AE x in M. nn_transfer_operator gm x \<le> nn_transfer_operator h x

goal (1 subgoal):
 1. AE x in M. ennreal (f x) * nn_transfer_operator gm x \<le> ennreal (f x) * nn_transfer_operator h x
[PROOF STEP]
by (auto simp: mult_left_mono)
[PROOF STATE]
proof (state)
this:
AE x in M. ennreal (f x) * nn_transfer_operator gm x \<le> ennreal (f x) * nn_transfer_operator h x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
[PROOF STEP]
have a: "(\<integral>\<^sup>+x. f x * nn_transfer_operator gm x \<partial>M) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M < \<infinity>
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator h x \<partial>M < \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M < \<infinity>

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "\<And>x. ennreal(norm(f x * enn2real(nn_transfer_operator gm x))) \<le> f x * nn_transfer_operator gm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<le> ennreal (f x) * nn_transfer_operator gm x
[PROOF STEP]
by (auto simp add: ennreal_mult intro!: mult_left_mono)
       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
[PROOF STATE]
proof (state)
this:
ennreal (norm (f ?x3 * enn2real (nn_transfer_operator gm ?x3))) \<le> ennreal (f ?x3) * nn_transfer_operator gm ?x3

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (norm (f ?x3 * enn2real (nn_transfer_operator gm ?x3))) \<le> ennreal (f ?x3) * nn_transfer_operator gm ?x3
[PROOF STEP]
have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_transfer_operator gm x)) \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_transfer_operator gm x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
ennreal (norm (f ?x3 * enn2real (nn_transfer_operator gm ?x3))) \<le> ennreal (f ?x3) * nn_transfer_operator gm ?x3

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M
[PROOF STEP]
by (simp add: nn_integral_mono)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M
[PROOF STEP]
have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_transfer_operator gm x)) \<partial>M) < \<infinity>"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M < \<infinity>
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M \<le> \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M < \<infinity>

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M < \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M < \<infinity>

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M < \<infinity>
[PROOF STEP]
have gm_int: "integrable M (\<lambda>x. f x * enn2real(nn_transfer_operator gm x))"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (norm (f x * enn2real (nn_transfer_operator gm x))) \<partial>M < \<infinity>

goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * enn2real (nn_transfer_operator gm x))
[PROOF STEP]
by (simp add: integrableI_bounded)
[PROOF STATE]
proof (state)
this:
integrable M (\<lambda>x. f x * enn2real (nn_transfer_operator gm x))

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have gm_fin: "AE x in M. f x * nn_transfer_operator gm x \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. ennreal (f x) * nn_transfer_operator gm x \<noteq> \<infinity>
[PROOF STEP]
apply (rule nn_integral_PInf_AE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<lambda>x. ennreal (f x) * nn_transfer_operator gm x) \<in> borel_measurable M
 2. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M \<noteq> \<infinity>
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M < \<infinity>

goal (2 subgoals):
 1. (\<lambda>x. ennreal (f x) * nn_transfer_operator gm x) \<in> borel_measurable M
 2. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M \<noteq> \<infinity>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. ennreal (f x) * nn_transfer_operator gm x \<noteq> \<infinity>

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral> x. f x * enn2real(nn_transfer_operator gm x) \<partial>M) = enn2real (\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gm x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * enn2real (nn_transfer_operator gm x) = enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M)
[PROOF STEP]
by (rule integral_eq_nn_integral) auto
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * enn2real (nn_transfer_operator gm x) = enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * enn2real (nn_transfer_operator gm x) = enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gm x)) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
assume "f x * nn_transfer_operator gm x \<noteq> \<infinity>"
[PROOF STATE]
proof (state)
this:
ennreal (f x) * nn_transfer_operator gm x \<noteq> \<infinity>

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (f x) * nn_transfer_operator gm x \<noteq> \<infinity>
[PROOF STEP]
have "ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x"
[PROOF STATE]
proof (prove)
using this:
ennreal (f x) * nn_transfer_operator gm x \<noteq> \<infinity>

goal (1 subgoal):
 1. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x
[PROOF STEP]
by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
[PROOF STATE]
proof (state)
this:
ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ennreal (f ?x5) * nn_transfer_operator gm ?x5 \<noteq> \<infinity> \<Longrightarrow> ennreal (f ?x5 * enn2real (nn_transfer_operator gm ?x5)) = ennreal (f ?x5) * nn_transfer_operator gm ?x5

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ennreal (f ?x5) * nn_transfer_operator gm ?x5 \<noteq> \<infinity> \<Longrightarrow> ennreal (f ?x5 * enn2real (nn_transfer_operator gm ?x5)) = ennreal (f ?x5) * nn_transfer_operator gm ?x5
[PROOF STEP]
have "AE x in M. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x"
[PROOF STATE]
proof (prove)
using this:
ennreal (f ?x5) * nn_transfer_operator gm ?x5 \<noteq> \<infinity> \<Longrightarrow> ennreal (f ?x5 * enn2real (nn_transfer_operator gm ?x5)) = ennreal (f ?x5) * nn_transfer_operator gm ?x5

goal (1 subgoal):
 1. AE x in M. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x
[PROOF STEP]
using gm_fin
[PROOF STATE]
proof (prove)
using this:
ennreal (f ?x5) * nn_transfer_operator gm ?x5 \<noteq> \<infinity> \<Longrightarrow> ennreal (f ?x5 * enn2real (nn_transfer_operator gm ?x5)) = ennreal (f ?x5) * nn_transfer_operator gm ?x5
AE x in M. ennreal (f x) * nn_transfer_operator gm x \<noteq> \<infinity>

goal (1 subgoal):
 1. AE x in M. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
AE x in M. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x
[PROOF STEP]
have "(\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gm x) \<partial>M) = (\<integral>\<^sup>+ x. f x * nn_transfer_operator gm x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
AE x in M. ennreal (f x * enn2real (nn_transfer_operator gm x)) = ennreal (f x) * nn_transfer_operator gm x

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M
[PROOF STEP]
by (rule nn_integral_cong_AE)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
have "... = (\<integral>\<^sup>+ x. f (T x) * gm x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * gm x \<partial>M
[PROOF STEP]
by (rule nn_transfer_operator_intg) (auto simp add: gm_def)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * gm x \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x) * nn_transfer_operator gm x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x)) * gm x \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
have "... = (\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gm x)) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f (T x)) * gm x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M
[PROOF STEP]
by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gm_def)
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f (T x)) * gm x \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M
[PROOF STEP]
have "(\<integral>\<^sup>+ x. f x * enn2real(nn_transfer_operator gm x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal(f (T x) * enn2real(gm x)) \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M

goal (1 subgoal):
 1. \<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M = \<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M

goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ x. ennreal (f x * enn2real (nn_transfer_operator gm x)) \<partial>M) = enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = (\<integral> x. f (T x) * enn2real(gm x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M) = LINT x|M. f (T x) * enn2real (gm x)
[PROOF STEP]
by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gm_def)
[PROOF STATE]
proof (state)
this:
enn2real (\<integral>\<^sup>+ x. ennreal (f (T x) * enn2real (gm x)) \<partial>M) = LINT x|M. f (T x) * enn2real (gm x)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. f x * enn2real (nn_transfer_operator gm x) = LINT x|M. f (T x) * enn2real (gm x)
[PROOF STEP]
have gm_expr: "(\<integral> x. f x * enn2real(nn_transfer_operator gm x) \<partial>M) = (\<integral> x. f (T x) * enn2real(gm x) \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
LINT x|M. f x * enn2real (nn_transfer_operator gm x) = LINT x|M. f (T x) * enn2real (gm x)

goal (1 subgoal):
 1. LINT x|M. f x * enn2real (nn_transfer_operator gm x) = LINT x|M. f (T x) * enn2real (gm x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * enn2real (nn_transfer_operator gm x) = LINT x|M. f (T x) * enn2real (gm x)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral> x. f x * enn2real(nn_transfer_operator gp x) - f x * enn2real(nn_transfer_operator gm x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f x * enn2real (nn_transfer_operator gp x) - f x * enn2real (nn_transfer_operator gm x)
[PROOF STEP]
unfolding real_transfer_operator_def gp_def gm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * (enn2real (nn_transfer_operator (\<lambda>x. ennreal (g x)) x) - enn2real (nn_transfer_operator (\<lambda>x. ennreal (- g x)) x)) = LINT x|M. f x * enn2real (nn_transfer_operator (\<lambda>x. ennreal (g x)) x) - f x * enn2real (nn_transfer_operator (\<lambda>x. ennreal (- g x)) x)
[PROOF STEP]
by (simp add: right_diff_distrib)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * real_transfer_operator g x = LINT x|M. f x * enn2real (nn_transfer_operator gp x) - f x * enn2real (nn_transfer_operator gm x)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * real_transfer_operator g x = LINT x|M. f x * enn2real (nn_transfer_operator gp x) - f x * enn2real (nn_transfer_operator gm x)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = (\<integral> x. f x * enn2real(nn_transfer_operator gp x) \<partial>M) - (\<integral> x. f x * enn2real(nn_transfer_operator gm x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * enn2real (nn_transfer_operator gp x) - f x * enn2real (nn_transfer_operator gm x) = (LINT x|M. f x * enn2real (nn_transfer_operator gp x)) - (LINT x|M. f x * enn2real (nn_transfer_operator gm x))
[PROOF STEP]
by (rule Bochner_Integration.integral_diff) (simp_all add: gp_int gm_int)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * enn2real (nn_transfer_operator gp x) - f x * enn2real (nn_transfer_operator gm x) = (LINT x|M. f x * enn2real (nn_transfer_operator gp x)) - (LINT x|M. f x * enn2real (nn_transfer_operator gm x))

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * enn2real (nn_transfer_operator gp x) - f x * enn2real (nn_transfer_operator gm x) = (LINT x|M. f x * enn2real (nn_transfer_operator gp x)) - (LINT x|M. f x * enn2real (nn_transfer_operator gm x))

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = (\<integral> x. f (T x) * enn2real(gp x) \<partial>M) - (\<integral> x. f (T x) * enn2real(gm x) \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. f x * enn2real (nn_transfer_operator gp x)) - (LINT x|M. f x * enn2real (nn_transfer_operator gm x)) = (LINT x|M. f (T x) * enn2real (gp x)) - (LINT x|M. f (T x) * enn2real (gm x))
[PROOF STEP]
using gp_expr gm_expr
[PROOF STATE]
proof (prove)
using this:
LINT x|M. f x * enn2real (nn_transfer_operator gp x) = LINT x|M. f (T x) * enn2real (gp x)
LINT x|M. f x * enn2real (nn_transfer_operator gm x) = LINT x|M. f (T x) * enn2real (gm x)

goal (1 subgoal):
 1. (LINT x|M. f x * enn2real (nn_transfer_operator gp x)) - (LINT x|M. f x * enn2real (nn_transfer_operator gm x)) = (LINT x|M. f (T x) * enn2real (gp x)) - (LINT x|M. f (T x) * enn2real (gm x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LINT x|M. f x * enn2real (nn_transfer_operator gp x)) - (LINT x|M. f x * enn2real (nn_transfer_operator gm x)) = (LINT x|M. f (T x) * enn2real (gp x)) - (LINT x|M. f (T x) * enn2real (gm x))

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. f x * enn2real (nn_transfer_operator gp x)) - (LINT x|M. f x * enn2real (nn_transfer_operator gm x)) = (LINT x|M. f (T x) * enn2real (gp x)) - (LINT x|M. f (T x) * enn2real (gm x))

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = (\<integral> x. f (T x) * max (g x) 0 \<partial>M) - (\<integral> x. f (T x) * max (-g x) 0 \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. f (T x) * enn2real (gp x)) - (LINT x|M. f (T x) * enn2real (gm x)) = (LINT x|M. f (T x) * max (g x) 0) - (LINT x|M. f (T x) * max (- g x) 0)
[PROOF STEP]
using gp_real gm_real
[PROOF STATE]
proof (prove)
using this:
enn2real (gp ?x3) = max (g ?x3) 0
enn2real (gm ?x3) = max (- g ?x3) 0

goal (1 subgoal):
 1. (LINT x|M. f (T x) * enn2real (gp x)) - (LINT x|M. f (T x) * enn2real (gm x)) = (LINT x|M. f (T x) * max (g x) 0) - (LINT x|M. f (T x) * max (- g x) 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(LINT x|M. f (T x) * enn2real (gp x)) - (LINT x|M. f (T x) * enn2real (gm x)) = (LINT x|M. f (T x) * max (g x) 0) - (LINT x|M. f (T x) * max (- g x) 0)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. f (T x) * enn2real (gp x)) - (LINT x|M. f (T x) * enn2real (gm x)) = (LINT x|M. f (T x) * max (g x) 0) - (LINT x|M. f (T x) * max (- g x) 0)

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = (\<integral> x. f (T x) * max (g x) 0 - f (T x) * max (-g x) 0 \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LINT x|M. f (T x) * max (g x) 0) - (LINT x|M. f (T x) * max (- g x) 0) = LINT x|M. f (T x) * max (g x) 0 - f (T x) * max (- g x) 0
[PROOF STEP]
by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2)
[PROOF STATE]
proof (state)
this:
(LINT x|M. f (T x) * max (g x) 0) - (LINT x|M. f (T x) * max (- g x) 0) = LINT x|M. f (T x) * max (g x) 0 - f (T x) * max (- g x) 0

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LINT x|M. f (T x) * max (g x) 0) - (LINT x|M. f (T x) * max (- g x) 0) = LINT x|M. f (T x) * max (g x) 0 - f (T x) * max (- g x) 0

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
have "... = (\<integral>x. f (T x) * g x \<partial>M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f (T x) * max (g x) 0 - f (T x) * max (- g x) 0 = LINT x|M. f (T x) * g x
[PROOF STEP]
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)
[PROOF STATE]
proof (state)
this:
LINT x|M. f (T x) * max (g x) 0 - f (T x) * max (- g x) 0 = LINT x|M. f (T x) * g x

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
show "(\<integral> x. f x * real_transfer_operator g x \<partial>M) = (\<integral>x. f (T x) * g x \<partial>M)"
[PROOF STATE]
proof (prove)
using this:
LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x

goal (1 subgoal):
 1. LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * real_transfer_operator g x = LINT x|M. f (T x) * g x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma atLeastAtMost_nat_numeral:
  "atLeastAtMost m (numeral k :: nat) =
     (if m \<le> numeral k then insert (numeral k) (atLeastAtMost m (pred_numeral k))
                 else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {m..numeral k} = (if m \<le> numeral k then insert (numeral k) {m..pred_numeral k} else {})
[PROOF STEP]
by (simp add: numeral_eq_Suc atLeastAtMostSuc_conv)


[STATEMENT]
lemma cadjoint_univ_prop:
  fixes G :: "'b::chilbert_space \<Rightarrow> 'a::complex_inner"
  assumes a1: \<open>bounded_clinear G\<close>
  shows \<open>cadjoint G x \<bullet>\<^sub>C y = x \<bullet>\<^sub>C G y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cadjoint G x \<bullet>\<^sub>C y = x \<bullet>\<^sub>C G y
[PROOF STEP]
using assms cadjoint_is_cadjoint is_cadjoint_def
[PROOF STATE]
proof (prove)
using this:
bounded_clinear G
bounded_clinear ?G \<Longrightarrow> is_cadjoint (cadjoint ?G) ?G
is_cadjoint ?F ?G = (\<forall>x y. ?F x \<bullet>\<^sub>C y = x \<bullet>\<^sub>C ?G y)

goal (1 subgoal):
 1. cadjoint G x \<bullet>\<^sub>C y = x \<bullet>\<^sub>C G y
[PROOF STEP]
by blast


[STATEMENT]
lemma is_projection_on_insert:
  assumes ortho: "\<And>s. s \<in> S \<Longrightarrow> is_orthogonal a s"
  assumes \<open>is_projection_on \<pi> (closure (cspan S))\<close>
  assumes \<open>is_projection_on \<pi>a (cspan {a})\<close>
  shows "is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))
[PROOF STEP]
from ortho
[PROOF STATE]
proof (chain)
picking this:
?s \<in> S \<Longrightarrow> is_orthogonal a ?s
[PROOF STEP]
have \<open>x \<in> cspan {a} \<Longrightarrow> y \<in> closure (cspan S) \<Longrightarrow> is_orthogonal x y\<close> for x y
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> is_orthogonal a ?s

goal (1 subgoal):
 1. \<lbrakk>x \<in> cspan {a}; y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
using is_orthogonal_cspan is_orthogonal_closure is_orthogonal_sym
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> is_orthogonal a ?s
\<lbrakk>\<And>s. s \<in> ?S \<Longrightarrow> is_orthogonal ?a s; ?x \<in> cspan ?S\<rbrakk> \<Longrightarrow> is_orthogonal ?a ?x
\<lbrakk>\<And>s. s \<in> ?S \<Longrightarrow> is_orthogonal ?a s; ?x \<in> closure ?S\<rbrakk> \<Longrightarrow> is_orthogonal ?a ?x
is_orthogonal ?\<psi> ?\<phi> = is_orthogonal ?\<phi> ?\<psi>

goal (1 subgoal):
 1. \<lbrakk>x \<in> cspan {a}; y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> is_orthogonal x y
[PROOF STEP]
by (smt (verit, ccfv_threshold) empty_iff insert_iff)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> cspan {a}; ?y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> is_orthogonal ?x ?y

goal (1 subgoal):
 1. is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> cspan {a}; ?y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> is_orthogonal ?x ?y
[PROOF STEP]
have \<open>is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (cspan {a} +\<^sub>M closure (cspan S))\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> cspan {a}; ?y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> is_orthogonal ?x ?y

goal (1 subgoal):
 1. is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (cspan {a} +\<^sub>M closure (cspan S))
[PROOF STEP]
apply (rule is_projection_on_plus)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> cspan {a}; y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> x \<in> cspan {a}
 2. \<And>x y. \<lbrakk>x \<in> cspan {a}; y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> y \<in> closure (cspan S)
 3. closed_csubspace (cspan {a})
 4. closed_csubspace (closure (cspan S))
 5. is_projection_on \<pi>a (cspan {a})
 6. is_projection_on \<pi> (closure (cspan S))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> is_orthogonal a ?s
is_projection_on \<pi> (closure (cspan S))
is_projection_on \<pi>a (cspan {a})

goal (6 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> cspan {a}; y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> x \<in> cspan {a}
 2. \<And>x y. \<lbrakk>x \<in> cspan {a}; y \<in> closure (cspan S)\<rbrakk> \<Longrightarrow> y \<in> closure (cspan S)
 3. closed_csubspace (cspan {a})
 4. closed_csubspace (closure (cspan S))
 5. is_projection_on \<pi>a (cspan {a})
 6. is_projection_on \<pi> (closure (cspan S))
[PROOF STEP]
by (auto simp add: closed_csubspace.intro)
[PROOF STATE]
proof (state)
this:
is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (cspan {a} +\<^sub>M closure (cspan S))

goal (1 subgoal):
 1. is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (cspan {a} +\<^sub>M closure (cspan S))

goal (1 subgoal):
 1. is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))
[PROOF STEP]
have \<open>\<dots> = closure (cspan (insert a S))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cspan {a} +\<^sub>M closure (cspan S) = closure (cspan (insert a S))
[PROOF STEP]
using closed_sum_cspan[where X=\<open>{a}\<close>]
[PROOF STATE]
proof (prove)
using this:
cspan {a} +\<^sub>M cspan ?Y = closure (cspan ({a} \<union> ?Y))

goal (1 subgoal):
 1. cspan {a} +\<^sub>M closure (cspan S) = closure (cspan (insert a S))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cspan {a} +\<^sub>M closure (cspan S) = closure (cspan (insert a S))

goal (1 subgoal):
 1. is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))

goal (1 subgoal):
 1. is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
is_projection_on (\<lambda>x. \<pi>a x + \<pi> x) (closure (cspan (insert a S)))

goal:
No subgoals!
[PROOF STEP]
qed