Fixed_Point_Method.thy

section \<open>Fixed Point Method\<close>

theory Fixed_Point_Method
  imports "ITree_Numeric_VCG.ITree_Numeric_VCG" Complex_Main Taylor_Peano
begin

subsection \<open>Contractive Map Facts\<close>

lemma contractive_deriv_bound_closed:
  fixes B :: real
  assumes C1:   "C_k_on 1 f U"
      and zU:   "z \<in> U"
      and Dz_lt: "\<bar>deriv f z\<bar> < B"
  shows "\<exists>\<epsilon>>0. \<exists>\<delta>>0.
           {z - \<delta> .. z + \<delta>} \<subseteq> U \<and>
           (\<forall>x \<in> {z - \<delta> .. z + \<delta>}. \<bar>deriv f x\<bar> \<le> B - \<epsilon>)"
proof -
  (* U contains a closed interval around z *)
  obtain \<nu> where \<nu>_pos: "\<nu> > 0" and \<nu>_in: "{z - \<nu> .. z + \<nu>} \<subseteq> U"
    by (metis C_k_on_def C1 zU cball_eq_atLeastAtMost open_contains_cball_eq)

  (* pick a positive margin \<epsilon> from the headroom B - |f'(z)| *)
  obtain \<epsilon> where \<epsilon>_def: "\<epsilon> = (B - \<bar>deriv f z\<bar>) / 2" and \<epsilon>_pos: "\<epsilon> > 0"
    using Dz_lt by fastforce

  (* continuity of the derivative at z *)
  have cont_on: "continuous_on U (deriv f)"
    using C1_cont_diff C1 by blast
  have cont_at: "continuous (at z) (deriv f)"
    using cont_on C1 zU by (simp add: C_k_on_def continuous_on_eq_continuous_at)
  then have "\<forall> \<epsilon> > 0. \<exists> \<delta> > 0.  \<forall>x. \<bar>x - z\<bar> < \<delta> \<longrightarrow> \<bar>deriv f x - deriv f z\<bar> < \<epsilon>"
    using continuous_at_eps_delta by blast

  then obtain \<delta>1 where \<delta>1_pos: "\<delta>1 > 0"
    and near: "\<forall>x. \<bar>x - z\<bar> < \<delta>1 \<longrightarrow> \<bar>deriv f x - deriv f z\<bar> < \<epsilon>"
    by (meson \<epsilon>_pos)

  (* choose a closed radius strictly inside the continuity radius *)
  define \<delta> where "\<delta> = min \<nu> (\<delta>1 / 2)"
  have \<delta>_pos: "\<delta> > 0" using \<nu>_pos \<delta>1_pos by (simp add: \<delta>_def)
  have \<delta>_le_\<nu>: "\<delta> \<le> \<nu>" by (simp add: \<delta>_def)
  have \<delta>_lt_\<delta>1: "\<delta> < \<delta>1" using \<delta>1_pos by (simp add: \<delta>_def)

  (* closed interval is inside U *)
  have subsetU: "{z - \<delta> .. z + \<delta>} \<subseteq> U"
    using \<nu>_in \<delta>_le_\<nu> by auto

  (* on the closed interval we still have the strict continuity bound *)
  have bound_strict:
    "\<forall>x \<in> {z - \<delta> .. z + \<delta>}. \<bar>deriv f x - deriv f z\<bar> < \<epsilon>"
  proof
    fix x assume xI: "x \<in> {z - \<delta> .. z + \<delta>}"
    have "\<bar>x - z\<bar> \<le> \<delta>" using xI by (simp add: abs_le_iff)
    hence "\<bar>x - z\<bar> < \<delta>1" using \<delta>_lt_\<delta>1 by linarith
    thus "\<bar>deriv f x - deriv f z\<bar> < \<epsilon>" using near by simp
  qed

  (* triangle inequality gives the uniform derivative bound on the closed interval *)
  have bound_closed:
    "\<forall>x \<in> {z - \<delta> .. z + \<delta>}. \<bar>deriv f x\<bar> \<le> B - \<epsilon>"
  proof
    fix x assume xI: "x \<in> {z - \<delta> .. z + \<delta>}"
    have "\<bar>deriv f x\<bar> \<le> \<bar>deriv f z\<bar> + \<bar>deriv f x - deriv f z\<bar>"
      by (simp add: abs_triangle_ineq4)
    also have "\<dots> < \<bar>deriv f z\<bar> + \<epsilon>"
      using bound_strict xI by simp
    also have "\<dots> = \<bar>deriv f z\<bar> + (B - \<bar>deriv f z\<bar>)/2"
      by (simp add: \<epsilon>_def)
    also have "\<dots> = B - \<epsilon>"
      by (smt (z3) \<epsilon>_def field_sum_of_halves)
    finally show "\<bar>deriv f x\<bar> \<le> B - \<epsilon>" by (rule less_imp_le)
  qed
  show ?thesis
    by (intro exI[of _ \<epsilon>] exI[of _ \<delta>] conjI \<epsilon>_pos conjI \<delta>_pos conjI subsetU bound_closed)
qed

corollary contractive_deriv_bound:
  fixes B :: real
  assumes "C_k_on 1 f U"
  assumes "z \<in> U"
  assumes "\<bar>deriv f z\<bar> < B"
  shows "\<exists> \<epsilon> > 0. \<exists>\<delta> > 0. ({z - \<delta> <..< z + \<delta>} \<subseteq> U) \<and> (\<forall> x \<in> {z - \<delta> <..< z + \<delta>}. \<bar>deriv f x\<bar> < B - \<epsilon>)"
proof - 
  from assms have "\<exists>\<epsilon>>0. \<exists>\<delta>>0.
           {z - \<delta> .. z + \<delta>} \<subseteq> U \<and>
           (\<forall>x \<in> {z - \<delta> .. z + \<delta>}. \<bar>deriv f x\<bar> \<le> B - \<epsilon>)"
    by(rule contractive_deriv_bound_closed)
  then obtain \<epsilon>0 \<delta>0 where \<epsilon>0: "\<epsilon>0 > 0" and \<delta>0: "\<delta>0 > 0"
      and sub: "{z - \<delta>0 .. z + \<delta>0} \<subseteq> U"
      and bd:  "\<forall>x\<in>{z - \<delta>0 .. z + \<delta>0}. \<bar>deriv f x\<bar> \<le> B - \<epsilon>0"
    by meson

  define \<epsilon> where "\<epsilon> = \<epsilon>0 / 2"
  define \<delta> where "\<delta> = \<delta>0"
  have "\<epsilon> > 0" by (simp add: \<epsilon>_def \<epsilon>0)
  have "\<delta> > 0" by (simp add: \<delta>_def \<delta>0)
  have open_sub: "{z - \<delta><..<z + \<delta>} \<subseteq> U"
    using \<delta>_def atLeastAtMost_eq_cball ball_subset_cball greaterThanLessThan_eq_ball sub by blast

  have bound_open: "\<forall>x\<in>{z - \<delta><..<z + \<delta>}. \<bar>deriv f x\<bar> < B - \<epsilon>"
  proof
    fix x assume "x \<in> {z - \<delta><..<z + \<delta>}"
    hence x_closed: "x \<in> {z - \<delta>0 .. z + \<delta>0}" by (simp add: \<delta>_def)
    have "\<bar>deriv f x\<bar> \<le> B - \<epsilon>0" using bd x_closed by blast
    moreover have "B - \<epsilon>0 < B - \<epsilon>"
      by (simp add: \<epsilon>0 \<epsilon>_def) 

    ultimately show "\<bar>deriv f x\<bar> < B - \<epsilon>" by linarith
  qed
  show ?thesis
    using \<delta>0 \<delta>_def \<open>0 < \<epsilon>\<close> bound_open open_sub by blast
qed

corollary contractive_deriv_imp_contra_closed:
  fixes B :: real
  assumes "C_k_on 1 f U"
      and "z \<in> U"
      and "\<bar>deriv f z\<bar> < B"
  shows "\<exists>\<epsilon> > 0. \<exists>\<delta> > 0.
           ((\<epsilon> < B) \<and> {z - \<delta> .. z + \<delta>} \<subseteq> U) \<and>
           (\<forall>x y. (x \<in> {z - \<delta> .. z + \<delta>} \<and> y \<in> {x .. z + \<delta>})
                \<longrightarrow> \<bar>f x - f y\<bar> \<le> (B - \<epsilon>) * \<bar>x - y\<bar>)"
proof -
  from contractive_deriv_bound_closed[OF assms]
  obtain \<epsilon>0 \<delta> where \<epsilon>0_pos: "\<epsilon>0 > 0" and \<delta>_pos: "\<delta> > 0"
    and subset: "{z - \<delta> .. z + \<delta>} \<subseteq> U"
    and dBd: "\<forall>x \<in> {z - \<delta> .. z + \<delta>}. \<bar>deriv f x\<bar> \<le> B - \<epsilon>0"
    by blast
  define \<epsilon> where "\<epsilon> = min \<epsilon>0 (B/2)"
  have \<epsilon>_pos: "\<epsilon> > 0"
    using \<epsilon>0_pos assms(3) by (simp add: \<epsilon>_def half_gt_zero_iff less_imp_le)
  have \<epsilon>_lt_B: "\<epsilon> < B"
    using \<epsilon>_def \<epsilon>_pos by linarith

  have mvt:
    "\<forall>x y. (x \<in> {z - \<delta> .. z + \<delta>} \<and> y \<in> {x .. z + \<delta>})
           \<longrightarrow> \<bar>f x - f y\<bar> \<le> (B - \<epsilon>) * \<bar>x - y\<bar>"
  proof clarify
    fix x y :: real
    assume x_in: "x \<in> {z - \<delta> .. z + \<delta>}" and y_in: "y \<in> {x .. z + \<delta>}"
    show "\<bar>f x - f y\<bar> \<le> (B - \<epsilon>) * \<bar>x - y\<bar>"
    proof (cases "x = y")
      case True  show ?thesis by (simp add: True)
    next
      case False
      hence x_lt_y: "x < y"
        using less_eq_real_def y_in by presburger 
      have "\<exists>t>x. t < y \<and> f y - f x = (y - x) * deriv f t"
      proof (rule MVT2[where a = x and b = y and f = f and f' = "deriv f"])
        fix t assume "x \<le> t" "t \<le> y"
        hence "t \<in> {z - \<delta> .. z + \<delta>}" using x_in y_in by auto
        then have "t \<in> U" using subset by blast
        thus "(f has_real_derivative deriv f t) (at t)"
          using C1_cont_diff assms(1) by blast
      qed (use x_lt_y in auto)
      then obtain \<theta> where \<theta>_in: "\<theta> \<in> {x <..< y}"
                        and \<theta>_eq: "f y - f x = (y - x) * deriv f \<theta>"
        by auto

      have \<theta>_closed: "\<theta> \<in> {z - \<delta> .. z + \<delta>}" using x_in y_in \<theta>_in by auto
      have "\<bar>deriv f \<theta>\<bar> \<le> B - \<epsilon>0" using dBd \<theta>_closed by blast
      also have "\<dots> \<le> B - \<epsilon>" by (simp add: \<epsilon>_def)
      finally have "\<bar>deriv f \<theta>\<bar> \<le> B - \<epsilon>".
      thus "\<bar>f x - f y\<bar> \<le> (B - \<epsilon>) * \<bar>x - y\<bar>"
        by (smt (z3) \<theta>_eq mult.commute mult_left_mono mult_minus_right) 
    qed
  qed
  show ?thesis
    using \<epsilon>_pos \<delta>_pos \<epsilon>_lt_B subset mvt by blast
qed

corollary contractive_deriv_imp_contra:
  fixes B :: real
  assumes "C_k_on 1 f U"
  assumes "z \<in> U"
  assumes "\<bar>deriv f z\<bar> < B"
  shows "\<exists>\<epsilon> > 0. \<exists>\<delta> > 0.
           ((\<epsilon> < B) \<and> {z - \<delta> <..< z + \<delta>} \<subseteq> U) \<and>
           (\<forall>x y. (x \<in> {z - \<delta> <..< z + \<delta>} \<and> y \<in> {x <..< z + \<delta>})
                \<longrightarrow> \<bar>f x - f y\<bar> < (B - \<epsilon>) * \<bar>x - y\<bar>)"
proof -
  from contractive_deriv_bound[OF assms] obtain \<epsilon> \<delta>
    where \<epsilon>_pos: "\<epsilon> > 0" and \<delta>_pos: "\<delta> > 0"
      and bound:   "\<forall>x \<in> {z - \<delta> <..< z + \<delta>}. \<bar>deriv f x\<bar> < B - \<epsilon>"
      and subset': "{z - \<delta> <..< z + \<delta>} \<subseteq> U"
    by auto
  then have \<epsilon>_lt_B: "\<epsilon> < B"
    by (smt (verit) dist_real_def field_sum_of_halves greaterThanLessThan_eq_ball mem_ball)

  have mvt:
    "\<forall>x y. (x \<in> {z - \<delta> <..< z + \<delta>} \<and> y \<in> {x <..< z + \<delta>})
           \<longrightarrow> \<bar>f x - f y\<bar> < (B - \<epsilon>) * \<bar>x - y\<bar>"
  proof clarify
    fix x y :: real
    assume x_in: "x \<in> {z - \<delta> <..< z + \<delta>}" and y_in: "y \<in> {x <..< z + \<delta>}"
    then have x_lt_y: "x < y"
      by (meson greaterThanLessThan_iff)
    then have "\<exists>t>x. t < y \<and> f y - f x = (y - x) * deriv f t"
    proof (rule MVT2[where a = x and b = y and f = f and f' = "deriv f"])
      fix t
      assume "x \<le> t" and "t \<le> y"
      hence "t \<in> {z - \<delta> <..< z + \<delta>}"
        using x_in y_in by auto
      then have "t \<in> U"
        using subset' by blast
      then show "(f has_real_derivative deriv f t) (at t)"
        using C1_cont_diff assms(1) by fast
    qed    
    then obtain \<theta> where \<theta>_in: "\<theta> \<in> {x <..< y}"
                     and \<theta>_eq: "f x - f y = (deriv f \<theta>) * (x - y)"
      by (metis add_0 cross3_simps(11,54) diff_diff_eq2 greaterThanLessThan_iff)
    have "\<theta> \<in> {z - \<delta> <..< z + \<delta>}"
      using x_in y_in \<theta>_in by auto
    then have "\<bar>deriv f \<theta>\<bar> < B - \<epsilon>"
      using bound by blast
    then show "\<bar>f x - f y\<bar> < (B - \<epsilon>) * \<bar>x - y\<bar>"
      using \<theta>_eq x_lt_y by (simp add: abs_mult)
  qed
  then show ?thesis
    using \<epsilon>_pos \<delta>_pos \<epsilon>_lt_B subset' by blast
qed



lemma contraction_ball_closure:
  fixes f :: "real \<Rightarrow> real" and r c \<delta> :: real
  assumes fr:      "f r = r"
    and contr:    "\<forall>s t. \<bar>s - r\<bar> < \<delta> \<longrightarrow> \<bar>t - r\<bar> < \<delta> \<longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>"
    and c_bound: "0 \<le> c \<and> c < 1"
  shows "\<forall>n x. \<bar>x - r\<bar> < \<delta> \<longrightarrow> \<bar>(f ^^ n) x - r\<bar> < \<delta>"
proof (clarify)
  fix n :: nat and x :: real
  assume H: "\<bar>x - r\<bar> < \<delta>"
  show "\<bar>(f ^^ n) x - r\<bar> < \<delta>"
  proof (induct n)
    show "\<bar>(f ^^ 0) x - r\<bar> < \<delta>"
      by (simp add: H) 
  next
    case (Suc k)
    then have IH: "\<bar>(f ^^ k) x - r\<bar> < \<delta>"
     by auto 
    have "\<bar>(f ^^ Suc k) x - r\<bar> = \<bar>f ((f ^^ k) x) - r\<bar>"
      by simp
    also have "\<dots> = \<bar>f ((f ^^ k) x) - f r\<bar>"
      using fr by simp
    also have "\<dots> \<le> c * \<bar>(f ^^ k) x - r\<bar>"
      using IH assms(2) by auto
    also have "\<dots> < \<delta>"
      by (smt (verit, best) Suc.hyps c_bound mult_left_le_one_le)
    finally show ?case.
  qed
qed

corollary contraction_ball_closure':
  fixes f :: "real \<Rightarrow> real" and r \<delta> \<delta>0 \<epsilon> :: real
  assumes order_bound:
      "\<forall>x y. x \<in> {r - \<delta>0<..<r + \<delta>0} \<longrightarrow> y \<in> {x<..<r + \<delta>0}
             \<longrightarrow> \<bar>f x - f y\<bar> < (1 - \<epsilon>) * \<bar>x - y\<bar>"
    and \<epsilon>_pos : "0 < \<epsilon>"
    and \<delta>_pos : "0 < \<delta>" and \<delta>_le: "\<delta> \<le> \<delta>0"
  shows "\<forall>s t. s \<noteq> t \<longrightarrow> \<bar>s - r\<bar> < \<delta> \<longrightarrow> \<bar>t - r\<bar> < \<delta>
               \<longrightarrow> \<bar>f s - f t\<bar> < (1 - \<epsilon>) * \<bar>s - t\<bar>"
proof (clarify)
  fix s t :: real
  assume s_neq: "s \<noteq> t"
     and sb:    "\<bar>s - r\<bar> < \<delta>"
     and tb:    "\<bar>t - r\<bar> < \<delta>"
  have s_in: "s \<in> {r - \<delta>0<..<r + \<delta>0}"
    using \<delta>_le dist_real_def sb by auto
  have t_in: "t \<in> {r - \<delta>0<..<r + \<delta>0}"
    using \<delta>_le dist_real_def tb by force
  show "\<bar>f s - f t\<bar> < (1 - \<epsilon>) * \<bar>s - t\<bar>"
  proof (cases "s < t")
    case True
    hence "t \<in> {s<..<r + \<delta>0}"
      using t_in by simp
    thus "\<bar>f s - f t\<bar> < (1 - \<epsilon>) * \<bar>s - t\<bar>"
      using order_bound s_in by blast
  next
    case False
    hence "t < s" 
      using s_neq by auto
    hence "s \<in> {t<..<r + \<delta>0}"
      using s_in by simp
    thus "\<bar>f s - f t\<bar> < (1 - \<epsilon>) * \<bar>s - t\<bar>"
      by (metis abs_minus_commute assms(1) t_in)     
  qed
qed

lemma contraction_cball_closure:
  fixes f :: "real \<Rightarrow> real" and r c \<delta> :: real
  assumes fr: "f r = r"
      and lips_cball: "\<And>s t. \<bar>s - r\<bar> \<le> \<delta> \<Longrightarrow> \<bar>t - r\<bar> \<le> \<delta> \<Longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>"
      and c_ge0: "0 \<le> c" and c_lt1: "c < 1"
  shows "\<forall>n x. \<bar>x - r\<bar> \<le> \<delta> \<longrightarrow> \<bar>(f ^^ n) x - r\<bar> \<le> \<delta>"
proof (intro allI impI)
  fix n x assume "\<bar>x - r\<bar> \<le> \<delta>"
  then show "\<bar>(f ^^ n) x - r\<bar> \<le> \<delta>"
  proof (induction n arbitrary: x)
    case 0 show ?case
      by (simp add: "0.prems")
  next
    case (Suc n x)
    have "\<bar>(f ^^ Suc n) x - r\<bar> = \<bar>f ((f ^^ n) x) - f r\<bar>"
      by (simp add: assms(1)) 
    also have "\<dots> \<le> c * \<bar>(f ^^ n) x - r\<bar>"
      using lips_cball Suc.IH Suc(2) by force 
    also have "\<dots> \<le> \<bar>(f ^^ n) x - r\<bar>"
      using c_ge0
      by (meson abs_ge_zero c_lt1 less_eq_real_def mult_left_le_one_le) 
    also have "\<dots> \<le> \<delta>" using Suc.IH Suc(2) by blast 
    finally show ?case.
  qed
qed

lemma inv_cball_of_budget:
  fixes f :: "real \<Rightarrow> real" and x0 R c :: real
  assumes "0 \<le> c" "c < 1" "R \<ge> 0"
      and lips:   "\<And>s t. \<bar>s - x0\<bar> \<le> R \<Longrightarrow> \<bar>t - x0\<bar> \<le> R \<Longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>"
      and budget: "\<bar>f x0 - x0\<bar> \<le> (1 - c) * R"
  shows "f ` cball x0 R \<subseteq> cball x0 R"
proof
  fix y 
  assume "y \<in> f ` cball x0 R"
  then obtain s where sB: "s \<in> cball x0 R" and y: "y = f s" by auto
  have "\<bar>y - x0\<bar> = \<bar>f s - x0\<bar>"
    by (simp add: norm_triangle_ineq4 y)
  also have "\<dots> \<le> \<bar>f s - f x0\<bar> + \<bar>f x0 - x0\<bar>"
    by simp
  also have "\<dots> \<le> c * \<bar>s - x0\<bar> + (1 - c) * R"
    by (smt (verit) assms(4,5) dist_real_def mem_cball sB) 
  also have "\<dots> \<le> c * R + (1 - c) * R"
    by (smt (verit, best) assms(1) dist_real_def mem_cball mult_left_mono sB)
  also have "\<dots> \<le>  R"
    by argo
  finally show "y \<in> cball x0 R"
    by (simp add: dist_real_def) 
qed

subsection \<open>Algorithm\<close>

zstore state = lvstore +
  x :: "real"
  fx :: "real"
  f'x :: "real"
  gx :: "real"
  x_new :: "real"
  itr :: "nat"
  Break :: "nat"

program fixed_point_iter "(f :: real \<Rightarrow> real, x\<^sub>0 :: real, tol :: real, max_iter :: nat)" over state
  = "x := x\<^sub>0; x_new := f x; itr := 0; Break :=0;
  while (itr < max_iter \<and> Break = 0)
    invariant itr \<le> max_iter
 \<and> x            = (f ^^ itr) x\<^sub>0
 \<and> x_new        = f x
 \<and> (Break \<noteq> 0 \<longrightarrow> \<bar>x_new - x\<bar> < tol)      
    variant max_iter - itr
  do
    if \<bar>x_new - x\<bar> < tol then Break := 1
    fi;
    x := x_new; x_new := f x; itr := itr + 1
  od"

execute "fixed_point_iter(\<lambda> x. x*x, 0.5, 0.1, 4)"
\<comment> \<open>This program terminates after 3 iterations with an estimate of the fixed point \(0\),
     namely \(0.0000152587890625), when starting from \(0.5\), within an error tolerance
     of \(0.1\).\<close>

execute "fixed_point_iter(\<lambda> x. 0.5*(3/x + x), 1, 0.0001, 10)"
\<comment> \<open>This program calculates the square root of 3\<close>

subsection \<open>Total Correctness Proofs\<close>

\<comment> \<open>This next lemma captures the standard local contraction argument behind fixed-point
   iteration. Under the assumptions (a fixed point \(f\,r = r\), a local
   contraction with constant \(0 \le c < 1\) on the ball \(\{x \mid |x-r| < \delta\}\),
   and an initial point \(x_0\) inside that ball), the Hoare triple asserts the
   quantitative error bound
   \[
     |x - r| \;\le\; c^{\mathit{itr}}\,|x_0 - r|
   \]
   at the end of the program. Intuitively, setting \(t = r\) in the contractive
   hypothesis yields \(|f(s) - r| \le c\,|s - r|\), so each iteration shrinks the
   distance to \(r\) by a factor \(c\); an \(itr\)-step induction gives the stated
   geometric rate.

   The result is *local*: no global properties of \(f\) are required—only
   contractivity in a neighborhood of \(r\). In particular, the bound also
   implies that all iterates remain inside the \(\delta\)-ball around \(r\),
   since \( |x_k - r| \le c^k |x_0 - r| < |x_0 - r| < \delta\).\<close>

lemma fixed_point_known_iter_error_bound_local_cball:
  fixes f       :: "real \<Rightarrow> real" 
  and r x\<^sub>0 c \<delta> :: real and max_iter :: nat
  assumes c_nonneg:  "0 \<le> c"
      and c_strict:  "c < 1"
      and \<delta>_ge0:     "0 \<le> \<delta>"
      and r_fixed:   "f r = r"
      and x0_in:     "\<bar>x\<^sub>0 - r\<bar> \<le> \<delta>"
      and lips_cball:"\<And>s t. \<bar>s - r\<bar> \<le> \<delta> \<Longrightarrow> \<bar>t - r\<bar> \<le> \<delta> \<Longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>"
  shows
  "H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter)
     [\<bar>x - r\<bar> \<le> c ^ itr * \<bar>x\<^sub>0 - r\<bar> \<and> itr \<le> max_iter]"
proof(vcg)
  fix itr :: nat
  assume step_small:  "\<bar>f ((f ^^ itr) x\<^sub>0) - (f ^^ itr) x\<^sub>0\<bar> < tol"
  assume below_max: "itr < max_iter"

  from assms have t_in_ball: "\<bar>(f ^^ itr) x\<^sub>0 - r\<bar> \<le> \<delta>"
    by (subst contraction_cball_closure, simp_all)
  then have s_in_ball: "\<bar>f ((f ^^ itr) x\<^sub>0) - r\<bar> \<le> \<delta>"
    by (smt (verit) assms(4,6) c_strict mult_less_cancel_right2)

  have step_bound:
    "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> \<le> c * \<bar>f ((f ^^ itr) x\<^sub>0) - (f ^^ itr) x\<^sub>0\<bar>"
    using assms(6) s_in_ball t_in_ball by presburger
  also have "... < tol"
    using c_strict
    by (meson abs_not_less_zero mult_le_cancel_right2 not_less not_less_iff_gr_or_eq order_trans_rules(21) step_small)

  finally show "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> < tol".
  then show "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> < tol".  (*Get one goal for free*)
next
 show "\<bar>(f ^^ max_iter) x\<^sub>0 - r\<bar> \<le> c ^ max_iter * \<bar>x\<^sub>0 - r\<bar>"
  proof (induction max_iter)
    show "\<bar>(f ^^ 0) x\<^sub>0 - r\<bar> \<le> c ^ 0 * \<bar>x\<^sub>0 - r\<bar>"
      by simp
  next
    case (Suc n)    
    have step: "\<bar>(f ^^ Suc n) x\<^sub>0 - r\<bar> = \<bar>f ((f ^^ n) x\<^sub>0) - r\<bar>"
      by simp
    also have "\<dots> = \<bar>f ((f ^^ n) x\<^sub>0) - f r\<bar>"
      using r_fixed by presburger
    also have "\<dots> \<le> c * \<bar>(f ^^ n) x\<^sub>0 - r\<bar>"
      by (smt (verit, ccfv_SIG) Suc.IH assms(1) assms(5) assms(6) c_strict mult_left_le_one_le power_le_one zero_le_power)    
    also have "\<dots> \<le> c * (c ^ n * \<bar>x\<^sub>0 - r\<bar>)"
      by (meson Suc.IH assms(1) mult_left_mono)
    also have "\<dots> = c ^ Suc n * \<bar>x\<^sub>0 - r\<bar>"
      by simp
    finally show ?case.
  qed
  then show "\<bar>(f ^^ max_iter) x\<^sub>0 - r\<bar> \<le> c ^ max_iter * \<bar>x\<^sub>0 - r\<bar>"
    by simp
next
  fix itr Break :: nat    
  show "\<bar>(f ^^ itr) x\<^sub>0 - r\<bar> \<le> c ^ itr * \<bar>x\<^sub>0 - r\<bar>"
  proof (induction itr)
    show "\<bar>(f ^^ 0) x\<^sub>0 - r\<bar> \<le> c ^ 0 * \<bar>x\<^sub>0 - r\<bar>"
      by simp
  next
    fix itr 
    assume IH: "\<bar>(f ^^ itr) x\<^sub>0 - r\<bar> \<le> c ^ itr * \<bar>x\<^sub>0 - r\<bar>"   
    have "\<bar>(f ^^ Suc itr) x\<^sub>0 - r\<bar> = \<bar>f ((f ^^ itr) x\<^sub>0) - r\<bar>"
      by simp
    also have "... = \<bar>f ((f ^^ itr) x\<^sub>0) - f r\<bar>"
      using assms(4) by auto
    also have "... \<le> c * \<bar>(f ^^ itr) x\<^sub>0 - r\<bar>"
      by (smt (verit, del_insts) IH assms(1,5,6) c_strict mult_left_le_one_le power_le_one zero_le_power)
    also have "... \<le> c * \<bar>(c ^ itr * \<bar>x\<^sub>0 - r\<bar>)\<bar>"
      using IH c_nonneg by (simp add: mult_mono)
    also have "... \<le> c ^ Suc itr * \<bar>x\<^sub>0 - r\<bar>"
      by (simp add: assms(1))
    finally show "\<bar>(f ^^ Suc itr) x\<^sub>0 - r\<bar> \<le> c ^ Suc itr * \<bar>x\<^sub>0 - r\<bar>".
  qed
qed
  
lemma fixed_point_known_iter_error_bound_local:
  fixes f       :: "real \<Rightarrow> real"
    and r x\<^sub>0  c \<delta> :: real
    and max_iter :: nat
  assumes c_nonneg:    "0 \<le> c"
    and c_strict:      "c < 1"
    and \<delta>_pos:         "\<delta> > 0"
    and r_is_fixed:    "f r = r"
    and x0_in_ball:    "\<bar>r - x\<^sub>0\<bar> < \<delta>"
    and contractive:   "\<forall>s t. \<bar>s - r\<bar> < \<delta> \<and> \<bar>t - r\<bar> < \<delta> \<longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>"
  shows 
    "H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter)[\<bar>x - r\<bar> \<le> c^itr *\<bar>x\<^sub>0 - r\<bar> \<and> (itr \<le> max_iter)]"
proof(vcg)
  fix itr :: nat
  assume step_small: "\<bar>f ((f ^^ itr) x\<^sub>0) - (f ^^ itr) x\<^sub>0\<bar> < tol"
     and below_max:  "itr < max_iter"
 
  from assms have t_in_ball: "\<bar>(f ^^ itr) x\<^sub>0 - r\<bar> < \<delta>"
    by (subst contraction_ball_closure, simp_all)
  then have s_in_ball: "\<bar>f ((f ^^ itr) x\<^sub>0) - r\<bar> < \<delta>"
    by (smt (verit) assms(4,6) c_strict mult_less_cancel_right2)  
  have step_bound:
    "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> \<le> c * \<bar>f ((f ^^ itr) x\<^sub>0) - (f ^^ itr) x\<^sub>0\<bar>"
    using contractive s_in_ball t_in_ball by presburger
  also have "... < tol"
    using c_strict
    by (smt (verit) mult_le_cancel_right2 step_small) 
  finally show "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> < tol".
  then show "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> < tol".  (*Get one goal for free*)
next     
  show "\<bar>(f ^^ max_iter) x\<^sub>0 - r\<bar> \<le> c ^ max_iter * \<bar>x\<^sub>0 - r\<bar>"
  proof (induction max_iter)
    show "\<bar>(f ^^ 0) x\<^sub>0 - r\<bar> \<le> c ^ 0 * \<bar>x\<^sub>0 - r\<bar>"
      by simp
  next
    case (Suc n)    
    have step: "\<bar>(f ^^ Suc n) x\<^sub>0 - r\<bar> = \<bar>f ((f ^^ n) x\<^sub>0) - r\<bar>"
      by simp
    also have "\<dots> = \<bar>f ((f ^^ n) x\<^sub>0) - f r\<bar>"
      using r_is_fixed by force
    also have "\<dots> \<le> c * \<bar>(f ^^ n) x\<^sub>0 - r\<bar>"
      by (smt (verit) Suc.IH assms(1,5,6) c_strict mult_left_le_one_le power_le_one zero_le_power)
    also have "\<dots> \<le> c * (c ^ n * \<bar>x\<^sub>0 - r\<bar>)"
      by (meson Suc.IH assms(1) mult_left_mono)
    also have "\<dots> = c ^ Suc n * \<bar>x\<^sub>0 - r\<bar>"
      by simp
    finally show ?case.
  qed
  then show "\<bar>(f ^^ max_iter) x\<^sub>0 - r\<bar> \<le> c ^ max_iter * \<bar>x\<^sub>0 - r\<bar>"
    by simp
next
  fix itr Break :: nat    
  show "\<bar>(f ^^ itr) x\<^sub>0 - r\<bar> \<le> c ^ itr * \<bar>x\<^sub>0 - r\<bar>"
  proof (induction itr)
    show "\<bar>(f ^^ 0) x\<^sub>0 - r\<bar> \<le> c ^ 0 * \<bar>x\<^sub>0 - r\<bar>"
      by simp
  next
    fix itr 
    assume IH: "\<bar>(f ^^ itr) x\<^sub>0 - r\<bar> \<le> c ^ itr * \<bar>x\<^sub>0 - r\<bar>"   
    have "\<bar>(f ^^ Suc itr) x\<^sub>0 - r\<bar> = \<bar>f ((f ^^ itr) x\<^sub>0) - r\<bar>"
      by simp
    also have "... = \<bar>f ((f ^^ itr) x\<^sub>0) - f r\<bar>"
      using assms(4) by auto
    also have "... \<le> c * \<bar>(f ^^ itr) x\<^sub>0 - r\<bar>"
      by (smt (verit, best) IH assms(1,5,6) c_strict mult_left_le_one_le power_le_one zero_le_power)
    also have "... \<le> c * \<bar>(c ^ itr * \<bar>x\<^sub>0 - r\<bar>)\<bar>"
      using IH c_nonneg by (simp add: mult_mono)
    also have "... \<le> c ^ Suc itr * \<bar>x\<^sub>0 - r\<bar>"
      by (simp add: assms(1))
    finally show "\<bar>(f ^^ Suc itr) x\<^sub>0 - r\<bar> \<le> c ^ Suc itr * \<bar>x\<^sub>0 - r\<bar>".
  qed
qed

lemma fixed_point_unknown_iter_error_bound_local_derive:
  fixes f :: "real \<Rightarrow> real"
  fixes x0 R c :: real and tol :: real and max_iter :: nat
  assumes c_ge0: "0 \<le> c"
      and c_lt1: "c < 1"
      and lips_cball: "\<And>s t. \<bar>s - x0\<bar> \<le> R \<Longrightarrow> \<bar>t - x0\<bar> \<le> R \<Longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>"
      and budget_half: "\<bar>f x0 - x0\<bar> / (1 - c) < R / 2"
  shows
  "\<exists>r\<in>cball x0 R. f r = r \<and>
     (\<exists>\<delta>>0.
        \<bar>x0 - r\<bar> < \<delta> \<and>
        (\<forall>s t. \<bar>s - r\<bar> < \<delta> \<and> \<bar>t - r\<bar> < \<delta> \<longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>) \<and>
        H[True] fixed_point_iter (f, x0, tol, max_iter)
          [\<bar>x - r\<bar> \<le> c ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter])"
proof -
  have R_pos: "R > 0"
    by (smt (verit, best) assms(2) budget_half divide_nonneg_nonneg field_sum_of_halves)
  hence R_ge0: "R \<ge> 0"
    by simp

(*Invariance of S = cball x0 R from the “budget/half” assumption *)
    have budget': "\<bar>f x0 - x0\<bar> \<le> (1 - c) * R"
      using budget_half c_lt1
      by (smt (verit, del_insts) divide_less_eq mult.commute mult_less_cancel_right1)

    have inv: "f ` cball x0 R \<subseteq> cball x0 R"
      using c_ge0 c_lt1 R_ge0 lips_cball budget' by (rule inv_cball_of_budget)

(* Banach on S: derive r *)
    have comp: "complete (cball x0 R)"
      by (simp add: compact_imp_complete)
    have ne:   "cball x0 R \<noteq> {}"
      using R_pos by simp

    from c_ge0 c_lt1 R_pos comp lips_cball inv have " \<exists>!x. x \<in> cball x0 R \<and> f x = x"
      by(subst banach_fix[where c = c], simp_all, metis dist_commute dist_real_def mem_cball)

    then obtain r where r_in: "r \<in> cball x0 R" and rfix: "f r = r"
      and runiq: "\<And>y. y \<in> cball x0 R \<Longrightarrow> f y = y \<Longrightarrow> y = r"
      by meson

(* r is strictly interior, with a quantitative bound *)
    have dist_r_x0_le: "\<bar>r - x0\<bar> \<le> \<bar>f x0 - x0\<bar> / (1 - c)"
    proof -
      have "\<bar>r - x0\<bar> = \<bar>f r - x0\<bar>" by (simp add: rfix)
      also have "\<dots> \<le> \<bar>f r - f x0\<bar> + \<bar>f x0 - x0\<bar>"
        by linarith 
      also have "\<dots> \<le> c * \<bar>r - x0\<bar> + \<bar>f x0 - x0\<bar>"
        using assms(3) dist_real_def r_in by force
      finally show ?thesis
        using c_lt1 by (simp add: field_simps)
    qed
    have r_strict_inside: "\<bar>r - x0\<bar> < R/2"
      using dist_r_x0_le budget_half by linarith

(*Pick \<delta> so that ball r \<delta> \<subseteq> cball x0 R and x0 is inside that \<delta>-ball *)
    define \<delta> where "\<delta> = R - \<bar>r - x0\<bar>"
    then have \<delta>_pos: "\<delta> > 0" 
      using r_strict_inside by linarith 

  have x0_in: "\<bar>x0 - r\<bar> < \<delta>"
    using \<delta>_def r_strict_inside by linarith

  have ball_in_cball:
    "\<And>y. \<bar>y - r\<bar> < \<delta> \<Longrightarrow> \<bar>y - x0\<bar> \<le> R"
    by (simp add: \<delta>_def abs_triangle_ineq4)

  (* Local contractivity on ball r \<delta> follows from Lipschitz on the cball *)
  have lips_local:
    "\<And>s t. \<bar>s - r\<bar> < \<delta> \<Longrightarrow> \<bar>t - r\<bar> < \<delta> \<Longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>"
  proof -
    fix s t assume sr: "\<bar>s - r\<bar> < \<delta>" and tr: "\<bar>t - r\<bar> < \<delta>"
    have "\<bar>s - x0\<bar> \<le> R" using ball_in_cball sr .
    moreover have "\<bar>t - x0\<bar> \<le> R" using ball_in_cball tr .
    ultimately show "\<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>"
      by (rule lips_cball)
  qed

  (* Apply "known fixed" version with this r and \<delta> *)
  from c_ge0 c_lt1 rfix \<delta>_pos x0_in
  have local_triple:
    "H[True] fixed_point_iter (f, x0, tol, max_iter)
       [\<bar>x - r\<bar> \<le> c ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter]"
    by (subst fixed_point_known_iter_error_bound_local_cball[where \<delta> = \<delta>], 
        simp_all,  simp add: \<delta>_def assms(3))

  (* Package \<delta> and the three conjuncts *)
  have ex_delta:
    "\<exists>\<delta>>0.
       \<bar>x0 - r\<bar> < \<delta> \<and>
       (\<forall>s t. \<bar>s - r\<bar> < \<delta> \<and> \<bar>t - r\<bar> < \<delta> \<longrightarrow> \<bar>f s - f t\<bar> \<le> c * \<bar>s - t\<bar>) \<and>
       H[True] fixed_point_iter (f, x0, tol, max_iter)
         [\<bar>x - r\<bar> \<le> c ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter]"
    by (intro exI[of _ \<delta>] conjI \<delta>_pos x0_in)
       (use lips_local local_triple in auto)

  (* Instantiate r for the outer bounded existential *)
  show ?thesis
    by (rule bexI[of _ r])
       (use r_in rfix ex_delta in auto)
qed

\<comment> \<open>This is a local Banach–type contraction statement. Since \(f \in C^{1}(U)\) and
\(|\mathrm{deriv}\,f\,r|<1\), continuity of \(\mathrm{deriv}\,f\) yields \(\varepsilon>0\) and
\(\delta>0\) with \(|\mathrm{deriv}\,f\,x|\le 1-\varepsilon\) whenever \(|x-r|<\delta\).
By the mean-value theorem, this uniform bound implies the local Lipschitz estimate
\(|f(s)-f(t)|\le(1-\varepsilon)\,|s-t|\) for all \(s,t\) with \(|s-r|,|t-r|<\delta\).

Instantiating the generic contraction error lemma with \(c=1-\varepsilon\) yields the geometric decay
\[
  |x-r|\;\le\;(1-\varepsilon)^{\mathit{itr}}\;|x_{0}-r|
\]
at loop exit, uniformly for every start \(x_{0}\) in the \(\delta\)-ball around \(r\).\<close>

lemma fixed_point_iter_error_bound_C1:
  fixes f    :: "real \<Rightarrow> real"
    and r tol :: real
    and max_iter :: nat
  assumes r_fixed   : "f r = r"
      and r_in_U    : "r \<in> U"
      and cont_deriv: "C_k_on 1 f U"    
      and f_strict  : "\<bar>deriv f r\<bar> < 1"
  shows
    "\<exists>(\<delta> :: real)>0. \<exists>(\<epsilon> :: real)>0.       
        (\<forall>(x\<^sub>0 :: real). \<bar>r - x\<^sub>0\<bar> < \<delta> \<longrightarrow>
           H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter)
             [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x\<^sub>0 - r\<bar> \<and> (itr \<le> max_iter)])"
proof -
  obtain \<epsilon> \<delta> where
      \<epsilon>_pos: "0 < \<epsilon>"
    and \<epsilon>_lt  :  "\<epsilon> < 1"
    and \<delta>_pos  : "\<delta> > 0"
    and subset : "{r - \<delta><..<r + \<delta>} \<subseteq> U"
    and lip    : "\<forall>x y. x \<in> {r-\<delta><..<r+\<delta>} \<longrightarrow> y \<in> {x<..<r+\<delta>}
                       \<longrightarrow> \<bar>f x - f y\<bar> < (1 - \<epsilon>) * \<bar>x - y\<bar>"
    by (meson assms(2,4) cont_deriv contractive_deriv_imp_contra)

  show "\<exists>\<delta>>0. (\<exists>\<epsilon>>0. (\<forall>x\<^sub>0. \<bar>r - x\<^sub>0\<bar> < \<delta> \<longrightarrow>
                      H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter)
                        [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x\<^sub>0 - r\<bar> \<and> (itr \<le> max_iter)]))"
  proof (intro exI[where x=\<delta>], intro conjI insert \<delta>_pos)
    show "\<exists>\<epsilon>>0. \<forall>x\<^sub>0. \<bar>r - x\<^sub>0\<bar> < \<delta> \<longrightarrow> H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter) [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x\<^sub>0 - r\<bar> \<and> (itr \<le> max_iter)]"
    proof (intro exI[where x=\<epsilon>], intro conjI insert \<epsilon>_pos, clarify)
      fix x\<^sub>0 :: real
      assume sufficiently_close: "\<bar>r - x\<^sub>0\<bar> < \<delta>"      
      with assms(1-3) \<delta>_pos show
        "H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter)
          [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x\<^sub>0 - r\<bar> \<and> (itr \<le> max_iter)]"
      proof (subst fixed_point_known_iter_error_bound_local[where \<delta> = \<delta>], safe)
        show "0 \<le> 1 - \<epsilon>"
          using \<epsilon>_lt by auto
        show "1 - \<epsilon> < 1"
          using \<epsilon>_pos by auto        
      next
        fix s t
        assume  a1: "\<bar>s - r\<bar> < \<delta>" and a2: "\<bar>t - r\<bar> < \<delta>"
         
        have s_dist: "s \<in> {r - \<delta><..<r + \<delta>}"
          using a1 dist_real_def by auto
        have t_dist: "t \<in> {r - \<delta><..<r + \<delta>}"
          using a2 dist_real_def by auto
  
        show "\<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
        proof (cases "t < s")
          show "\<lbrakk>t < s\<rbrakk> \<Longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
            by (metis abs_minus_commute greaterThanLessThan_iff less_eq_real_def lip s_dist t_dist)
          show "\<lbrakk>\<not> t < s\<rbrakk> \<Longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
            by (metis abs_0 cancel_comm_monoid_add_class.diff_cancel greaterThanLessThan_iff 
                lip mult.commute mult_zero_left not_less_iff_gr_or_eq s_dist t_dist verit_comp_simplify1(3))
        qed
      qed
    qed
  qed
qed

lemma fixed_point_iter_error_bound_C1_closed:
  fixes f :: "real \<Rightarrow> real" and r tol :: real and max_iter :: nat
  assumes r_fixed : "f r = r"
      and r_in_U  : "r \<in> U"
      and U_open  : "open U"
      and C1_on_U : "C_k_on 1 f U"
      and deriv_strict: "\<bar>deriv f r\<bar> < 1"
  shows
  "\<exists>\<delta>>0. \<exists>\<epsilon>>0.
     (\<forall>x0::real. \<bar>x0 - r\<bar> \<le> \<delta> \<longrightarrow>
        H[True] fixed_point_iter (f, x0, tol, max_iter)
          [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter])"
proof -
  obtain \<epsilon> \<delta> where
      \<epsilon>_pos : "0 < \<epsilon>"
    and \<epsilon>_lt1: "\<epsilon> < 1"
    and \<delta>_pos : "\<delta> > 0"
    and subset: "{r - \<delta> .. r + \<delta>} \<subseteq> U"
    and lip_ord:
      "\<forall>x y. x \<in> {r - \<delta> .. r + \<delta>} \<longrightarrow> y \<in> {x .. r + \<delta>}
           \<longrightarrow> \<bar>f x - f y\<bar> \<le> (1 - \<epsilon>) * \<bar>x - y\<bar>"
    by (meson C1_on_U r_in_U deriv_strict
              contractive_deriv_imp_contra_closed[of f U r 1])

  show "\<exists>\<delta>>0. (\<exists>\<epsilon>>0.
         (\<forall>x0. \<bar>x0 - r\<bar> \<le> \<delta> \<longrightarrow>
            H[True] fixed_point_iter (f, x0, tol, max_iter)
              [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter]))"
  proof (intro exI[where x=\<delta>], intro conjI insert \<delta>_pos)
    show "\<exists>\<epsilon>>0. \<forall>x0. \<bar>x0 - r\<bar> \<le> \<delta> \<longrightarrow> H[True] fixed_point_iter (f, x0, tol, max_iter) [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter]"
    proof (intro exI[where x=\<epsilon>], intro conjI insert \<epsilon>_pos, clarify)
      fix x\<^sub>0 :: real
      assume sufficiently_close: "\<bar>x\<^sub>0 - r\<bar> \<le> \<delta>"      
      show "H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter) [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x\<^sub>0 - r\<bar> \<and> itr \<le> max_iter]"        
      proof (subst fixed_point_known_iter_error_bound_local_cball[where \<delta> = \<delta>], safe)
        show "0 \<le> 1 - \<epsilon>" using \<epsilon>_lt1 by simp
        show "1 - \<epsilon> < 1" using \<epsilon>_pos by simp
        show "0 \<le> \<delta>" using \<delta>_pos by simp
        show " f r = r" using r_fixed by simp        
        show "\<bar>x\<^sub>0 - r\<bar> \<le> \<delta>" using sufficiently_close by simp       
      next
        fix s t :: real
        assume a1: "\<bar>s - r\<bar> \<le> \<delta>" and a2: "\<bar>t - r\<bar> \<le> \<delta>"
        have s_in: "s \<in> {r - \<delta> .. r + \<delta>}"
          using a1 by force
        have t_in: "t \<in> {r - \<delta> .. r + \<delta>}"
          using a2 by force

        show "\<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
        proof (cases "t \<le> s")
          case True
          hence "s \<in> {t .. r + \<delta>}" 
            using s_in by presburger
          hence "\<bar>f t - f s\<bar> \<le> (1 - \<epsilon>) * \<bar>t - s\<bar>"
            using lip_ord t_in by blast
          thus ?thesis 
            by (simp add: abs_minus_commute)
        next
          case False
          hence "s \<le> t" by simp
          hence "t \<in> {s .. r + \<delta>}"
            using t_in by presburger
          hence "\<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
            using lip_ord s_in by blast
          thus ?thesis.
        qed
      qed 
    qed
  qed
qed

lemma fixed_point_iter_error_bound_C1_closed_derive_local:
  fixes f :: "real \<Rightarrow> real"
  fixes x0 R \<epsilon> tol :: real and max_iter :: nat
  assumes U_open   : "open U"
      and C1_on_U  : "C_k_on 1 f U"
      and subU     : "cball x0 R \<subseteq> U"
      and R_pos    : "R > 0"
      and eps_pos  : "\<epsilon> > 0"
      and eps_lt1  : "\<epsilon> < 1"
      and deriv_bd : "\<And>x. \<bar>x - x0\<bar> \<le> R \<Longrightarrow> \<bar>deriv f x\<bar> \<le> 1 - \<epsilon>"
      and budget_half: "\<bar>f x0 - x0\<bar> / \<epsilon> < R / 2"
  shows
  "\<exists>r\<in>cball x0 R. f r = r \<and>
     (\<exists>\<delta>>0.
        \<bar>x0 - r\<bar> < \<delta> \<and>
        (\<forall>s t. \<bar>s - r\<bar> < \<delta> \<and> \<bar>t - r\<bar> < \<delta> \<longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>) \<and>
        H[True] fixed_point_iter (f, x0, tol, max_iter)
          [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter])"
proof -
  (* Lipschitz with constant (1-\<epsilon>) on S = cball x0 R via MVT *)
  have lips:
    "\<And>s t. \<bar>s - x0\<bar> \<le> R \<Longrightarrow> \<bar>t - x0\<bar> \<le> R \<Longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
  proof -
    fix s t 
    assume hs: "\<bar>s - x0\<bar> \<le> R" and ht: "\<bar>t - x0\<bar> \<le> R"
    consider (lt) "s < t" | (gt) "t < s" | (eq) "s = t" by linarith
    show "\<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
    proof -
      (* segment stays in the working ball, hence in U *)
      have seg_in_ball: "{min s t .. max s t} \<subseteq> cball x0 R"
      proof
        fix x :: real
        assume xseg: "x \<in> {min s t .. max s t}"
        define s' where "s' = min s t"
        define t' where "t' = max s t"
        have "s' \<le> x \<and> x \<le> t'" 
          using xseg by (simp add: s'_def t'_def)
        then have "\<bar>x - x0\<bar> \<le> max (\<bar>s' - x0\<bar>) (\<bar>t' - x0\<bar>)"
          by linarith
        also have "\<dots> \<le> R"
          using hs ht s'_def t'_def by linarith
        finally show "x \<in> cball x0 R" 
          by (simp add: dist_real_def)
      qed
      have seg_in_U: "{min s t .. max s t} \<subseteq> U" 
        using subU seg_in_ball by blast
    
      consider (eq) "s = t" | (lt) "s < t" | (gt) "t < s" by linarith
      then show ?thesis
      proof cases
        case eq
        then show ?thesis by simp
      next
        case lt
        then have cont_f: "continuous_on {s..t} f"
          by(metis C1_cont_diff assms(2) continuous_on_subset differentiable_imp_continuous_on 
             max.absorb4 min.strict_order_iff seg_in_U)
        with lt 
        have mvt_ex:
          "\<exists>l z. s < z \<and> z < t \<and> (f has_real_derivative l) (at z)
                \<and> f t - f s = (t - s) * l"
          by (rule MVT, smt (z3) C1_cont_diff DERIV_deriv_iff_real_differentiable 
              assms(2) atLeastAtMost_eq_cball dist_real_def field_sum_of_halves 
              mem_cball seg_in_U subset_eq)        
        then obtain \<xi> l where \<xi>_between: "s < \<xi>" "\<xi> < t"
          and hasD: "(f has_real_derivative l) (at \<xi>)"
          and slope_l: "f t - f s = (t - s) * l"
          by blast
    
        have \<xi>_in_ball: "\<xi> \<in> cball x0 R"
          using \<xi>_between(1) \<xi>_between(2) dist_real_def hs ht by force
        
        have der_bd: "\<bar>deriv f \<xi>\<bar> \<le> 1 - \<epsilon>"
          using \<xi>_between(1,2) assms(7) hs ht by auto
    
        have "\<bar>f s - f t\<bar> = \<bar>l\<bar> * \<bar>s - t\<bar>"
          by (metis Groups.mult_ac(2) abs_minus_commute abs_mult slope_l)
        also have "\<dots> = \<bar>deriv f \<xi>\<bar> * \<bar>s - t\<bar>"
          using DERIV_imp_deriv[OF hasD] by simp
        also have "\<dots> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
          by (simp add: der_bd mult_right_mono)
        finally show ?thesis.
      next
        case gt
        then have cont_f: "continuous_on {t..s} f"
          by (metis C1_cont_diff assms(2) continuous_on_subset differentiable_imp_continuous_on 
              max_min_same(3,4) min.strict_order_iff min_max_distribs(4) seg_in_U)

        with gt
        have mvt_ex:
          "\<exists>l z. t < z \<and> z < s \<and> (f has_real_derivative l) (at z)
                \<and> f s - f t = (s - t) * l"
          by (rule MVT,
              smt (z3) C1_cont_diff DERIV_deriv_iff_real_differentiable assms(2)
                       atLeastAtMost_eq_cball dist_real_def field_sum_of_halves
                       mem_cball seg_in_U subset_eq)
        then obtain \<xi> l where \<xi>_between: "t < \<xi>" "\<xi> < s"
          and hasD: "(f has_real_derivative l) (at \<xi>)"
          and slope_l: "f s - f t = (s - t) * l"
          by blast
      
        have \<xi>_in_ball: "\<xi> \<in> cball x0 R"
          using \<xi>_between(1,2) dist_real_def hs ht by force
      
        have der_bd: "\<bar>deriv f \<xi>\<bar> \<le> 1 - \<epsilon>"
          using \<xi>_between(1,2) assms(7) hs ht by auto
      
        have "\<bar>f s - f t\<bar> = \<bar>l\<bar> * \<bar>s - t\<bar>"
          by (metis Groups.mult_ac(2) abs_mult slope_l)
        also have "\<dots> = \<bar>deriv f \<xi>\<bar> * \<bar>s - t\<bar>"
          using DERIV_imp_deriv[OF hasD] by simp
        also have "\<dots> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
          by (simp add: der_bd mult_right_mono)
        finally show ?thesis.
      qed
    qed
  qed
    (* Invariance of the ball and Banach fixed point on S = cball x0 R *)
  have c_pos: "0 < 1 - \<epsilon>" using eps_lt1 by simp
  have c_nonneg: "0 \<le> 1 - \<epsilon>" using c_pos by linarith
  have c_lt1: "(1 - \<epsilon>) < 1"  using eps_pos by simp
  have R_ge0: "0 \<le> R" using R_pos by simp

  have inv: "f ` cball x0 R \<subseteq> cball x0 R"
  proof (rule inv_cball_of_budget[where c = "1 - \<epsilon>"])
    show "0 \<le> 1 - \<epsilon>" by (rule c_nonneg)
    show "1 - \<epsilon> < 1" by (rule c_lt1)
    show "0 \<le> R" by (rule R_ge0)
    show "\<And>s t. \<bar>s - x0\<bar> \<le> R \<Longrightarrow> \<bar>t - x0\<bar> \<le> R \<Longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
      by (rule lips)
    show "\<bar>f x0 - x0\<bar> \<le> (1 - (1 - \<epsilon>)) * R"
      by (smt (verit, best) R_ge0 assms(8) divide_less_cancel eps_pos 
          field_sum_of_halves nonzero_mult_div_cancel_left)
  qed

  have comp: "complete (cball x0 R)"
    by (simp add: complete_eq_closed)

  have ne:   "cball x0 R \<noteq> {}"      
    using R_pos by simp

  have exuniq: "\<exists>!x. x \<in> cball x0 R \<and> f x = x"
  proof (rule banach_fix[where c = "1 - \<epsilon>"])
    show "complete (cball x0 R)" by (rule comp)
    show "cball x0 R \<noteq> {}" by (rule ne)
    show "0 \<le> 1 - \<epsilon>" by (rule c_nonneg)
    show "1 - \<epsilon> < 1" by (rule c_lt1)
    show "f ` cball x0 R \<subseteq> cball x0 R" by (rule inv)
    show "\<forall>x\<in>cball x0 R. \<forall>y\<in>cball x0 R.
            dist (f x) (f y) \<le> (1 - \<epsilon>) * dist x y"
      by (simp add: dist_commute dist_real_def lips)
  qed
  then obtain r where r_in: "r \<in> cball x0 R" and rfix: "f r = r"
    and runiq: "\<And>y. y \<in> cball x0 R \<Longrightarrow> f y = y \<Longrightarrow> y = r"
    by blast

  (* One-step contraction toward r on S *)
  have step_contr:
    "\<And>y. y \<in> cball x0 R \<Longrightarrow> \<bar>f y - r\<bar> \<le> (1 - \<epsilon>) * \<bar>y - r\<bar>"
    using lips r_in rfix  by (smt (verit, del_insts) dist_real_def mem_cball)

  thm contraction_cball_closure
  (* Iterates stay in S *)
  have x0_in: "x0 \<in> cball x0 R" using R_pos by simp
  have stay: "\<forall> n. (f ^^ n) x0 \<in> cball x0 R"
  proof clarify
    fix n :: nat
    show "(f ^^ n) x0 \<in> cball x0 R"    
    proof (induction n)
      show "(f ^^ 0) x0 \<in> cball x0 R"
        using x0_in by force
    next
      case (Suc n)
      have "(f ^^ n) x0 \<in> cball x0 R" by (rule Suc.IH)
      hence "f ((f ^^ n) x0) \<in> f ` cball x0 R" by (rule imageI)
      hence "f ((f ^^ n) x0) \<in> cball x0 R"
        using inv by (blast dest: subsetD)
      thus ?case by simp
    qed
  qed
  
  (* Geometric error bound *)
  have geom: "\<forall> n. \<bar>(f ^^ n) x0 - r\<bar> \<le> (1 - \<epsilon>) ^ n * \<bar>x0 - r\<bar>"
  proof clarify
    fix n :: nat
    show "\<bar>(f ^^ n) x0 - r\<bar> \<le> (1 - \<epsilon>) ^ n * \<bar>x0 - r\<bar>"
    proof (induction n)
      case 0  show ?case by simp
    next   
      case (Suc n)
      have "\<bar>(f ^^ Suc n) x0 - r\<bar> = \<bar>f ((f ^^ n) x0) - r\<bar>" by simp
      also have "\<dots> \<le> (1 - \<epsilon>) * \<bar>(f ^^ n) x0 - r\<bar>"
        using stay step_contr by simp
      also have "\<dots> \<le> (1 - \<epsilon>) * ((1 - \<epsilon>) ^ n * \<bar>x0 - r\<bar>)"
        by (meson Suc.IH c_nonneg mult_left_mono)
      also have "\<dots> = (1 - \<epsilon>) ^ Suc n * \<bar>x0 - r\<bar>" by simp
      finally show ?case.
    qed
  qed
  (* r is strictly interior: |r - x0| \<le> |f x0 - x0| / \<epsilon> < R/2 *)
  have r_dist: "\<bar>r - x0\<bar> \<le> \<bar>f x0 - x0\<bar> / \<epsilon>"
  proof -
    have "\<bar>r - x0\<bar> = \<bar>f r - x0\<bar>" by (simp add: rfix)
    also have "\<dots> \<le> \<bar>f r - f x0\<bar> + \<bar>f x0 - x0\<bar>" by linarith
    also have "\<dots> \<le> (1 - \<epsilon>) * \<bar>r - x0\<bar> + \<bar>f x0 - x0\<bar>"
      using lips r_in by (simp add: dist_real_def)
    finally have "\<epsilon> * \<bar>r - x0\<bar> \<le> \<bar>f x0 - x0\<bar>" by (simp add: field_simps)
    thus ?thesis using eps_pos by (simp add: field_simps)
  qed
  have r_strict: "\<bar>r - x0\<bar> < R / 2"
    using r_dist budget_half by linarith

  (* choose \<delta> so that ball r \<delta> \<subseteq> cball x0 R and x0 \<in> ball r \<delta> *)
  define \<delta> where "\<delta> = R - \<bar>r - x0\<bar>"
  have \<delta>_pos: "\<delta> > 0" using R_pos r_strict by (simp add: \<delta>_def)
  have x0_in: "\<bar>x0 - r\<bar> < \<delta>" using \<delta>_def r_strict by linarith
  have ball_in_cball:
    "\<And>y. \<bar>y - r\<bar> < \<delta> \<Longrightarrow> \<bar>y - x0\<bar> \<le> R"
    by (simp add: \<delta>_def abs_triangle_ineq4)

  (* local Lipschitz on ball r \<delta> from global on cball x0 R *)
  have lips_local:
    "\<And>s t. \<bar>s - r\<bar> < \<delta> \<Longrightarrow> \<bar>t - r\<bar> < \<delta> \<Longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
  proof -
    fix s t assume sr: "\<bar>s - r\<bar> < \<delta>" and tr: "\<bar>t - r\<bar> < \<delta>"
    have "\<bar>s - x0\<bar> \<le> R" using ball_in_cball sr .
    moreover have "\<bar>t - x0\<bar> \<le> R" using ball_in_cball tr .
    ultimately show "\<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>" by (rule lips)
  qed

  (* local iteration bound at r with c = 1 - \<epsilon> *)
  have local_triple:
    "H[True] fixed_point_iter (f, x0, tol, max_iter)
       [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter]"
  proof (subst fixed_point_known_iter_error_bound_local_cball[where \<delta> = \<delta> and c = "1 - \<epsilon>"], safe)
    show "0 \<le> 1 - \<epsilon>" using eps_lt1 by simp
    show "1 - \<epsilon> < 1" using eps_pos by simp
    show "0 \<le> \<delta>"
      using \<delta>_pos by linarith 
    show "f r = r" by (rule rfix)
    show "\<bar>x0 - r\<bar> \<le> \<delta>"
      using x0_in by auto 
    show "\<And>s t. \<lbrakk>\<bar>s - r\<bar> \<le> \<delta>; \<bar>t - r\<bar> \<le> \<delta>\<rbrakk> \<Longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
      by (simp add: \<delta>_def lips)
  qed
  then have "(\<exists>\<delta>>0. \<bar>x0 - r\<bar> < \<delta> \<and>
              (\<forall>s t. \<bar>s - r\<bar> < \<delta> \<and> \<bar>t - r\<bar> < \<delta> \<longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>) \<and>
              H[True] fixed_point_iter (f, x0, tol, max_iter)
               [\<bar>x - r\<bar> \<le> (1 - \<epsilon>) ^ itr * \<bar>x0 - r\<bar> \<and> itr \<le> max_iter])"
    by (intro exI[of _ \<delta>] conjI \<delta>_pos x0_in, simp add: lips_local local_triple, blast)
  then show ?thesis
    using exuniq runiq by blast
qed
          
\<comment> \<open>Quadratic error decay near a fixed point.
Assume \(f(r)=r\), \(f \in C^{1}(U)\), \(f'(r)=0\), and \(f\) is twice differentiable at \(r\).
Then there exist \(\delta>0\) and \(\varepsilon>0\) such that, for all starts \(x_{0}\) with
\(|x_{0}-r|<\delta\), the iteration satisfies the bound
\[
  |x-r|\;\le\;\Bigl(\tfrac{|f''(r)|+\varepsilon}{2}\Bigr)^{\,2^{\mathit{itr}}-1}\,|x_{0}-r|^{\,2^{\mathit{itr}}}.
\]
This is the hallmark of quadratic convergence: each step (locally) squares the error up to a
uniform constant depending on \(f''(r)\). The parameter \(\varepsilon>0\) accounts for the
local nature of the estimate and can be made arbitrarily small by shrinking the neighborhood.
Our proof invokes the Peano form of Taylor’s theorem near \(r\), yielding
\(f(x)-r=\tfrac12 f''(r)(x-r)^2+o\!\left((x-r)^2\right)\), from which the stated bound follows.\<close>
    
lemma fixed_point_iter_quadratic_convergence_case:
  fixes f        :: "real \<Rightarrow> real"
    and r        :: real
    and max_iter  :: nat
  assumes r_fixed   : "f r = r"
      and r_in_U    : "r \<in> U"
      and cont_deriv: "C_k_on 1 f U"      
      and der0     : "deriv f r = 0"     
      and twice_dff: "f twice_differentiable_at r"
  shows
    "\<exists>(\<delta> :: real)>0. \<exists>(\<epsilon> :: real)>0.           
      (\<forall>x\<^sub>0. \<bar>r - x\<^sub>0\<bar> < \<delta> \<longrightarrow>
       H[True] fixed_point_iter (f,x\<^sub>0, tol, max_iter)
       [\<bar>x - r\<bar> \<le> (((\<bar>deriv (deriv f) r\<bar> + \<epsilon>)/2)^(2^itr-1))* \<bar>x\<^sub>0 - r\<bar>^(2^itr) \<and> (itr \<le> max_iter)])"
proof - 
  obtain \<epsilon> \<delta>0 where
      \<epsilon>_pos: "0 < \<epsilon>" 
    and \<epsilon>_lt: "\<epsilon> < 1"
    and \<delta>0_pos  : "\<delta>0 > 0"
    and subset : "{r - \<delta>0<..<r + \<delta>0} \<subseteq> U"
    and lip    : "\<forall>x y. x \<in> {r-\<delta>0<..<r+\<delta>0} \<longrightarrow> y \<in> {x<..<r+\<delta>0}
                       \<longrightarrow> \<bar>f x - f y\<bar> < (1 - \<epsilon>) * \<bar>x - y\<bar>"
    by (metis abs_0 assms(2,4) cont_deriv contractive_deriv_imp_contra zero_less_one)

  \<comment> \<open>Here we apply Taylor’s theorem with Peano remainder at \(r\): \<close>
  have "(\<lambda>x. peano_remainder (Suc 1) f r x / (x - r) ^ Suc 1) \<midarrow>r\<rightarrow> 0"
    apply (rule Taylor_Peano_remainder)
    using Suc_1 twice_dff by presburger
  then have "(\<lambda>x. (f x - (\<Sum>i\<le>2. Nth_derivative i f r / fact i * (x - r) ^ i)) / (x - r) ^ 2) \<midarrow>r\<rightarrow> 0"
    unfolding peano_remainder_def taylor_poly_def
    by (metis Suc_1) 
  then have "(\<forall>\<epsilon>>0. \<exists>\<delta>>0. \<forall>y. y \<noteq> r \<and> \<bar>y - r\<bar> < \<delta> \<longrightarrow> 
  \<bar>(\<lambda>x. (f x - (\<Sum>m\<le>2. Nth_derivative m f r / fact m * (x - r) ^ m)) / (x - r) ^ 2) y - 0\<bar> < \<epsilon>)"
    using tendsto_at_x_epsilon_def by simp
  then obtain \<delta>1 where \<delta>1_pos: "\<delta>1 > 0"
  and r0_prop:
    "\<And>x. x \<noteq> r \<Longrightarrow> \<bar>x - r\<bar> < \<delta>1 \<longrightarrow>
         \<bar>(f x - (\<Sum>m\<le>2. Nth_derivative m f r / fact m * (x - r)^m)) / (x - r)^2\<bar> < \<epsilon> / 2"
    using \<epsilon>_pos by (smt (verit, del_insts) half_gt_zero)

  then obtain h :: "real \<Rightarrow> real" where h_def: "h = (\<lambda> x. (f x - (\<Sum>m\<le>2. Nth_derivative m f r / fact m * (x - r)^m)) / (x - r)^2)"
      and h_bound: "\<And>x. x \<noteq> r \<Longrightarrow> \<bar>x - r\<bar> < \<delta>1 \<longrightarrow> \<bar>h x\<bar> < \<epsilon> / 2"
    by presburger

  obtain \<delta> where \<delta>_def: "\<delta> = min \<delta>0 \<delta>1"
    by blast
  then have \<delta>_pos: "0 < \<delta>" and \<delta>_leq_\<delta>0: "\<delta> \<le> \<delta>0" and \<delta>_leq_\<delta>1: "\<delta> \<le> \<delta>1"
    using \<delta>0_pos \<delta>1_pos by linarith+

  from lip have contraction: "\<forall>s t. s \<noteq> t \<longrightarrow> \<bar>s - r\<bar> < \<delta> \<longrightarrow> \<bar>t - r\<bar> < \<delta> \<longrightarrow> \<bar>f s - f t\<bar> < (1 - \<epsilon>) * \<bar>s - t\<bar>"
    by(rule contraction_ball_closure', (simp add: \<epsilon>_pos \<delta>_pos \<delta>_leq_\<delta>0)+)

  show "\<exists>\<delta>>0. \<exists>\<epsilon>>0. \<forall>x\<^sub>0. \<bar>r - x\<^sub>0\<bar> < \<delta> \<longrightarrow> H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter) 
                    [\<bar>x - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ itr - 1) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ itr \<and> (itr \<le> max_iter)]"
  proof(intro exI[where x=\<delta>], intro conjI insert \<delta>_pos)
    show "\<exists>\<epsilon>>0. \<forall>x\<^sub>0. \<bar>r - x\<^sub>0\<bar> < \<delta> \<longrightarrow> H[True]fixed_point_iter (f, x\<^sub>0, tol, max_iter) 
               [\<bar>x - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ itr - 1) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ itr \<and> (itr \<le> max_iter)]"
    proof(intro exI[where x=\<epsilon>], intro conjI insert \<epsilon>_pos, clarify)
      fix x\<^sub>0 :: real
      assume sufficiently_close: "\<bar>r - x\<^sub>0\<bar> < \<delta>"

      have contractive_iterates: "\<forall> (Itr :: nat). \<bar>(f ^^ Itr) x\<^sub>0 - r\<bar> < \<delta>"
      proof clarify
        fix Itr
        show "\<bar>(f ^^ Itr) x\<^sub>0 - r\<bar> < \<delta>"
        proof(subst contraction_ball_closure[where c = "(1 - \<epsilon>)"])
          show "f r = r"
            by (simp add: assms(1))
          show "0 \<le> 1 - \<epsilon> \<and> 1 - \<epsilon> < 1"
            using \<epsilon>_lt \<epsilon>_pos by auto
          show "\<bar>x\<^sub>0 - r\<bar> < \<delta>" and True
            using sufficiently_close by auto
          show "\<forall>s t. \<bar>s - r\<bar> < \<delta> \<longrightarrow> \<bar>t - r\<bar> < \<delta> \<longrightarrow> \<bar>f s - f t\<bar> \<le> (1 - \<epsilon>) * \<bar>s - t\<bar>"
            by (metis abs_0 cancel_comm_monoid_add_class.diff_cancel contraction less_eq_real_def mult.commute mult_zero_left)
        qed
      qed
         
      show "H[True] fixed_point_iter (f, x\<^sub>0, tol, max_iter) [\<bar>x - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ itr - 1) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ itr \<and> (itr \<le> max_iter)]"
      proof(vcg)
        fix itr :: nat
        assume step_small: "\<bar>f ((f ^^ itr) x\<^sub>0) - (f ^^ itr) x\<^sub>0\<bar> < tol"
           and below_max:  "itr < max_iter"
        then have "\<bar>f ((f ^^ itr) x\<^sub>0) - r\<bar> < \<delta>"
          by (metis contractive_iterates funpow.simps(2) o_apply)
        then have step_bound:
          "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> \<le> (1 - \<epsilon>) * \<bar>f ((f ^^ itr) x\<^sub>0) - (f ^^ itr) x\<^sub>0\<bar>"
          by (metis abs_0 arith_simps(63) contraction diff_self less_eq_real_def contractive_iterates)
        also have "... < tol"
          by (smt (verit, best) \<epsilon>_lt \<epsilon>_pos mult_left_le_one_le step_small)
        finally show "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> < tol".
        then show "\<bar>f (f ((f ^^ itr) x\<^sub>0)) - f ((f ^^ itr) x\<^sub>0)\<bar> < tol".  (*Get one goal for free*)
      next  
        have one_step:
          "\<forall>(x::real). \<bar>x - r\<bar> < \<delta> \<longrightarrow>  \<bar>f x - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) * \<bar>x - r\<bar>^2"
        proof(clarify)
          fix x :: real
          assume delta_close: "\<bar>x - r\<bar> < \<delta>"
          then have h_bnd:"\<bar>h x\<bar> < \<epsilon> / 2"
            by (smt (verit, del_insts) h_bound \<delta>_leq_\<delta>1 \<epsilon>_pos division_ring_divide_zero  h_def half_gt_zero mult_cancel_left2 power2_eq_square)

          show "\<bar>f x - r\<bar> \<le> (\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2 * \<bar>x - r\<bar>\<^sup>2"
          proof(cases "x = r")
            show " \<lbrakk>x = r\<rbrakk> \<Longrightarrow> \<bar>f x - r\<bar> \<le> (\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2 * \<bar>x - r\<bar>\<^sup>2"
              by (simp add: assms(1))
          next
            assume x_neq_r: "x \<noteq> r"
            then have pos_dist: "0 < \<bar>x - r\<bar>"
              by auto

            have taylor_snd_order:
              "f = (\<lambda>x.
                    f r
                  + ((deriv (deriv f) r) / 2) * (x - r)^2
                  + (x - r)^2 * h x)"            
            proof -   
              have f_eq: "f = (\<lambda>x. (\<Sum> m \<le> 2. Nth_derivative m f r / fact m * (x - r)^m) + (x - r)^2 * h x)"
                by (auto simp: h_def fun_eq_iff)   
              then have "f  = 
                     (\<lambda> x.(\<Sum> m \<le> 1. Nth_derivative m f r / fact m * (x - r)^m)
                                  + (Nth_derivative 2 f r / fact 2 * (x - r)^2)
                                  + (x - r)^2 * h x)"
                by (metis (no_types, lifting) Suc_1 sum.atMost_Suc)
              also have "... =
                    (\<lambda> x.            (Nth_derivative 0 f r / fact 0 * (x - r)^0)
                                   + (Nth_derivative 1 f r / fact 1 * (x - r)^1)
                                   + (Nth_derivative 2 f r / fact 2 * (x - r)^2)
                                   + (x - r)^2 * h x)"
                by simp
              also have "... =
                    (\<lambda> x.            (f r)
                                   + (deriv f r  * (x - r))
                                   + ((deriv (deriv f) r) /  2 * (x - r)^2)
                                   + (x - r)^2 * h x)"
                using second_derivative_alt_def by auto
              also have "... =
                    (\<lambda> x.            (f r)                                
                                   + ((deriv (deriv f) r) /  2 * (x - r)^2)
                                   + (x - r)^2 * h x)"
                by (simp add: assms(4))
              finally show ?thesis.
            qed
            then have "f x - r = ((deriv (deriv f) r) / 2 + h x) * (x - r)^2"
              by (smt (verit, best) Groups.mult_ac(2) assms(1) right_diff_distrib')            
            then have abs_fx: "\<bar>f x - r\<bar> = \<bar>(deriv (deriv f) r) / 2 + h x\<bar> * \<bar>x - r\<bar>^2"
              by (simp add: abs_mult)
            also have "... \<le> (\<bar>deriv (deriv f) r\<bar> / 2 + \<bar>h x\<bar>)  * \<bar>x - r\<bar>^2"
              by (simp add: mult_right_mono)
            also have "... \<le> (\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2 * \<bar>x - r\<bar>\<^sup>2"
              using h_bnd pos_dist by auto
            finally show ?thesis.
          qed              
        qed
  
        have Inductive_Step: "\<forall> (Itr :: nat). \<bar>(f ^^ Itr) x\<^sub>0 - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ Itr - Suc 0) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ Itr"
        proof(clarify)
          fix Itr :: nat
          show "\<bar>(f ^^ Itr) x\<^sub>0 - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ Itr - Suc 0) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ Itr"
          proof(induct Itr)
            show "\<bar>(f ^^ 0) x\<^sub>0 - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ 0 - Suc 0) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ 0"
              by simp
          next
            fix Itr
            assume IH:  "\<bar>(f ^^ Itr) x\<^sub>0 - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ Itr - Suc 0) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ Itr"  
            have step_eq: "\<bar>(f ^^ Suc Itr) x\<^sub>0 - r\<bar> = \<bar>f ((f ^^ Itr) x\<^sub>0) - r\<bar>"
              by simp
            also have "\<dots> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) * \<bar>(f ^^ Itr) x\<^sub>0 - r\<bar>^2"
              using one_step contractive_iterates
              by blast  
            also have "\<dots> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2)
                       * ( ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ Itr - Suc 0)
                       * \<bar>x\<^sub>0 - r\<bar> ^ (2 ^ Itr) ) ^ 2"
              by (smt (z3) IH \<epsilon>_pos field_sum_of_halves mult_left_mono power_less_imp_less_base)
            also have "\<dots> = ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (1 + 2 * (2 ^ Itr - Suc 0))
                       * \<bar>x\<^sub>0 - r\<bar> ^ (2 * (2 ^ Itr))"
              by (simp add: power_even_eq power_mult_distrib)
            ultimately show "\<bar>(f ^^ Suc Itr) x\<^sub>0 - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ Suc Itr - Suc 0) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ Suc Itr"
              by (smt (verit, ccfv_SIG) Suc_1 Suc_pred bot_nat_0.not_eq_extremum diff_diff_left
                  nat.discI nat.simps(1) nat_power_eq_Suc_0_iff plus_1_eq_Suc power_Suc0_right 
                  power_add power_eq_0_iff power_eq_if right_diff_distrib')
          qed
        qed
        then show "\<bar>(f ^^ max_iter) x\<^sub>0 - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ max_iter - Suc 0) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ max_iter"
          by blast
        then show "\<bar>(f ^^ max_iter) x\<^sub>0 - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ max_iter - Suc 0) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ max_iter"
          by blast
        show "\<And>itr Break. \<lbrakk>itr \<le> max_iter; 0 < Break; \<bar>f ((f ^^ itr) x\<^sub>0) - (f ^^ itr) x\<^sub>0\<bar> < tol\<rbrakk>  \<Longrightarrow> \<bar>(f ^^ itr) x\<^sub>0 - r\<bar> \<le> ((\<bar>deriv (deriv f) r\<bar> + \<epsilon>) / 2) ^ (2 ^ itr - Suc 0) * \<bar>x\<^sub>0 - r\<bar> ^ 2 ^ itr"
          using Inductive_Step by blast
      qed
    qed
  qed
qed

end