[STATEMENT]
lemma real_transfer_operator_mono:
  assumes "AE x in M. f x \<le> g x" and [measurable]: "integrable M f" "integrable M g"
  shows "AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
have "AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x
[PROOF STEP]
by (rule AE_symmetric[OF real_transfer_operator_diff], auto simp add: assms)
[PROOF STATE]
proof (state)
this:
AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
have "AE x in M. real_transfer_operator (\<lambda>x. g x - f x) x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. 0 \<le> real_transfer_operator (\<lambda>x. g x - f x) x
[PROOF STEP]
by (rule real_transfer_operator_pos, auto simp add: assms(1))
[PROOF STATE]
proof (state)
this:
AE x in M. 0 \<le> real_transfer_operator (\<lambda>x. g x - f x) x

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x
AE x in M. 0 \<le> real_transfer_operator (\<lambda>x. g x - f x) x
[PROOF STEP]
have "AE x in M. real_transfer_operator g x - real_transfer_operator f x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
AE x in M. real_transfer_operator g x - real_transfer_operator f x = real_transfer_operator (\<lambda>x. g x - f x) x
AE x in M. 0 \<le> real_transfer_operator (\<lambda>x. g x - f x) x

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

goal (1 subgoal):
 1. AE x in M. real_transfer_operator f x \<le> real_transfer_operator g x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AE x in M. 0 \<le> real_transfer_operator g x - real_transfer_operator f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
AE x in M. 0 \<le> real_transfer_operator g x - real_transfer_operator f x

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

goal:
No subgoals!
[PROOF STEP]
qed