[STATEMENT]
lemma EM_remainder_converges_of_real_iff:
  fixes f :: "real \<Rightarrow> real"
  assumes "continuous_on {of_int a..} f"
  shows   "EM_remainder_converges n (\<lambda>x. of_real (f x) :: 
            'a :: {banach, real_normed_algebra_1, real_inner}) a \<longleftrightarrow> EM_remainder_converges n f a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a = EM_remainder_converges n f a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a \<Longrightarrow> EM_remainder_converges n f a
 2. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
assume "EM_remainder_converges n (\<lambda>x. of_real (f x) :: 'a) a"
[PROOF STATE]
proof (state)
this:
EM_remainder_converges n (\<lambda>x. of_real (f x)) a

goal (2 subgoals):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a \<Longrightarrow> EM_remainder_converges n f a
 2. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
obtain L :: 'a
    where L: "((\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x)) (of_int a) (of_int b)) \<longlongrightarrow> L) at_top"
[PROOF STATE]
proof (prove)
using this:
EM_remainder_converges n (\<lambda>x. of_real (f x)) a

goal (1 subgoal):
 1. (\<And>L. ((\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b)) \<longlongrightarrow> L) at_top \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: EM_remainder_converges_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b)) \<longlongrightarrow> L) at_top

goal (2 subgoals):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a \<Longrightarrow> EM_remainder_converges n f a
 2. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
have "((\<lambda>b. EM_remainder' n f (of_int a) (of_int b)) \<longlongrightarrow> L \<bullet> 1) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>b. EM_remainder' n f (real_of_int a) (real_of_int b)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top
[PROOF STEP]
proof (rule Lim_transform_eventually)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (?f \<longlongrightarrow> L \<bullet> (1::'a)) at_top
 2. \<forall>\<^sub>F x in at_top. ?f x = EM_remainder' n f (real_of_int a) (real_of_int x)
[PROOF STEP]
show "eventually (\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x) :: 'a) (of_int a) (of_int b) \<bullet> 1 =
            EM_remainder' n f (of_int a) (of_int b)) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F b in at_top. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b) \<bullet> (1::'a) = EM_remainder' n f (real_of_int a) (real_of_int b)
[PROOF STEP]
using eventually_ge_at_top[of a]
[PROOF STATE]
proof (prove)
using this:
eventually ((\<le>) a) at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F b in at_top. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b) \<bullet> (1::'a) = EM_remainder' n f (real_of_int a) (real_of_int b)
[PROOF STEP]
by eventually_elim
         (subst EM_remainder'_bounded_linear [OF bounded_linear_of_real],
          auto intro!: continuous_on_subset[OF assms])
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F b in at_top. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b) \<bullet> (1::'a) = EM_remainder' n f (real_of_int a) (real_of_int b)

goal (1 subgoal):
 1. ((\<lambda>b. EM_remainder' n (\<lambda>x. of_real (f x)) (real_of_int a) (real_of_int b) \<bullet> (1::'a)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top
[PROOF STEP]
qed (intro tendsto_intros L)
[PROOF STATE]
proof (state)
this:
((\<lambda>b. EM_remainder' n f (real_of_int a) (real_of_int b)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top

goal (2 subgoals):
 1. EM_remainder_converges n (\<lambda>x. of_real (f x)) a \<Longrightarrow> EM_remainder_converges n f a
 2. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
thus "EM_remainder_converges n f a"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>b. EM_remainder' n f (real_of_int a) (real_of_int b)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top

goal (1 subgoal):
 1. EM_remainder_converges n f a
[PROOF STEP]
unfolding EM_remainder_converges_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>b. EM_remainder' n f (real_of_int a) (real_of_int b)) \<longlongrightarrow> L \<bullet> (1::'a)) at_top

goal (1 subgoal):
 1. \<exists>L. ((\<lambda>x. EM_remainder' n f (real_of_int a) (real_of_int x)) \<longlongrightarrow> L) at_top
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
EM_remainder_converges n f a

goal (1 subgoal):
 1. EM_remainder_converges n f a \<Longrightarrow> EM_remainder_converges n (\<lambda>x. of_real (f x)) a
[PROOF STEP]
qed (intro EM_remainder_converges_of_real assms)