Theory Lipschitz_Subdivisions_Refinements

(***********************************************************************************
 * Copyright (c) University of Exeter, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-3-Clause
 ***********************************************************************************)

chapter‹Subdivisions and Refinements›

theory 
  Lipschitz_Subdivisions_Refinements
  imports 
  Lipschitz_Interval_Extension
  Multi_Interval_Preliminaries
begin

section ‹Subdivisions›

text ‹A uniform subdivision of an interval @{term ‹X›} splits @{term ‹X›} into a vector of equal 
length, contiguous intervals.›

definition uniform_subdivision :: "'a::linordered_field interval ⇒ nat ⇒ 'a interval list" where
"uniform_subdivision A n = map (λi. let i' = of_nat i in 
                                     mk_interval (lower A + (upper A - lower A) *  i' /  of_nat n, 
                                                  lower A + (upper A - lower A) * (i' + 1) /  of_nat n)) [0..<n]"

text ‹The definition @{term "uniform_subdivision"} refers to definition 6.2 
in~\<^cite>‹"moore.ea:introduction:2009"››

definition overlapping_ordered :: "'a::{preorder} interval list ⇒ bool" where
"overlapping_ordered xs = (∀i. i < length xs - 1 ⟶  lower (xs ! (i + 1)) ≤ upper (xs ! i))"

definition overlapping_non_zero_width :: "'a::{preorder, minus, zero, ord} interval list ⇒ bool" where
"overlapping_non_zero_width xs = (∀ i < length xs - 1 . ∃ e. e ∈⇩i (xs ! (i + 1)) ∧ e ∈⇩i (xs ! i) ∧ 0 < width (xs ! (i + 1)) ∧ 0 < width (xs ! i ) ) "

definition overlapping :: "'a::{preorder} interval list ⇒ bool" where
"overlapping xs = (∀ i < length xs - 1 . ∃ e. e ∈⇩i (xs ! (i + 1)) ∧ e ∈⇩i (xs ! i)) "

definition check_is_uniform_subdivision :: "'a::linordered_field interval ⇒ 'a interval list ⇒ bool" where
"check_is_uniform_subdivision A xs = (let n = length xs in 
                                      if n = 0 then True 
                                      else 
                                        let d = width A / of_nat n in
                                        list_all (λ x. width x = d) xs ∧ 
                                        contiguous xs ∧
                                        lower (hd xs) = lower A ∧ 
                                        upper (last xs) = upper A)"

lemma non_empty_subdivision:
  assumes "0 < n"
  shows "uniform_subdivision A n ≠ []"
  unfolding uniform_subdivision_def using assms by simp

lemma uniform_subdivision_id: "uniform_subdivision X 1 = [X]"
  unfolding uniform_subdivision_def by simp

lemma subdivision_length_n:
  assumes "0 < n"
  shows "length(uniform_subdivision A n) = n"
  using assms
proof(induction n rule:nat_induct_non_zero)
  case 1
  then show ?case unfolding uniform_subdivision_def by simp
next
  case (Suc n)
  then show ?case unfolding uniform_subdivision_def by simp
qed

lemma contiguous_uniform_subdivision: "contiguous (uniform_subdivision A n)"
proof -
  have a0: "∀i<length (uniform_subdivision A n) - 1. 
            upper (uniform_subdivision A n ! i) = lower A + (upper A - lower A) * of_nat (i + 1) / of_nat n"
    by (simp add: uniform_subdivision_def divide_right_mono mult_left_mono) 
  have a1: "∀i<length (uniform_subdivision A n) - 1.  
            lower A + (upper A - lower A) * of_nat (i + 1) / of_nat n = lower (uniform_subdivision A n ! (i + 1))"
    by (simp add: uniform_subdivision_def divide_right_mono mult_left_mono) 
  have a2: "∀i<length (uniform_subdivision A n) - 1. 
            upper (uniform_subdivision A n ! i) = lower (uniform_subdivision A n ! (i + 1))"
    using a0 a1 by simp
  have a3: "contiguous (uniform_subdivision A n) = 
            (∀i<length (uniform_subdivision A n) - 1. 
             upper (uniform_subdivision A n ! i) = lower (uniform_subdivision A n ! (i + 1)))"
    unfolding contiguous_def by simp
  show ?thesis using a0 a1 a2 a3 by simp
qed



lemma overlapping_ordered_uniform_subdivision:   
  assumes "0 < n"
  shows "overlapping_ordered (uniform_subdivision A n)"
proof - 
  have a0: "∀i<length (uniform_subdivision A n) - 1. 
            upper (uniform_subdivision A n ! i) ≥ lower A + (upper A - lower A) * of_nat (i + 1) / of_nat n"
    using assms 
    by (simp add: uniform_subdivision_def divide_right_mono mult_left_mono) 
  have a1: "∀i<length (uniform_subdivision A n) - 1.  
            lower A + (upper A - lower A) * of_nat (i + 1) / of_nat n ≥ lower (uniform_subdivision A n ! (i + 1))"
    using assms 
    by (simp add: uniform_subdivision_def divide_right_mono mult_left_mono) 
  have a2: "∀i<length (uniform_subdivision A n) - 1. 
            upper (uniform_subdivision A n ! i) ≥ lower (uniform_subdivision A n ! (i + 1))"
    using a0 a1 by force
  have a3: "overlapping_ordered (uniform_subdivision A n) = 
            (∀i<length (uniform_subdivision A n) - 1. 
             upper (uniform_subdivision A n ! i) ≥ lower (uniform_subdivision A n ! (i + 1)))"
    unfolding overlapping_ordered_def by simp
  show ?thesis using a0 a1 a2 a3 by simp
qed

lemma overlapping_uniform_subdivision:
  assumes "0 < N"
  shows "overlapping (uniform_subdivision X N)"
  using assms
proof - 
  let ?n = "length (uniform_subdivision X N) - 1"
  have a0: "∀ i < ?n . lower (uniform_subdivision X N ! (i + 1)) = upper (uniform_subdivision X N ! i)"
    using assms contiguous_uniform_subdivision unfolding contiguous_def by metis
  have a1: "∀ i < ?n. upper (uniform_subdivision X N ! i) ∈⇩i uniform_subdivision X N ! i
                    ∧ upper (uniform_subdivision X N ! i) ∈⇩i (uniform_subdivision X N ! (i + 1))"
    using a0 in_intervalI lower_le_upper order.refl
    by metis
  have a2: "∀i< ?n. ∃e. e ∈⇩i uniform_subdivision X N ! (i + 1) ∧ e ∈⇩i uniform_subdivision X N ! i" 
    using a1 by auto[1]
  show ?thesis using a2 unfolding overlapping_def by simp
qed 

lemma hd_lower_uniform_subdivision:
  assumes "0 < n"
  shows "lower ( hd (uniform_subdivision A n)) = lower A"
proof -
  have "lower ( hd (uniform_subdivision A n)) = lower A + (upper A - lower A) * of_nat 0 / of_nat n"
    using assms
    by (simp add: uniform_subdivision_def mk_interval' hd_map)  
  also have "... = lower A"
    by simp
  finally show ?thesis .
qed

lemma last_upper_uniform_subdivision:
  assumes "0 < n"
  shows "upper ( last (uniform_subdivision A n)) = upper A"
proof -
  have "upper ( last (uniform_subdivision A n)) = lower A + (upper A - lower A) * of_nat n / of_nat n"
    using assms
    apply (auto simp add: uniform_subdivision_def mk_interval' last_map Let_def)[1] 
    using One_nat_def Suc_pred' add.commute le_add_diff_inverse lower_le_upper 
      nonzero_mult_div_cancel_right of_nat_0_less_iff of_nat_Suc order_less_irrefl apply metis
    by ( simp add: divide_right_mono mult_left_mono) 
    also have "... = upper A"
    using assms by simp
  finally show ?thesis .
qed

lemma uniform_subdivisions_width_single:
  fixes A ::"'a::linordered_field interval"
  shows ‹width (Interval (lower A + (upper A - lower A) *  x / of_nat n,
                    lower A + (upper A - lower A) * (x + 1) /  of_nat n)) =  width A / of_nat n›
proof - 
  have "lower A ≤ upper A " using lower_le_upper by simp
  then have leq: "lower A + (upper A - lower A) *  x /  of_nat n ≤ 
             lower A + (upper A - lower A) * ( x + 1) /  of_nat n"
    by (simp add: divide_le_cancel linorder_not_less mult_le_cancel_left)
  have U: ‹upper (Interval (lower A + (upper A - lower A) *  x / of_nat n,
                            lower A + (upper A - lower A) * ( x + 1) /  of_nat n)) = 
           lower A + (upper A - lower A) * ( x + 1) / of_nat n›
    using upper_bounds leq by blast 
  have L: ‹lower (Interval (lower A + (upper A - lower A) *  x / of_nat n,
                            lower A + (upper A - lower A) * ( x + 1) / of_nat n)) = 
           lower A + (upper A - lower A) *  x / of_nat n›
    using lower_bounds leq by blast
  then show ?thesis using U L add_diff_cancel_left add_diff_cancel_left' diff_divide_distrib 
      mult.comm_neutral vector_space_over_itself.scale_right_diff_distrib unfolding width_def  
    by metis
qed

lemma uniform_subdivisions_width:
  assumes "0 < n" 
  shows ‹∀ A. A ∈ set (uniform_subdivision X n) ⟶ width A = width X / of_nat n›
  apply (simp add: uniform_subdivision_def mk_interval' o_def image_def width_def Let_def split: if_split)
  apply auto[1]
  apply (metis add_diff_cancel_left' diff_divide_distrib mult.right_neutral right_diff_distrib)
  using assms uniform_subdivisions_width_single[simplified width_def] 
  by (simp add: divide_right_mono mult_left_mono) 

lemma uniform_subdivision_sum_width:
  assumes ‹0 < n›
  shows ‹sum_list (map width (uniform_subdivision X n)) = width X›
proof -
  have ‹∀ a . a ∈ set (uniform_subdivision X n) ⟶ width a = width X / of_nat n ›
    using uniform_subdivisions_width using assms by blast
  then have width: "∀ a . a ∈ set (map width (uniform_subdivision X n)) ⟶ a = width X / of_nat n"
    unfolding width_def by auto[1]
  then have width_list: "list_all (λ a . a = width X / of_nat n) (map width (uniform_subdivision X n)) "
    unfolding width_def using list_all_iff by blast
  then have length: "length (map width (uniform_subdivision X n)) = n "
    unfolding uniform_subdivision_def by simp
  then have "sum_list (map width (uniform_subdivision X n)) = (width X / of_nat n) * of_nat n"
    using width_list by (metis list.map_ident_strong mult_of_nat_commute sum_list_triv width) 
  then show ?thesis by (simp add: assms)
qed

lemma uniform_subdivisions_distinct:
  assumes "0 < n" "0 < width A"
  shows "distinct (uniform_subdivision A n)"
proof -
  have "∀i< n. ∀j< n. i ≠ j ⟶ (uniform_subdivision A n) ! i ≠ (uniform_subdivision A n) ! j"
  proof -
      have f1: "∀i< n. ∀j< n. i ≠ j ⟶ (upper A - lower A) * of_nat i / of_nat n ≠ (upper A - lower A) * of_nat j / of_nat n"
        using assms(1) assms(2) divide_cancel_right less_numeral_extra(3) mult_cancel_left of_nat_eq_0_iff of_nat_eq_iff width_def 
        by metis
      have f2: "∀i< n. ∀j< n. i ≠ j ⟶ lower A + (upper A - lower A) * of_nat (i + 1) / of_nat n ≠ lower A + (upper A - lower A) * of_nat (j + 1) / of_nat n"
        using  assms(1) assms(2) unfolding width_def by simp
      have f3: "∀i<  n. lower ((uniform_subdivision A n) ! i) = lower A + (upper A - lower A) *  of_nat i / of_nat n"
        using assms by (simp add: uniform_subdivision_def divide_right_mono mult_left_mono Let_def) 
      have f5: "∀i<n - 1. (upper ((uniform_subdivision A n) ! i)) = lower ((uniform_subdivision A n) ! Suc i)"
        using assms by (simp add: uniform_subdivision_def divide_right_mono mult_left_mono)
      have f6: "∀j<n - 1. (upper ((uniform_subdivision A n) ! j)) = lower ((uniform_subdivision A n) ! Suc j)"
        using assms(1) f5 contiguous_uniform_subdivision unfolding contiguous_def subdivision_length_n by blast
      have "∀i<n. ∀j<n. i ≠ j ⟶ lower ((uniform_subdivision A n) ! i) ≠ lower ((uniform_subdivision A n) ! j)"
        using f1 f2 f3 by auto[1]
    then show ?thesis by metis
  qed
  then show ?thesis using assms(1) distinct_conv_nth subdivision_length_n by metis
qed

lemma uniform_subdivisions_non_overlapping:
  assumes "0 < n" 
  shows "non_overlapping_sorted (uniform_subdivision A n)"
proof -
  have "∀i<n. ∀j<n. i < j ⟶ upper ((uniform_subdivision A n) ! i) ≤ lower ((uniform_subdivision A n) ! j)"
  proof -
    have f0: ‹0 ≤ width A› unfolding width_def lower_le_upper by simp 
      have f2: "∀i<n. upper ((uniform_subdivision A n) ! i) = lower A + (upper A - lower A) * of_nat (i + 1) / of_nat n"
        using assms by (simp add: uniform_subdivision_def divide_right_mono mult_left_mono Let_def) 
      have f3: "∀j<n. lower ((uniform_subdivision A n) ! j) = lower A + (upper A - lower A) * of_nat j / of_nat n"
        using assms by (simp add: uniform_subdivision_def divide_right_mono mult_left_mono Let_def) 
      have f4: "∀i<n. ∀j<n. i < j ⟶ lower A + (upper A - lower A) * of_nat (i + 1) / of_nat n ≤ lower A + (upper A - lower A) * of_nat j / of_nat n"
        using assms divide_right_mono mult_left_mono Suc_eq_plus1 Suc_leI add_le_cancel_left 
          interval_width_positive of_nat_0_le_iff of_nat_le_iff width_def
        by metis
      have "∀i<n. ∀j<n. i < j ⟶ upper ((uniform_subdivision A n) ! i) ≤ lower ((uniform_subdivision A n) ! j)"
        using f0 f2 f3 f4 by simp
    then show ?thesis by auto[1]
  qed
  then show ?thesis 
    unfolding non_overlapping_sorted_def cmp_non_overlapping_def 
    by (simp add: assms(1) sorted_wrt_iff_nth_less subdivision_length_n)
qed

text ‹We prove that our uniform subdivision meets the multi-interval type›

lemma uniform_subdivisions_valid_ainterval:
  assumes "0 < n" "0 < width A"
  shows "valid_mInterval_adj(uniform_subdivision A n)"
  using assms 
  unfolding valid_mInterval_adj_def 
  apply safe 
  subgoal using uniform_subdivisions_non_overlapping by blast
  subgoal using uniform_subdivisions_distinct by blast
  subgoal using non_empty_subdivision by blast
  done

lemma uniform_subdivisions_valid:
  assumes "0 < n"
  shows "check_is_uniform_subdivision A (uniform_subdivision A n)"
  unfolding check_is_uniform_subdivision_def Let_def
  apply (simp split: if_split) 
  apply safe
  subgoal using assms uniform_subdivisions_width subdivision_length_n 
    by (metis (mono_tags, lifting) Ball_set) 
  subgoal using assms contiguous_uniform_subdivision by blast
  subgoal using assms hd_lower_uniform_subdivision by blast
  subgoal using assms last_upper_uniform_subdivision by blast
  done

section ‹Refinement›

text ‹Let @{term ‹F(X)›} be an inclusion isotonic, Lipschitz, interval extension for @{term ‹X ⊆ Y›}. 
A refinement @{term ‹F⇩N(X)›} of @{term ‹F(X)›} is the union of interval values of @{term ‹X›} over 
the elements of a uniform subdivision of @{term ‹X›}›

definition refinement :: "('a::{linordered_field,lattice} interval⇒ 'a interval) ⇒ nat ⇒ 'a interval ⇒ 'a interval" where
‹refinement F N X = (interval_list_union (map F (uniform_subdivision X N)))›

definition check_is_refinement where
‹check_is_refinement F n As B = (let I = refinement F n As in lower B ≤ lower I ∧ upper I ≤ upper B)›

definition refinement_set :: "('a::{linordered_field,lattice} interval⇒ 'a interval) ⇒ nat ⇒ 'a interval ⇒ 'a set" where
‹refinement_set F N X = (set_of_interval_list (map F (uniform_subdivision X N)))›

text ‹The definition @{term "refinement"} refers to definition 6.3 in~\<^cite>‹"moore.ea:introduction:2009"›.›

text ‹The excess width of @{term "F(X)"} is  @{term "w(E(X)) = w(F(X)) - w(f(X))"}. The united 
extension @{term "f(x)"} for @{term "x ∈ X"} has zero excess width and we can compute @{term "f(x)"}
as closely as desired by computing refinements of an extension @{term "F(X)"}.›

definition "width_set s = Sup s - Inf s"

lemma width_set_bounded:
  fixes X :: ‹real set›
  assumes  ‹bdd_below X› ‹bdd_above X› 
  shows ‹∀ x ∈ X. ∀ x' ∈ X. dist x x' ≤ width_set X›
  using assms  sup_inf_dist_bounded
  unfolding width_set_def 
  by(simp)

lemma width_inclusion_isotonic_approx:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  "F is_interval_extension_of f"
  shows ‹0 ≤ width (F X) - width_set (f ` set_of X)›
  by (smt (verit, del_insts) assms(1) assms(2) inclusion_isotonic_inf 
          inclusion_isotonic_sup width_def width_set_def)

lemma diameter_width: 
  assumes ‹a ≤ b›
  shows ‹diameter {a..b} = width_set {a..b}›
  by (simp add: assms linorder_not_less diameter_Sup_Inf width_set_def)

lemma lipschitz_dist_diameter_limit:
  fixes S::‹'a::{metric_space, heine_borel} set›
  and   f::‹'a::{metric_space, heine_borel} ⇒ 'b::{metric_space, heine_borel}›
  assumes ‹C-lipschitz_on S f› and ‹bounded S› 
  shows ‹x ∈ (f `S) ⟹ y ∈ (f `S) ⟹ dist x y ≤ diameter (f` S)›
  using lipschitz_on_uniformly_continuous[of C S f, simplified assms]
        bounded_uniformly_continuous_image[of S f, simplified assms]
        diameter_bounded_bound[of "f ` S" x y]
  by simp 

definition excess_width_diameter :: "('a::preorder interval ⇒ real interval) ⇒ ('a ⇒ 'b::metric_space) ⇒ 'a interval ⇒ real" where
‹excess_width_diameter F f X = width(F X) - diameter (f ` set_of X)›

definition excess_width_set :: "('a::{minus,linorder,Inf,Sup} interval ⇒ 'a set) ⇒ ('a ⇒ 'a) ⇒ 'a interval ⇒ 'a" where
‹excess_width_set F f X = width_set(F X) - width_set (f ` set_of X)›

definition excess_width :: "('a::{minus,linorder,Inf,Sup} interval ⇒ 'a interval) ⇒ ('a ⇒ 'a) ⇒ 'a interval ⇒ 'a" where
‹excess_width F f X = width(F X) - width_set (f ` set_of X)›

text ‹The definition @{term "excess_width"} refers to definition 6.4 in~\<^cite>‹"moore.ea:introduction:2009"››

lemma  width_set_of: fixes X :: "real interval"
 shows width_set_upper_lower: ‹width_set (set_of X) = ¦(lower X) - (upper X)¦›
  by (simp add: width_set_def set_of_eq)
 
lemma width_set_dist:
  fixes f :: "real ⇒ real"
  shows "width_set ( set_of X) =  (dist (lower X) (upper X))"
  by(simp add:set_of_eq width_set_def dist_real_def)

lemma  diameter_of: fixes X :: "real interval"
  shows diameter_upper_lower: ‹diameter (set_of X) = ¦(lower X) - (upper X)¦›
  by (simp add: linorder_not_less set_of_eq) 

lemma diameter_dist:
  fixes X :: "real interval"
  shows "diameter ( set_of X) =  (dist (lower X) (upper X))"
  unfolding set_of_eq dist_real_def abs_real_def 
  using lower_le_upper[of X] diameter_closed_interval[of "lower X" "upper X"] 
  by argo 

lemma  bdd_below_f_set_of:
  fixes f :: "real ⇒ real"
  assumes "C-lipschitz_on X f"
  and ‹bounded X› and ‹X ≠ {}›
  shows ‹bdd_below (f ` X)›
  using assms atLeastAtMost_iff bdd_below.unfold bounded_imp_bdd_below image_def 
        lipschitz_bounded_image_real set_of_eq set_of_nonempty
  by simp

lemma  bdd_above_f_set_of:
  fixes f :: "real ⇒ real"
  assumes "C-lipschitz_on (X) f"  
  and ‹bounded X› and ‹X ≠ {}›
  shows ‹bdd_above (f ` X)›
  using assms atLeastAtMost_iff bdd_above.unfold bounded_imp_bdd_above image_def 
        lipschitz_bounded_image_real set_of_eq set_of_nonempty
  by simp

lemma diameter_image_dist: 
  fixes f::‹real ⇒ real›
  assumes ‹continuous_on (set_of X) f›
  shows ‹(∃ x∈ set_of X.  ∃ x'∈ set_of X . diameter (f ` set_of X) =  dist (f x) (f x'))›
  using assms compact_continuous_image[of "set_of X" f, simplified assms compact_set_of[of X]]  
        lower_le_upper[of X] diameter_closed_interval[of "f (lower X)" "f(upper X)", symmetric] 
        diameter_compact_attained[of "f ` set_of X"] set_f_nonempty[of f X] 
  by fastforce 

lemma excess_width_inf_diameter:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  "F is_interval_extension_of f" ‹ C-lipschitz_on (set_of X) f›
  shows ‹dist (Inf (f ` set_of X)) (lower (F X)) ≤ excess_width_diameter F f X› 
      unfolding dist_real_def abs_real_def excess_width_diameter_def  width_def
      using inclusion_isotonic_inf[of F f X, simplified assms]
            inclusion_isotonic_sup[of F f X, simplified assms]
            diameter_Sup_Inf[of "f ` set_of X", simplified assms lipschitz_on_continuous_on[of C "(set_of X)" f]
                                                compact_img_set_of[of X f], simplified] 
      by simp 

lemma excess_width_inf:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  "F is_interval_extension_of f" ‹ C-lipschitz_on (set_of X) f›
  shows ‹dist (Inf (f ` set_of X)) (lower (F X)) ≤ excess_width F f X› 
      unfolding dist_real_def abs_real_def excess_width_def  width_def
      using inclusion_isotonic_inf[of F f X, simplified assms]
            inclusion_isotonic_sup[of F f X, simplified assms]
      by (simp add: width_set_def)


lemma excess_width_sup_diameter:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  "F is_interval_extension_of f" ‹ C-lipschitz_on (set_of X) f›
  shows ‹dist (Sup (f ` set_of X)) (upper (F X)) ≤ excess_width F f X› 
      unfolding dist_real_def abs_real_def excess_width_diameter_def  width_def
      using inclusion_isotonic_inf[of F f X, simplified assms]
            inclusion_isotonic_sup[of F f X, simplified assms]
            diameter_Sup_Inf[of "f ` set_of X", simplified assms lipschitz_on_continuous_on[of C "(set_of X)" f]
                                                compact_img_set_of[of X f], simplified] 
      by (simp add: excess_width_def width_def width_set_def) 

lemma excess_width_sup:
  fixes F::‹real interval ⇒ real interval›
  assumes  "inclusion_isotonic F"  "F is_interval_extension_of f" ‹ C-lipschitz_on (set_of X) f›
  shows ‹dist (Sup (f ` set_of X)) (upper (F X)) ≤ excess_width F f X› 
      unfolding dist_real_def abs_real_def excess_width_def  width_def
      using inclusion_isotonic_inf[of F f X, simplified assms]
            inclusion_isotonic_sup[of F f X, simplified assms]
      by (simp add: width_set_def) 

text ‹If @{term "F(X)"} is an inclusion isotonic, Lipschitz, interval extension then the excess 
width of a refinement is of order @{term ‹1/N›}›

text ‹If @{term ‹X› } and @{term ‹X› } are intervals such that @{term ‹X ⊆ Y›}, then there is 
an interval @{term ‹E› } with @{term ‹lower E ≤ 0 ∧ 0 ≤ upper E› } such that 
@{term ‹Y = X + E›} and @{term ‹w(Y) = w(X) + w(E)›}.›

lemma interval_subset_width:
  fixes X Y :: "'a::{linordered_ring, lattice} interval"
  assumes "X ≤ Y"
  and X_def: "X = Interval(a, b)" and x_valid: "a ≤ b"
  and Y_def: "Y = Interval(c, d)" and y_valid: "c ≤ d"
  shows "∃ E. 0 ∈⇩i E ∧ Y = X + E ∧ width Y = width X + width E"
proof -
  have "c ≤ a" "b ≤ d" 
  proof -
      have leq: "lower Y ≤ lower X ∧ upper X ≤ upper Y" using assms(1) unfolding less_eq_interval_def by simp
      have X_bounds: "lower X = a" "upper X = b" unfolding X_def by (simp add: x_valid bounds_of_interval_eq_lower_upper)+
      have Y_bounds: "lower Y = c" "upper Y = d" unfolding Y_def by (simp add: y_valid bounds_of_interval_eq_lower_upper)+
      show "c ≤ a" "b ≤ d" using assms(1) X_bounds Y_bounds unfolding less_eq_interval_def by simp_all
  qed
  define e where "e = c - a"
  define f where "f = d - b"
  define E where "E = Interval(e, f)"
  have "0 ∈⇩i E" unfolding E_def  e_def f_def using ‹c ≤ a›  ‹b ≤ d› set_of_subset_iff 
    by (smt (verit, ccfv_SIG) diff_ge_0_iff_ge in_intervalI le_iff_diff_le_0 lower_bounds order.trans upper_bounds) 
  have "Y = X + E" 
  proof -
    have X_bounds: "lower X = a" "upper X = b" 
      unfolding X_def by (simp add: x_valid bounds_of_interval_eq_lower_upper)+
    have Y_bounds: "lower Y = c" "upper Y = d" 
      unfolding Y_def by (simp add: y_valid bounds_of_interval_eq_lower_upper)+
    have E_bound_1: "lower E = c - a" 
      unfolding E_def e_def f_def 
      using ‹b ≤ d› ‹c ≤ a› diff_left_mono diff_self lower_bounds order_trans
      by metis
    have E_bound_2:"upper E = d - b" 
      unfolding E_def e_def f_def 
      using ‹b ≤ d› ‹c ≤ a›  E_bound_1 ‹0 ∈⇩i E› diff_ge_0_iff_ge dual_order.trans in_bounds upper_bounds
      by metis 
    have add: "Interval(a,b) + Interval(c-a,d-b) = Interval(c,d)" 
      using X_bounds Y_bounds E_bound_1 E_bound_2
      by (simp add: E_def X_def Y_def e_def f_def interval_eqI)
    show ?thesis unfolding E_def X_def Y_def e_def f_def using add by simp
  qed
  have "width Y = width X + width E" unfolding width_def using E_def X_def Y_def ‹Y = X + E› e_def f_def by force 
  from ‹0 ∈⇩i E› ‹Y = X + E› ‹width Y = width X + width E› show ?thesis by auto[1]
qed

lemma excess_width_incl:
  fixes F :: "real interval ⇒ real interval" and X :: "real interval"
  assumes int: ‹F is_interval_extension_of f›
  and iso: "inclusion_isotonic F" 
  and "L-lipschitz_on (set_of X) f"
shows ‹ ∃ E . F X = Interval(Inf (f ` set_of X), Sup (f ` set_of X)) + E ›  
proof -
  have a0: ‹f ` (set_of X) ≠ {}› using in_intervalI by fastforce
  have a1: "Inf (f ` set_of X) ≤ Sup (f ` set_of X)" 
    using assms a0 inf_le_sup_image_real by simp
  have a2: ‹f ` (set_of X) ⊆ set_of (F X)› 
    using assms fundamental_theorem_of_interval_analysis by simp 
  have max: ‹Sup (f ` (set_of X)) ≤ Sup (set_of (F X))› 
    using assms(3) a0 a2 sup_image_le_real[of f X F] by blast   
  have max_interval: "Sup (f ` (set_of X)) ≤ upper (F X)" 
    using max sup_set_of by metis
  have min: ‹Inf (set_of (F X)) ≤ Inf (f ` (set_of X))›
    using assms(3) a0 a2 inf_image_le_real[of f X F] by blast 
  have min_interval: "lower (F X) ≤ Inf (f ` (set_of X))" 
    using min inf_set_of by metis
  have lower_min: "lower (Interval (Inf (f ` set_of X), Sup (f ` set_of X))) = Inf (f ` set_of X)" 
    using lower_bounds a1 by simp
  have upper_max: "upper (Interval (Inf (f ` set_of X), Sup (f ` set_of X))) = Sup (f ` set_of X)" 
    using upper_bounds a1 by simp
  have a3: "Interval(Inf (f ` set_of X), Sup (f ` set_of X)) ≤ F X" 
    using min_interval max_interval lower_min upper_max unfolding less_eq_interval_def by simp 
  have a4: "∃ E . Interval(Inf (f ` set_of X), Sup (f ` set_of X)) + E = F X" using a3 
    by (metis (no_types, opaque_lifting) bounds_of_interval_eq_lower_upper 
        bounds_of_interval_inverse interval_subset_width lower_le_upper)
  then show ?thesis by metis
qed  

lemma excess_interval_superset_interval:
  fixes F :: "real interval ⇒ real interval" and X :: "real interval"
  assumes int: ‹F is_interval_extension_of f›
  and iso: "inclusion_isotonic F" 
  and "L-lipschitz_on (set_of X) f"
  and ex: ‹ ∃ E . F X = Interval(Inf (f ` set_of X), Sup (f ` set_of X)) + E ›
shows ‹Interval(Inf (f ` set_of X), Sup (f ` set_of X)) ≤ F X›
proof -
  have lhs: "lower (F X) ≤ lower (Interval(Inf (f ` set_of X), Sup (f ` set_of X)))"
    using assms(1,2,3)  inf_image_le_real inf_le_sup_image_real  inf_set_of 
          fundamental_theorem_of_interval_analysis lower_bounds 
    by metis 
 have rhs: "upper (Interval(Inf (f ` set_of X), Sup (f ` set_of X))) ≤ upper (F X)"
   using assms(1,2,3)  inf_le_sup_image_real  sup_image_le_real sup_set_of
          fundamental_theorem_of_interval_analysis upper_bounds 
   by metis
  show ?thesis using lhs rhs unfolding less_eq_interval_def by simp
qed

lemma each_subdivision_width_order:
  fixes X :: "'a::{linordered_field,lattice,metric_space} interval"
  assumes "inclusion_isotonic F" "lipschitzI_on C U F" "F is_interval_extension_of f"
  and "set (uniform_subdivision X N) ⊆ U"  "0 < N" "Xs ∈ set (uniform_subdivision X N)" 
shows "width(F Xs) ≤ C * width (X) / of_nat N"
proof -
  have a0: "∀Xs ∈ set (uniform_subdivision X N). width (F Xs) ≤ C * width Xs"
    using assms(2) assms(4) lipschitzI_onD by blast
  have a1: "∀ Xs ∈ set (uniform_subdivision X N). width(F Xs) ≤ C * width (X) / of_nat N"
    using a0 assms(5) uniform_subdivisions_width[of N X] by simp 
  show ?thesis using a1 assms by simp
qed

lemma each_subdivision_excess_width_order:
  fixes X :: "real interval"
  assumes "inclusion_isotonic F" "lipschitzI_on C U F" "F is_interval_extension_of f"
  and "set (uniform_subdivision X N) ⊆ U"  "0 < N"
  and " L-lipschitz_on (set_of (interval_list_union (uniform_subdivision X N))) f " 
shows "∀ Xs ∈ set (uniform_subdivision X N) . excess_width F f Xs ≤ C * width (X) / of_nat N" 
proof -
  have a0: "∀Xs ∈ set (uniform_subdivision X N). width (F Xs) ≤ C * width Xs"
    using assms lipschitzI_onD by blast
  have a1: "∀ Xs ∈ set (uniform_subdivision X N). width(F Xs) ≤ C * width (X) / of_nat N"
    using a0 assms uniform_subdivisions_width[of N X] by simp
  have a2: "∀ Xs ∈ set (uniform_subdivision X N). excess_width F f Xs ≤ C * width (X) / of_nat N"
  proof - 
    have b0: "set (uniform_subdivision X N) ≠ {}" 
      using assms non_empty_subdivision by simp
    have b1: "∀ Xs ∈ set (uniform_subdivision X N) . 0 ≤ width_set (f ` set_of Xs)" 
    proof - 
       have c0: "∀ Xs ∈ set (uniform_subdivision X N) . set_of Xs ⊆ set_of (interval_list_union (uniform_subdivision X N))" 
        using assms interval_list_union_correct in_set_conv_nth non_empty_subdivision
        by metis
      then have c1: "∀ Xs ∈ set (uniform_subdivision X N) . set_of Xs ≠ {}" using in_intervalI by fastforce
      then have c2: "∀ Xs ∈ set (uniform_subdivision X N) . Inf (f ` set_of Xs) ≤ Sup (f ` set_of Xs)"  
        using assms c0 c1 inf_le_sup_image_real lipschitz_on_subset 
        by (metis inf_le_sup_image_real)
      then have c3: "∀ Xs ∈ set (uniform_subdivision X N) . 0 ≤ width_set (f ` set_of Xs)"
        by (simp add: width_set_def) 
      then show ?thesis by simp
    qed 
    have b2: "∀ Xs ∈ set (uniform_subdivision X N) . width(F Xs) - width_set (f ` set_of Xs) ≤ width(F Xs)"
      using b0 b1 assms inf_set_of lower_le_upper sup_set_of inf_le_sup_image_real image_is_empty
      by (simp add: width_set_def)
    then show ?thesis
      using a1 unfolding excess_width_def width_set_def by fastforce
    qed
  show ?thesis using assms a0 a1 a2 by simp
qed

text ‹The theorem @{thm "each_subdivision_width_order"} refers to Theorem 6.1 in~\<^cite>‹"moore.ea:introduction:2009"›.›

lemma sup_interval_max: 
  fixes X Y :: "'a::{linordered_ring, lattice} interval"
  shows "sup X Y = Interval(min (lower X) (lower Y), max (upper X) (upper Y))"
  using Interval.lower_sup Interval.upper_sup Interval_id inf_real_def sup_max
  by (metis inf_min)

lemma interval_inf_sup_lower: "inf (lower I1) (lower I2) = lower (sup I1 I2)" 
  unfolding sup_interval_def 
  by (metis (mono_tags, lifting) Interval.lower_sup sup_interval_def)

lemma interval_sup_sup_upper: "sup (upper I1) (upper I2) = upper (sup I1 I2)"
  unfolding sup_interval_def 
  by (metis (mono_tags, lifting) Interval.upper_sup sup_interval_def)

lemma interval_union_lower: 
  assumes "contiguous Xs" "Xs ≠ []"
  shows "lower (interval_list_union Xs) = lower (Xs!0)"
  using assms
proof(induction Xs rule:interval_list_union.induct)
  case 1
  then show ?case by simp
next
  case (2 I)
  then show ?case by simp
next
  case (3 I v va)
  have a0: "contiguous (v # va)" using 3 unfolding contiguous_def by auto
  have a1: "(v # va) ≠ []" by simp
  then show ?case
    unfolding sorted_wrt_lower_def 3 
  proof - 
    have b0: "lower ((I # v # va) ! 0) = lower I" by simp
    have b1: "lower I ≤ lower v" 
      using "3.prems" a1  
      unfolding contiguous_def 
      by (metis Suc_eq_plus1 add_diff_cancel_left' length_Cons less_Suc_eq_0_disj 
          lower_le_upper nth_Cons_0 nth_Cons_Suc plus_1_eq_Suc)
    show "lower (interval_list_union (I # v # va)) = lower ((I # v # va) ! 0)" 
      using b0 b1 3(2) interval_list_union.simps(3) "3.IH" Interval.lower_sup a0 a1 inf.orderE 
        nth_Cons_0 
      unfolding sorted_wrt_lower_def 
      by metis
  qed 
qed

lemma interval_union_upper: 
  assumes "contiguous Xs" "Xs ≠ []"
  shows "upper (interval_list_union Xs) = upper (last Xs)"
  using assms
proof(induction Xs rule:interval_list_union.induct)
  case 1
  then show ?case by simp
next
  case (2 I)
  then show ?case by simp
next
  case (3 I v va)
  have a0: "contiguous (v # va)" using 3 unfolding contiguous_def by auto
  have a1: "(v # va) ≠ []" by simp
  then show ?case
  proof - 
    have b0: "upper ((I # v # va) ! (length (I # v # va) - 1)) = upper (last (I # v # va))" 
      using last_conv_nth by fastforce
    have b1: "upper I ≤ upper v" using "3.prems" unfolding contiguous_def by auto
    show "upper (interval_list_union (I # v # va)) = upper (last (I # v # va))" 
      using b0 b1 interval_list_union.simps(3) "3.IH" a0 a1 interval_list_union.simps(3) 
        Interval.upper_sup last.simps
      by (metis (no_types, opaque_lifting) dual_order.trans min_list.cases sup_absorb2 sup_ge1)
  qed 
qed

lemma union_set:
  assumes "0 < n" 
  shows "interval_list_union (uniform_subdivision X n) = X"
  using assms
proof (induction n rule:nat_induct_non_zero)
  case 1
  then show ?case using uniform_subdivision_id  interval_list_union.simps(2) by metis
next
  case (Suc n)
  then show ?case
  proof (induction "uniform_subdivision X (Suc n)" rule:interval_list_union.induct)
    case 1
    then show ?case by (metis less_Suc_eq non_empty_subdivision)  
  next
    case (2 I)
    then show ?case using One_nat_def interval_list_union.simps(2) subdivision_length_n uniform_subdivision_id zero_less_Suc
      by metis 
  next
    case (3 I v va)
    then have a0: "lower I = lower X"  
      using hd_lower_uniform_subdivision assms 
      by (metis list.collapse list.simps(3) nth_Cons_0 zero_less_Suc)
    then have a1: "upper (last ( I # v # va)) = upper X" 
      using last_upper_uniform_subdivision[of "Suc n" X] assms "3.hyps"(2) by simp
    then have a2: "contiguous ( I # v # va)" 
      using contiguous_uniform_subdivision assms zero_less_Suc "3.hyps"(2) by metis 
    then have a3: "overlapping_ordered ( I # v # va)"
      using overlapping_uniform_subdivision  assms zero_less_Suc "3.hyps"(2) 
      by (simp add: overlapping_ordered_uniform_subdivision)
    then have a4: "∀i<length ( I # v # va) - 1. upper (( I # v # va) ! i) = lower (( I # v # va) ! (i + 1))"
        using a0 a2 unfolding contiguous_def by simp 
      have a5: "∀i<length ( I # v # va) - 1. lower (( I # v # va) ! i) ≤ lower (( I # v # va) ! (i + 1))"
        using a0 a2 contiguous_def lower_le_upper by metis 
      have a6: "∀i<length ( I # v # va) - 1. upper (( I # v # va) ! i) ≤ upper (( I # v # va) ! (i + 1))"
        using a0 a2 contiguous_def lower_le_upper by metis
      then show ?case 
      proof -
      have "lower (interval_list_union ( I # v # va)) = lower X" 
      proof -
        have c0: "lower (interval_list_union ( I # v # va)) = lower (sup I (interval_list_union (v # va)))"  
          using interval_list_union.simps(3) by metis     
        have c1: "lower (sup I (interval_list_union ( v # va))) = min (lower I) (lower (interval_list_union ( v # va)))"
          using inf_real_def sup_interval_def sup_interval_max sup_real_def 
          by (simp add: inf_min)
        have c2: "min (lower I) (lower (interval_list_union (v # va))) = lower I" 
          using 3 hd_lower_uniform_subdivision[of "Suc n" X] a0 
                contiguous_uniform_subdivision[of  X, simplified contiguous_def 3(2)[symmetric]] 
                interval_union_lower[of "( I # v # va)"] 
          by (metis a2 c0 c1 list.discI nth_Cons_0) 
        show ?thesis using a0 c0 c1 c2 by simp 
        qed
        moreover have "upper (interval_list_union ( I # v # va)) = upper X" 
        proof - 
          have c0: "upper (interval_list_union ( I # v # va)) = upper (sup I (interval_list_union ( v # va)))"
            using interval_list_union.simps(3) by metis
          have c1: "upper (sup I (interval_list_union (v # va))) = max (upper I) (upper (interval_list_union ( v # va)))"
            using inf_real_def sup_interval_def sup_interval_max sup_real_def 
            by (simp add: sup_max)
          have c2: "max (upper I) (upper (interval_list_union ( v # va))) = upper (last ( I # v # va))"
             using contiguous_uniform_subdivision[of  X, simplified contiguous_def 3(2)[symmetric]] 
                 interval_union_upper[of "( I # v # va)"] 
             by (metis a2 c0 c1 list.discI ) 
          show ?thesis using c0 c1 c2 "3.hyps"(2) last_upper_uniform_subdivision by auto[1]
        qed
      ultimately show ?thesis 
        using interval_eqI 3 by auto[1]
    qed
  qed
qed
 
lemma sum_list_less:
  assumes "list_all (λn. n ≤ (y::real)) xs"
  shows "sum_list xs ≤ y * length xs"
proof -
  have "∀x∈set xs. x ≤ y"
    using assms list_all_iff by metis
  hence "sum_list xs ≤ sum_list (replicate (length xs) y)"
    using sum_list_mono 
    by (simp add: order_less_imp_le sum_list_mono2)
  also have "... = y * length xs"
    by (simp add: sum_list_replicate)
  finally show ?thesis by simp
qed

lemma in_bounds2:
  fixes X Y :: "'a::{linordered_ring} interval"
  shows "x ∈⇩i X ∧ x ∈⇩i Y ⟹
     (lower Y ≤ lower X ∧ upper Y ≤ upper X ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X) ∨
     (lower X ≤ lower Y ∧ upper X ≤ upper Y ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X) ∨
     (lower Y ≤ lower X ∧ upper X ≤ upper Y ∧ lower Y ≤ lower X ∧ lower Y ≤ upper X) ∨ 
     (lower X ≤ lower Y ∧ upper Y ≤ upper X ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X)"
  apply(clarify)
  by (metis (full_types) in_bounds nle_le order.trans) 

lemma overlapping_width_sum:
  fixes X Y :: "'a::{linordered_ring, lattice} interval"
  assumes "overlapping [X,Y]"
  shows "width (sup X Y) ≤ width X + width Y"
proof - 
  have a0: "∀i<length [X, Y] - 1. ∃e. e ∈⇩i [X, Y] ! (i + 1) ∧ e ∈⇩i [X, Y] ! i"
    using assms unfolding overlapping_def by blast
  have a1: "(lower Y ≤ lower X ∧ upper Y ≤ upper X ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X) ∨
     (lower X ≤ lower Y ∧ upper X ≤ upper Y ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X) ∨
     (lower Y ≤ lower X ∧ upper X ≤ upper Y ∧ lower Y ≤ lower X ∧ lower Y ≤ upper X) ∨ 
     (lower X ≤ lower Y ∧ upper Y ≤ upper X ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X)"
    using assms in_bounds2[of _  X Y] unfolding overlapping_def by auto
  have a2: "(lower Y ≤ lower X ∧ upper Y ≤ upper X ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X) ⟹ width (sup X Y) ≤ width X + width Y"
    by (simp add: inf_min width_def)
  have a3: "(lower X ≤ lower Y ∧ upper X ≤ upper Y ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X) ⟹ width (sup X Y) ≤ width X + width Y"
    by (simp add: inf_min width_def)
  have a4: "(lower Y ≤ lower X ∧ upper X ≤ upper Y ∧ lower Y ≤ lower X ∧ lower Y ≤ upper X) ⟹ width (sup X Y) ≤ width X + width Y"
    by (simp add: inf_min sup_max width_def)
  have a5: "(lower X ≤ lower Y ∧ upper Y ≤ upper X ∧ lower X ≤ upper Y ∧ lower Y ≤ upper X) ⟹ width (sup X Y) ≤ width X + width Y"
    by (metis interval_width_positive le_add_same_cancel1 less_eq_interval_def sup.order_iff)
  show ?thesis using assms a0 a1 a2 a3 a4 a5 by blast
qed

lemma interval_list_union_width:
  fixes xs :: "'a::{linordered_ring, lattice} interval list"
  assumes "overlapping xs" "xs ≠ []" 
  shows "overlapping xs ⟹ width (interval_list_union xs) ≤ sum_list (map width xs)"
  using assms unfolding contiguous_def width_def
proof (induction xs rule: interval_list_union.induct)
  case 1
  then show ?case by simp
next
  case (2 I)
  then show ?case by simp
next
  case (3 I1 I2 Is)
  then show ?case unfolding overlapping_def
  proof -
    have a0: "width (interval_list_union (I1 # I2 # Is)) = width (sup I1 (interval_list_union (I2 # Is)))" 
      using interval_list_union.simps by simp
    have a1: "... ≤ width I1 + width (interval_list_union (I2 # Is))" 
    proof -
      have b0: "overlapping [I1, interval_list_union (I2 # Is)]" 
        using "3.prems" list.simps(3) list.size(3) list.size(4) interval_list_union_correct 
        unfolding overlapping_def 
        by (smt (verit, ccfv_threshold) One_nat_def Suc_eq_plus1 diff_add_inverse2  
            length_greater_0_conv less_one nth_Cons' subsetD) 
      show ?thesis 
        using overlapping_width_sum[of I1 "(interval_list_union (I2 # Is))", simplified b0] 
        by blast
    qed
    have a2: "... ≤ width I1 + sum_list (map width (I2 # Is))"
    proof -
      have b0: "(width I1 + width (interval_list_union (I2 # Is)) ≤ width I1 + sum_list (map width (I2 # Is))) = 
                (width (interval_list_union (I2 # Is)) ≤ sum_list (map width (I2 # Is)))" by simp
      have b1: "overlapping (I2 # Is)" using "3.prems" unfolding overlapping_def by force
      have b2: "I2 # Is ≠ []" by simp
      have b3: "width (interval_list_union (I2 # Is)) ≤ sum_list (map width (I2 # Is))" 
        using "3.IH" b1 b2 unfolding width_def by simp
      show ?thesis using b0 b3 by simp
    qed
    have a3: "... = sum_list (map width (I1 # I2 # Is))" by auto[1]
    show ?thesis using a0 a1 a2 a3 map_eq_conv width_def 
      by (smt (verit, ccfv_SIG) dual_order.trans)
  qed
qed

lemma map_non_zero_width:
  fixes U :: "'a::{linordered_idom} interval set"
  assumes "C-lipschitzI_on U F" "inclusion_isotonic F" "set xs ⊆ U"
  shows "∀x ∈ set xs. 0 ≤ width x  ⟶ 0 ≤ width (F x)"
proof
  fix x
  assume a0: "x ∈ set xs"
  show "0 ≤ width x  ⟶ 0 ≤ width (F x)"
  proof
    assume a1: "0 ≤ width x" 
    have a2: "width (F x) ≤ C * width x" using assms(1,3) a0 unfolding lipschitzI_on_def by blast 
    have a4: "width (F x) ≤ C * width x + 1" using assms(1,3) a0 unfolding lipschitzI_on_def by fastforce
    have "0 ≤ C * width x" using assms(1) a1 unfolding lipschitzI_on_def by simp
    show "0 ≤ width (F x)" using assms(1) a0 interval_width_positive unfolding lipschitzI_on_def interval_width_positive by blast
  qed
qed


lemma inclusion_isotonic_preserves_overlapping:
  assumes "inclusion_isotonic F"  "xs ≠ []"  "F is_interval_extension_of f" 
  shows "contiguous xs ⟹ overlapping (map F xs)" 
proof (induct xs rule: induct_list012)
  case 1
  then show ?case 
    unfolding overlapping_def by simp
next
  case (2 x)
  then show ?case 
    unfolding overlapping_def by simp
next
  case (3 x y zs)
  then show ?case 
  proof -
    have a0: "∀i<length (map F (x # y # zs)) - 1. ∃e. e ∈⇩i map F (x # y # zs) ! (i + 1) ∧ e ∈⇩i map F (x # y # zs) ! i"
    proof -
      have b0: "length (map F (x # y # zs)) ≥ 1" using "3.prems" by simp
      have b2: "∀i<length (x # y # zs) - 1. upper ((x # y # zs) ! i) = lower ((x # y # zs) ! (i + 1))" 
        using "3.prems" unfolding contiguous_def by auto[1]
      have b3: "∀i<length (x # y # zs) - 1. upper ((x # y # zs) ! i) ≤ upper ((x # y # zs) ! (i + 1))" 
        using "3.prems" unfolding contiguous_def by auto[1]
      have b4: "∀i<length (x # y # zs) - 1. lower ((x # y # zs) ! i) ≤ lower ((x # y # zs) ! (i + 1)) "
        using "3.prems" lower_le_upper b2 unfolding contiguous_def by metis
      have b5: "∀i<length (x # y # zs) - 1. f (upper ((x # y # zs) ! i)) = f (lower ((x # y # zs) ! (i + 1)))" 
        using b2 by simp
      have b6: "∀i<length (x # y # zs) - 1. f (upper ((x # y # zs) ! i)) ∈⇩i F  ((x # y # zs) ! i)" 
        using assms b2 b4 in_intervalI interval_of_in_eq  
        unfolding is_interval_extension_of_def inclusion_isotonic_def 
        by (metis lower_interval_of lower_le_upper upper_interval_of) 
      have b7: "∀i<length (x # y # zs) - 1. f (upper ((x # y # zs) ! i)) ∈⇩i F  ((x # y # zs) ! (i+1))" 
        using assms b2 b3 in_intervalI interval_of_in_eq  
        unfolding is_interval_extension_of_def inclusion_isotonic_def 
        by (metis lower_interval_of lower_le_upper upper_interval_of) 
      have b8: "∀i<length (x # y # zs) - 1. f (upper ((x # y # zs) ! i)) ∈⇩i F  ((x # y # zs) ! (i+1)) ∧ f (upper ((x # y # zs) ! i)) ∈⇩i F  ((x # y # zs) ! i)"
        using b6 b7 by blast
      show ?thesis using b8 apply simp 
        by (metis One_nat_def Suc_eq_plus1 le_simps(2) list.map(2) list.size(4) nth_map order_less_le)
    qed
    show ?thesis using a0 unfolding overlapping_def by simp
  qed 
qed
  
lemma bounded_image_of:
  fixes f::‹real ⇒ real›
  assumes ‹L-lipschitz_on (set_of X) f›
  shows ‹bounded (f ` set_of X)›
  using lipschitz_bounded_image_real[of "set_of X" L f] assms 
  using bounded_set_of set_of_nonempty by blast

lemma dist_le_diameter:   
  fixes f::‹real ⇒ real ›
  assumes  ‹ C-lipschitz_on (set_of X) f›
  shows ‹dist (f (upper X)) (f (lower X)) ≤ diameter (f ` set_of X)›
  using diameter_bounded_bound[of "f` set_of X" "f (upper X)" "f (lower X)", 
        simplified  
        bounded_image_of[of C X f, simplified assms]]
  by simp 

lemma excess_width_inf_sup:
  fixes X :: "real interval" and f::‹real ⇒ real›
  assumes ‹continuous_on (set_of X) f›
  shows "Inf (f ` set_of X) - lower (F X) + upper (F X) - Sup (f ` set_of X) ≤ excess_width F f X"
  using diameter_Sup_Inf[of "f ` set_of X", simplified compact_img_set_of set_f_nonempty assms]
  unfolding excess_width_def  width_def width_set_def set_of_eq 
  by simp
                                           
lemma excess_width_lower_bound:
  fixes X :: "real interval"
  assumes  "inclusion_isotonic F"  "F is_interval_extension_of f"  ‹continuous_on (set_of X) f›
  shows  "Inf (f ` set_of X) - lower (F X) ≤ excess_width F f X"
proof -
  have a0: "0 ≤ upper (F X) - Sup (f ` set_of X)" 
    using assms(1) assms(2) diff_ge_0_iff_ge inclusion_isotonic_sup
    by metis 
  show ?thesis using a0 excess_width_inf_sup assms
    by (smt (verit, ccfv_threshold)) 
qed

lemma excess_width_upper_bound:
  fixes X :: "real interval"
  assumes  "inclusion_isotonic F"  "F is_interval_extension_of f" ‹continuous_on (set_of X) f›
  shows  "upper (F X) - Sup (f ` set_of X) ≤ excess_width F f X"
proof -
  have a0: "0 ≤ Inf (f ` {lower X..upper X}) - lower (F X)" 
    using assms(1) assms(2) diff_ge_0_iff_ge inclusion_isotonic_sup set_of_eq 
      inclusion_isotonic_inf
    by metis 
  show ?thesis using a0 excess_width_inf_sup assms unfolding set_of_eq
    by (smt (verit, ccfv_threshold))   
qed

lemma lipschitz_excess_width_lower_bound:
  fixes X :: "real interval"
  assumes "inclusion_isotonic F" "lipschitzI_on C U F" "F is_interval_extension_of f"
  and "set (uniform_subdivision X N) ⊆ U"  "N = 1"
  and "L-lipschitz_on (set_of (interval_list_union (uniform_subdivision X N))) f "  
  shows  "Inf (f ` set_of X) - lower (F X) ≤ C * width X"
proof-
  have a0: "excess_width F f X ≤ C * width X"
    using each_subdivision_excess_width_order[of F C U f X N L, simplified assms] 
      assms(4) assms(5) assms(6) div_by_1 insert_iff less_numeral_extra(1) list.set(2) of_nat_1 
      uniform_subdivision_id
    by metis 
  have a1: "Inf (f ` set_of X) - lower (F X) ≤ excess_width F f X"
    using excess_width_lower_bound[of F f X, simplified assms]
    by (metis assms(5) assms(6) lipschitz_on_continuous_on union_set zero_less_one) 
  show ?thesis using a0 a1 by simp
qed

lemma lipschitz_excess_width_upper_bound:
  fixes X :: "real interval"
  assumes "inclusion_isotonic F" "lipschitzI_on C U F" "F is_interval_extension_of f"
  and "set (uniform_subdivision X N) ⊆ U"  "N = 1"
  and "L-lipschitz_on (set_of (interval_list_union (uniform_subdivision X N))) f "  
  shows  "upper (F X) - Sup (f ` set_of X) ≤ C * width X"
proof-
  have a0: "excess_width F f X ≤ C * width X"
    using each_subdivision_excess_width_order[of F C U f X N L, simplified assms] 
      assms(4) assms(5) assms(6) div_by_1 insert_iff less_numeral_extra(1) list.set(2) of_nat_1 
      uniform_subdivision_id
    by metis 
  have a1: "upper (F X) - Sup (f ` set_of X) ≤ excess_width F f X"
    using excess_width_upper_bound[of F f X, simplified assms] 
    by (metis assms(5) assms(6) lipschitz_on_continuous_on union_set zero_less_one) 
  show ?thesis using a0 a1 by simp
qed

lemma excess_width_bound_inf:
  fixes X :: "real interval"
  assumes excess_width_bound: ‹excess_width F f X ≤ k›
  and     inclusion_isotonic: ‹inclusion_isotonic F›
  and     interval_extension: ‹F is_interval_extension_of f›
  shows ‹Inf (f ` set_of X) - k ≤ lower (F X)›
  using excess_width_bound[simplified excess_width_def width_def width_set_def]
        inclusion_isotonic interval_extension
  by (smt (verit, best) inclusion_isotonic_sup) 

lemma excess_width_bound_sup:
  fixes X :: "real interval"
  assumes excess_width_bound: ‹excess_width F f X ≤ k›
  and     inclusion_isotonic: ‹inclusion_isotonic F›
  and     interval_extension: ‹F is_interval_extension_of f›
  shows ‹upper (F X) ≤ Sup (f ` set_of X) + k›
  using excess_width_bound[simplified excess_width_def width_def width_set_def]
        inclusion_isotonic interval_extension
  by (smt (verit, best) inclusion_isotonic_inf) 

lemma set_of_interval_list_subset_inf_sup:
  assumes non_empty: ‹XS ≠ ([]::real interval list)›
shows ‹set_of_interval_list XS ⊆ {Min(set (map lower XS))..Max(set (map upper XS))}›
  using assms unfolding set_of_interval_list_def  
proof(induction XS rule:list_nonempty_induct)
  case (single x)
  then show ?case by(simp add:set_of_eq)
next
  case (cons x xs)
  then show ?case 
    apply(simp add:set_of_eq)
    by fastforce 
qed

lemma lower_bound_F_inf: 
  assumes non_empty: ‹XS ≠ ([]::real interval list)›
  and     inclusion_isotonic: ‹inclusion_isotonic F›
  and     interval_extension: ‹F is_interval_extension_of f›
  and     sorted_lower: ‹sorted_wrt_lower XS›
  and     lipschitz:  ‹0 ≤ C› ‹C-lipschitz_on ((set_of_interval_list XS)) f›
  and     excess_width_bounded: ‹(Max (set ((map (excess_width F f)) XS))) ≤ k›
shows ‹(Inf (f ` (set_of_interval_list XS))) - k ≤ Inf (set_of_interval_list (map F XS))›
 using assms proof(induction XS rule:list_nonempty_induct)
  case (single x)
  then show ?case 
    using excess_width_bound_inf[of F f x k]
    unfolding set_of_interval_list_def
    by (simp add: inf_set_of)
next
  case (cons x xs)
  then show ?case 
    using excess_width_bound_inf[of F f x]
    unfolding set_of_interval_list_def 
    apply(simp)
    apply(fold set_of_interval_list_def)
    apply(subst image_Un)
    apply(subst cInf_union_distrib)
    subgoal 
      by simp
    subgoal 
      apply(simp add: set_of_eq)
      by (meson bounded_imp_bdd_below compact_Icc compact_continuous_image compact_imp_bounded 
                lipschitz_on_continuous_on lipschitz_on_subset sup_ge1) 
    subgoal 
      unfolding set_of_interval_list_def 
      by (metis image_is_empty set_of_interval_list_def set_of_interval_list_nonempty)
    subgoal 
      using compact_set_of_interval_list[of XS]
            compact_imp_bounded[of " (set_of_interval_list XS)"]
      by (meson bounded_imp_bdd_below compact_continuous_image compact_imp_bounded 
                compact_set_of_interval_list lipschitz_on_continuous_on lipschitz_on_mono sup_ge2) 
    subgoal  
      apply(subst cInf_union_distrib)
      subgoal 
        by simp 
      subgoal 
        by (meson bdd_below_set_of) 
      subgoal 
        by(simp add: set_of_interval_list_nonempty) 
      subgoal 
        using set_of_interval_list_bdd_below by simp
      subgoal 
      proof -
        assume a1: "xs ≠ []"
        assume a2: "⟦sorted_wrt_lower xs; C-lipschitz_on (set_of_interval_list xs) f⟧ ⟹ Inf (f ` set_of_interval_list xs) - k ≤ Inf (set_of_interval_list (map F xs))"
        assume a3: "sorted_wrt_lower (x # xs)"
        assume a4: "C-lipschitz_on (set_of x ∪ set_of_interval_list xs) f"
        assume a5: "excess_width F f x ≤ k ∧ (∀a∈set xs. excess_width F f a ≤ k)"
        assume a6: "⋀k. excess_width F f x ≤ k ⟹ Inf (f ` set_of x) - k ≤ lower (F x)"
        have f7: "sorted_wrt_lower xs"
          using a3 a1 sorted_wrt_lower_unroll by blast
        have f8: "Inf (set_of (F x)) = lower (F x)"
          using inf_set_of by blast
        have f9: "C-lipschitz_on (set_of_interval_list xs) f"
          using a4 lipschitz_on_subset by blast
        have f10: "inf (Inf (f ` set_of x)) (Inf (f ` set_of_interval_list xs)) ≤ Inf (f ` set_of x)"
          using inf_le1 by blast
        have f11: "inf (Inf (f ` set_of x)) (Inf (f ` set_of_interval_list xs)) ≤ Inf (f ` set_of_interval_list xs)"
          using inf_le2 by blast
        have "Inf (f ` set_of x) - excess_width F f x ≤ lower (F x)"
          using a6 by blast
        have "inf (Inf (f ` set_of x)) (Inf (f ` set_of_interval_list xs)) - k ≤ Inf (set_of (F x)) 
            ∧ inf (Inf (f ` set_of x)) (Inf (f ` set_of_interval_list xs)) - k ≤ Inf (set_of_interval_list (map F xs))"
          using f11 f10 f9 f8 f7 a5 a2 
          using ‹Inf (f ` set_of x) - excess_width F f x ≤ lower (F x)› by linarith 
        then show ?thesis by simp 
      qed
      done
    done
qed

lemma upper_bound_F_sup: 
  assumes non_empty: ‹XS ≠ ([]::real interval list)›
  and     inclusion_isotonic: ‹inclusion_isotonic F›
  and     interval_extension: ‹F is_interval_extension_of f›
  and     sorted_upper: ‹sorted_wrt_upper XS›
  and     lipschitz:  ‹0 ≤ C› ‹C-lipschitz_on ((set_of_interval_list XS)) f›
  and     excess_width_bounded: ‹(Max (set ((map (excess_width F f)) XS))) ≤ k›
shows ‹Sup (set_of_interval_list (map F XS)) ≤ (Sup (f ` (set_of_interval_list XS))) + k ›
 using assms proof(induction XS rule:list_nonempty_induct)
  case (single x)
  then show ?case 
    using excess_width_bound_sup[of F f x k]
    unfolding set_of_interval_list_def   
    by (simp add: sup_set_of)
next
  case (cons x xs)
  then show ?case 
    using excess_width_bound_inf[of F f x]
    unfolding set_of_interval_list_def 
    apply(simp)
    apply(fold set_of_interval_list_def)
    apply(subst image_Un)
    apply(subst cSup_union_distrib)
    subgoal 
      by simp
    subgoal 
      by(simp add: set_of_eq)
    subgoal 
      by(simp add: set_of_interval_list_nonempty) 
    subgoal 
      using set_of_interval_list_bdd_above by simp 
    subgoal  
      apply(subst cSup_union_distrib)
      subgoal 
        by simp 
      subgoal  
        by (meson bdd_above_mono bdd_above_set_of fundamental_theorem_of_interval_analysis) 
      subgoal 
        by(simp add: set_of_interval_list_nonempty) 
      subgoal 
        using set_of_interval_list_bdd_above 
        by (meson bounded_imp_bdd_above compact_continuous_image compact_imp_bounded 
           compact_set_of_interval_list lipschitz_on_continuous_on lipschitz_on_subset sup_ge2) 
      subgoal  
        apply(auto)[1] 
        subgoal 
          by (smt (verit) excess_width_def inclusion_isotonic_inf sup_ge1 sup_set_of width_def width_set_def)
        subgoal 
          by (smt (verit, ccfv_threshold) lipschitz_on_subset sorted_wrt_upper_unroll sup_ge2)
        done 
      done
    done
qed

lemma Inf_interval_list_approx:  assumes non_empty: ‹XS ≠ ([]::real interval list)›
  and     inclusion_isotonic: ‹inclusion_isotonic F›
  and     interval_extension: ‹F is_interval_extension_of f›
  and     sorted_upper: ‹sorted_wrt_upper XS›
  and     lipschitz:  ‹0 ≤ C› ‹C-lipschitz_on ((set_of_interval_list XS)) f›
  and     excess_width_bounded: ‹(Max (set ((map (excess_width F f)) XS))) ≤ k›
shows " Inf (set_of_interval_list (map F XS)) ≤ Inf (f ` set_of_interval_list XS) "
 using assms proof(induction XS rule:list_nonempty_induct)
  case (single x)
  then show ?case 
    apply(simp add: set_of_interval_list_def set_of_eq)
    by (metis inclusion_isotonic_inf set_of_eq) 
next
  case (cons x xs)
  then show ?case 
    apply(simp add: set_of_interval_list_def set_of_eq)
    apply(subst image_Un)
    apply(subst cInf_union_distrib)
    subgoal 
      by simp
    subgoal 
      by simp
    subgoal 
      proof -
        assume "xs ≠ []"
        then have "set_of_interval_list (map F xs) ≠ {}"
          by (simp add: set_of_interval_list_nonempty)
        then show ?thesis
          by (simp add: set_of_eq set_of_interval_list_def)
      qed 
    subgoal 
    proof -
      have "∀is. bdd_below (set_of_interval_list is::real set)"
        by (simp add: bounded_imp_bdd_below compact_imp_bounded compact_set_of_interval_list)
      then show ?thesis
        by (simp add: set_of_eq set_of_interval_list_def)
    qed 
    subgoal 
      apply(subst cInf_union_distrib)
      subgoal 
        by simp 
      subgoal 
        by (meson bounded_imp_bdd_below compact_Icc compact_continuous_image compact_imp_bounded 
                  lipschitz_on_continuous_on lipschitz_on_subset sup_ge1) 
      subgoal       
      proof -
        assume "xs ≠ []"
        then have "set_of_interval_list xs ≠ {}"
          by (simp add: set_of_interval_list_nonempty)
        then show ?thesis
          by (simp add: set_of_eq set_of_interval_list_def)
      qed
      subgoal       
      proof -
        assume "C-lipschitz_on ({lower x..upper x} ∪ foldr (λx. (∪) {lower x..upper x}) xs {}) f"
        then have "C-lipschitz_on ({lower x..upper x} ∪ set_of_interval_list xs) f"
          by (simp add: set_of_eq set_of_interval_list_def)
        then have "bounded (f ` set_of_interval_list xs)"
          by (metis compact_imp_bounded compact_set_of_interval_list lipschitz_bounded_image_real lipschitz_on_subset sup_ge2)
        then show ?thesis
          by (simp add: bounded_imp_bdd_below set_of_eq set_of_interval_list_def)
      qed
      subgoal
        apply(simp, rule conjI)
        subgoal 
          using inclusion_isotonic_inf[of F f x, simplified assms set_of_eq, simplified]  
          by (smt (verit, ccfv_threshold) inclusion_isotonic_inf le_infI1 set_of_eq)     
        subgoal 
        proof -
          assume a1: "xs ≠ []"
          assume a2: "⟦sorted_wrt_upper xs; C-lipschitz_on (foldr (λx. (∪) {lower x..upper x}) xs {}) f⟧ ⟹ Inf (foldr (λx. (∪) {lower x..upper x}) (map F xs) {}) ≤ Inf (f ` foldr (λx. (∪) {lower x..upper x}) xs {})"
          assume a3: "sorted_wrt_upper (x # xs)"
          assume "C-lipschitz_on ({lower x..upper x} ∪ foldr (λx. (∪) {lower x..upper x}) xs {}) f"
          then have "C-lipschitz_on (foldr (λi. (∪) {lower i..upper i}) xs {}) f"
            using lipschitz_on_mono by blast
          then show ?thesis
            using a3 a2 a1 by (meson le_infI2 sorted_wrt_upper_unroll)
        qed 
        done
      done 
    done 
qed

lemma Sup_interval_list_approx:  assumes non_empty: ‹XS ≠ ([]::real interval list)›
  and     inclusion_isotonic: ‹inclusion_isotonic F›
  and     interval_extension: ‹F is_interval_extension_of f›
  and     sorted_lower: ‹sorted_wrt_lower XS›
  and     lipschitz:  ‹0 ≤ C› ‹C-lipschitz_on ((set_of_interval_list XS)) f›
  and     excess_width_bounded: ‹(Max (set ((map (excess_width F f)) XS))) ≤ k›
shows "Sup (f ` set_of_interval_list XS) ≤ Sup (set_of_interval_list (map F XS))"
 using assms proof(induction XS rule:list_nonempty_induct)
  case (single x)
  then show ?case 
    apply(simp add: set_of_interval_list_def set_of_eq)
    by (metis inclusion_isotonic_sup set_of_eq) 
next
  case (cons x xs)
  then show ?case 
    apply(simp add: set_of_interval_list_def set_of_eq)
    apply(subst image_Un)
    apply(subst cSup_union_distrib)
    subgoal 
      by simp
    subgoal 
      by (meson bounded_imp_bdd_above compact_Icc compact_continuous_image compact_imp_bounded lipschitz_on_continuous_on lipschitz_on_subset sup_ge1) 
    subgoal 
    proof -
      assume a1: "xs ≠ []"
      have f2: "∀R Ra is isa f fa. ((R::real set) ≠ Ra ∨ is ≠ isa ∨ (∃R i. (i::real interval) ∈ set is ∧ f i R ≠ fa i R)) ∨ foldr f is R = foldr fa isa Ra"
        by (meson foldr_cong)
      obtain ii :: "(real interval ⇒ real set ⇒ real set) ⇒ (real interval ⇒ real set ⇒ real set) ⇒ real interval list ⇒ real interval" and RR :: "(real interval ⇒ real set ⇒ real set) ⇒ (real interval ⇒ real set ⇒ real set) ⇒ real interval list ⇒ real set" where
        "∀x0 x1 x3. (∃v6 v7. v7 ∈ set x3 ∧ x1 v7 v6 ≠ x0 v7 v6) = (ii x0 x1 x3 ∈ set x3 ∧ x1 (ii x0 x1 x3) (RR x0 x1 x3) ≠ x0 (ii x0 x1 x3) (RR x0 x1 x3))"
        by moura
      then have "∀R Ra is isa f fa. (R ≠ Ra ∨ is ≠ isa ∨ ii fa f is ∈ set is ∧ f (ii fa f is) (RR fa f is) ≠ fa (ii fa f is) (RR fa f is)) ∨ foldr f is R = foldr fa isa Ra"
        using f2 by presburger
      then show ?thesis
        using a1 by (smt (z3) image_is_empty set_of_eq set_of_interval_list_def set_of_interval_list_nonempty)
    qed 
    subgoal 
    proof -
      assume "C-lipschitz_on ({lower x..upper x} ∪ foldr (λx. (∪) {lower x..upper x}) xs {}) f"
      then have "C-lipschitz_on ({lower x..upper x} ∪ set_of_interval_list xs) f"
        by (simp add: set_of_eq set_of_interval_list_def)
      then have "bounded (f ` set_of_interval_list xs)"
        by (metis (no_types) compact_imp_bounded compact_set_of_interval_list lipschitz_bounded_image_real lipschitz_on_subset sup_ge2)
      then show ?thesis
        by (simp add: bounded_imp_bdd_above set_of_eq set_of_interval_list_def)
    qed 
    subgoal 
      apply(subst cSup_union_distrib)
      subgoal 
      by simp 
     subgoal 
       by (meson bdd_above_Icc)
      subgoal       
      proof -
        assume "xs ≠ []"
       then have "set_of_interval_list (map F xs) ≠ {}"
          by (simp add: set_of_interval_list_nonempty)
        then show ?thesis
          by (simp add: set_of_eq set_of_interval_list_def)
      qed 
      subgoal       
      proof -
        have "∀is. bdd_above (set_of_interval_list is::real set)"
          by (simp add: bounded_imp_bdd_above compact_imp_bounded compact_set_of_interval_list)
        then show ?thesis
          by (simp add: set_of_eq set_of_interval_list_def)
      qed 
      subgoal
        apply(simp, rule conjI)
        subgoal 
          using inclusion_isotonic_sup[of F f x, simplified assms set_of_eq, simplified] le_supI1
          by auto
        subgoal
        proof -
          assume a1: "xs ≠ []"
          assume a2: "⟦sorted_wrt_lower xs; C-lipschitz_on (foldr (λx. (∪) {lower x..upper x}) xs {}) f⟧ ⟹ Sup (f ` foldr (λx. (∪) {lower x..upper x}) xs {}) ≤ Sup (foldr (λx. (∪) {lower x..upper x}) (map F xs) {})"
          assume a3: "sorted_wrt_lower (x # xs)"
          assume a4: "C-lipschitz_on ({lower x..upper x} ∪ foldr (λx. (∪) {lower x..upper x}) xs {}) f"
          have f5: "sorted_wrt_lower xs"
            using a3 a1 sorted_wrt_lower_unroll by blast
          have f6: "Sup (foldr (λi. (∪) {lower i..upper i}) (map F xs) {}) ≤ sup (upper (F x)) (Sup (foldr (λi. (∪) {lower i..upper i}) (map F xs) {}))"
            using sup_ge2 by blast
          have "C-lipschitz_on (foldr (λi. (∪) {lower i..upper i}) xs {}) f"
            using a4 lipschitz_on_mono by blast
          then show ?thesis             
            using f6 f5 a2 by linarith
        qed 
        done
      done 
    done 
qed


lemma map_inclusion_isotonic_excess_width_bounded:
  assumes non_empty: ‹XS ≠ ([]::real interval list)›
  and     inclusion_isotonic: ‹inclusion_isotonic F›
  and     interval_extension: ‹F is_interval_extension_of f›
  and     sorted_lower: ‹sorted_wrt_lower XS›   (* should not be required, relaxing this assumption requires updating several helper lemmata *)
  and     sorted_upper: ‹sorted_wrt_upper XS›(* should not be required, relaxing this assumption requires updating several helper lemmata *)
  and     lipschitz:  ‹C-lipschitz_on ((set_of_interval_list XS)) f›
  and     excess_width_bounded: ‹(Max (set ((map (excess_width F f)) XS))) ≤ k›
shows ‹width_set (set_of_interval_list (map F XS)) - width_set (f ` (set_of_interval_list XS)) ≤ 2 * k›
 and  ‹width_set (set_of_interval_list (map F XS)) - width_set (f ` (set_of_interval_list XS)) ≥ 0›
  subgoal (* ‹width_set (set_of_interval_list (map F XS)) - width_set (f ` (set_of_interval_list XS)) ≤ 2 * k› *)
    unfolding width_set_def
    using lipschitz_on_nonneg[of C "((set_of_interval_list XS))" f, simplified assms, simplified]
          lower_bound_F_inf[of XS F f C k, simplified assms, simplified]
          upper_bound_F_sup[of XS F f C k, simplified assms, simplified]
    by(simp) 
  subgoal (* ‹width_set (set_of_interval_list (map F XS)) - width_set (f ` (set_of_interval_list XS)) ≥ 0› *)    
    unfolding width_set_def
    using lipschitz_on_nonneg[of C "((set_of_interval_list XS))" f, simplified assms, simplified]
          Inf_interval_list_approx[of XS F f C k, simplified assms, simplified]
          Sup_interval_list_approx[of XS F f C k, simplified assms, simplified]
    by simp  
  done

lemma max_subdivision_excess_width_order:
  fixes X :: "real interval"
  assumes "inclusion_isotonic F" "lipschitzI_on C U F" "F is_interval_extension_of f"
  and "set (uniform_subdivision X N) ⊆ U"  "0 < N"
  and " L-lipschitz_on (set_of_interval_list (uniform_subdivision X N)) f " 
shows ‹Max (set (map (excess_width F f) (uniform_subdivision X N))) ≤ C * width X / real N›
proof(cases " (set (map (excess_width F f) (uniform_subdivision X N))) = {}")
  case True
  then show ?thesis 
   using non_empty_subdivision[of N X, simplified assms, simplified]
   by simp
next
  case False
  then show ?thesis 
    apply(subst set_map)   
    using each_subdivision_excess_width_order[of F C U f X N L, simplified assms, simplified]
          set_of_interval_list_set_eq_interval_list_union_contiguous[of "(uniform_subdivision X N)", simplified contiguous_uniform_subdivision[of X N] non_empty_subdivision[of N X, simplified assms, simplified], simplified]
    using assms(6) by auto[1] 
qed

lemma set_of_interval_list_set_eq_interval_list_union_contiguous:
  assumes non_empty: ‹XS ≠ ([]::real interval list)›
  and     contiguous: ‹contiguous XS›
shows ‹set_of_interval_list XS = set_of (interval_list_union XS)›
  using interval_list_union_contiguous[of XS, simplified assms, simplified]
        set_of_interval_list_contiguous[of XS,simplified assms, simplified]
        contiguous_non_overlapping[of XS, simplified assms, simplified]
        non_overlapping_implies_sorted_wrt_upper[of XS]
        non_overlapping_implies_sorted_wrt_lower[of XS]
  interval_list_union_contiguous_lower[of XS] 
  interval_list_union_contiguous_upper[of XS]
  using set_of_eq non_empty by metis


lemma width_eq_wdith_set:
  fixes X :: ‹('a::{conditionally_complete_lattice, minus, preorder}) interval›
  shows  ‹width X = width_set (set_of X)›
  unfolding width_def set_of_eq width_set_def by(simp)

lemma width_zero_lower_upper:
  fixes X :: "real interval"
  assumes ‹width X = 0›
  shows ‹lower X = upper X›
  using assms width_def[of X]
  by simp

lemma width_zero_mk_interval:
  fixes X :: "real interval"
  assumes ‹width X = 0›
  shows ‹∃ x. X = mk_interval(x,x)›
  using assms width_def[of X]
  unfolding mk_interval'
  by (auto, metis Interval_id)

lemma width_zero_interval_of:
  fixes X :: "real interval"
  assumes ‹width X = 0›
  shows ‹∃ x. X = interval_of x›
  using assms width_def[of X]
  by (metis eq_iff_diff_eq_0 interval_eqI lower_interval_of upper_interval_of) 

lemma width_zero_interval_extension:
  fixes F :: "real interval ⇒ real interval"
  assumes ‹F is_interval_extension_of f›
  and     ‹width X = 0›
shows ‹width (F X) = 0›
  using assms width_zero_interval_of[of X, simplified assms, simplified]
  unfolding is_interval_extension_of_def
  by (metis add_0 add_diff_cancel lower_interval_of upper_interval_of width_def)

section ‹Lipschitz Interval Inclusive› 

text ‹If @{term ‹F›} is a natural interval extension of a real valued rational function with 
@{term ‹F(X)›} defined for @{term ‹X ⊆ Y›} where @{term ‹X›} and @{term ‹Y›} are intervals or
n-dimentional interval vectors then @{term ‹F›} is Lipschitz in @{term ‹Y›}›
 
lemma interval_extension_bounded:
  fixes F :: "real interval ⇒ real interval"
  assumes ‹F is_interval_extension_of f›
  and     ‹(width (F X)) / (width X) ≤ L›
shows "width (F X) ≤ L * width X"
proof(cases  "width X = 0")
  case True
  then show ?thesis 
    using width_zero_interval_extension[of F f X, simplified True assms, simplified]
    by auto
next
  case False
  then show ?thesis 
    using assms interval_width_positive[of X]
    by (metis mult.commute mult_right_mono nonzero_mult_div_cancel_left times_divide_eq_right) 
qed

lemma lipschitz_on_implies_lipschitzI_on:
  fixes F :: "real interval ⇒ real interval"
  assumes ‹F is_interval_extension_of f›
  and ‹C-lipschitz_on X f›
  and ‹⋃ (set_of ` Y) ⊆ X›
  and ‹0 ≤ L›
  and ‹∀ y ∈ Y. (width (F y)) / (width y) ≤ L›
shows "L-lipschitzI_on Y F"
  unfolding lipschitzI_on_def
  using assms interval_extension_bounded
  by(auto)

lemma lipschitz_on_implies_lipschitzI_on2:
  fixes f :: ‹real ⇒ real›
  assumes ‹S ≠ []› and ‹0 ≤ C› 
   and ‹F is_interval_extension_of f›
   and ‹0 ≤ L›
   and ‹∀ y ∈ (set S). (width (F y)) / (width y) ≤ L›
   and ‹C-lipschitz_on (set_of (interval_list_union (S))) f ›
  shows ‹L-lipschitzI_on (set (S)) F›
  apply(rule lipschitzI_onI)
  subgoal using assms interval_extension_bounded by blast  
  subgoal using assms by blast  
  done 


lemma width_img_Max:
  assumes ‹finite S›
  shows ‹∀x∈S. width (F x) ≤ Max (width ` F ` S)›
  using assms by auto 
lemma width_Min:
  assumes ‹finite S›
  shows ‹∀x∈S. Min (width ` S) ≤ width x›
  using assms by auto 

lemma lipschitzI_on_le_interval:
  fixes F  :: ‹real interval ⇒ real interval›
  assumes inc_isontonic_F: ‹inclusion_isotonic F›
      and lipschitzI_F:    ‹C-lipschitzI_on {X} F›
      and interval_inc:    ‹x ≤ X›
    shows ‹width (F x) ≤ C * width X›
  using assms
  unfolding inclusion_isotonic_def lipschitzI_on_def 
            width_def less_eq_interval_def
  by fastforce 

lemma lipschitzI_on_le_lipschitzI_on:
  fixes F  :: ‹real interval ⇒ real interval›
  assumes inc_isontonic_F: ‹inclusion_isotonic F›
      and lipschitzI_F:    ‹C-lipschitzI_on {X} F›
      and interval_inc:    ‹x ≤ X›
      and interval_ext:    ‹F is_interval_extension_of f›
    shows ‹∃ L. L-lipschitzI_on {x} F›
  apply(rule exI[of _ "C * (width X)/(width x)"]) 
  apply(subst lipschitzI_onI, simp_all add: assms)
  subgoal
    apply(rule conjI)
    subgoal 
      using width_zero_interval_extension[of F f x, simplified assms, simplified] 
      by simp 
    subgoal 
      using inc_isontonic_F interval_inc lipschitzI_F lipschitzI_on_le_interval by blast 
    done 
    using lipschitzI_on_le_interval[of F C X x, simplified assms , simplified]
  subgoal 
    using lipschitzI_on_nonneg assms
    by (metis divide_nonneg_nonneg interval_width_positive mult_nonneg_nonneg)  
  done 

lemma uniform_subdivision_le:
  fixes X  :: ‹real interval›
  assumes ‹N>0›
  shows ‹∀ x ∈ set (uniform_subdivision X N). x ≤ X›
  using last_upper_uniform_subdivision[of N X, simplified assms, simplified]
        hd_lower_uniform_subdivision[of N X, simplified assms, simplified]
        non_overlapping_implies_sorted_wrt_upper[of "(uniform_subdivision X N)", simplified uniform_subdivisions_non_overlapping assms, simplified]
        non_overlapping_implies_sorted_wrt_lower[of "(uniform_subdivision X N)", simplified uniform_subdivisions_non_overlapping assms, simplified]
  unfolding sorted_wrt_upper_def sorted_wrt_lower_def cmp_lower_width_def less_eq_interval_def
  by (metis (no_types, lifting) assms in_set_conv_nth interval_list_union_correct non_empty_subdivision set_of_subset_iff union_set)

lemma lipschitzI_on_uniform_subdivision:
  fixes F  :: ‹real interval ⇒ real interval›
  assumes inc_isontonic_F: ‹inclusion_isotonic F›
      and lipschitzI_F:    ‹C-lipschitzI_on ({X}) F›
      and ‹N>0›
    shows ‹∀x∈(set (uniform_subdivision X N)). width (F x) ≤ C * width X›
  using lipschitzI_on_le_interval[of F C X, simplified assms, simplified]
        uniform_subdivision_le[of N X, simplified assms, simplified ]
  by simp 

lemma division_leq_pos:
  fixes x :: "'a::{linordered_field}"
  assumes "x > 0" and "y > 0" and "z > 0" and "y ≤ z"
  shows "x / z ≤ x / y"
proof -
  have "x * y ≤ x * z" using assms by simp
  hence "(x * y) / (y * z) ≤ (x * z) / (y * z)" 
    using assms 
    by (simp add: frac_le)
  thus ?thesis using assms by auto[1]  
qed

lemma each_subdivision_width_order':
  fixes X :: "real interval"
  assumes "F is_interval_extension_of f"
  and "0 < N"
  and "Xs ∈ set (uniform_subdivision X N)" 
shows "∃ L. width(F Xs) ≤ L * width (X) / of_nat N" 
  by (metis assms less_numeral_extra(3) mult_eq_0_iff nonzero_divide_eq_eq 
      of_nat_le_0_iff order_refl uniform_subdivisions_width width_zero_interval_extension) 

lemma uniform_subdivision_min_nonzero: 
  assumes ‹N > 0›
  and ‹width X > 0›
  shows ‹0 < Min (width ` set (uniform_subdivision X N))› 
  using assms unfolding image_set uniform_subdivision_def Let_def width_def
  by (simp, simp add: order_le_less) 

lemma uniform_subdivision_width_zero_replicate_eq: 
  fixes X::‹real interval›
  assumes positive_N:  ‹0 < N› 
  and zero_width_X: ‹0 = width X ›  
  shows‹replicate N X = (uniform_subdivision X N)›
  using assms 
proof(induction N)
  case 0
  then show ?case 
    by simp
next
  case (Suc N)
  then show ?case 
    using width_zero_lower_upper[of X, simplified assms, simplified]
    unfolding uniform_subdivision_def
    by (simp, metis append.right_neutral map_replicate_trivial mk_interval_id replicate_app_Cons_same)
qed

lemma set_of_interval_list_zero_width:
  fixes X::‹real interval›
  assumes positive_N:  ‹0 < N› 
  and zero_width_X: ‹0 = width X ›  
  shows‹set_of_interval_list (uniform_subdivision X N) = {lower X..upper X}›
proof(insert assms, simp add: uniform_subdivision_width_zero_replicate_eq[of N X, simplified assms, simplified, symmetric], induction N)
  case 0
  then show ?case 
    by(simp)
next
  case (Suc N)
  then show ?case 
    unfolding set_of_interval_list_def set_of_eq
    by(simp, fastforce)
qed

lemma  width_zero_subdivision: "width X = (0::real) ==> N > 0 ⟹ set (uniform_subdivision X N) = {X}"
  using width_zero_lower_upper[of X]
  unfolding uniform_subdivision_def Let_def mk_interval'
  apply(auto simp add: image_def)[1]
  apply (metis Interval_id)
  apply (metis Interval_id)
  done 

lemma lipschitz_on_implies_lipschitzI_on_pre:
  fixes f :: ‹real ⇒ real›
 and F  :: ‹real interval ⇒ real interval›
  assumes ‹finite S›
   and ‹0 < Min (width ` S)›
 shows ‹let max_F_width = Max (width ` (F ` S));
            min_f_width = Min (width ` S)
        in ∀ x ∈ S. width (F x) ≤ (max_F_width/min_f_width) *  width x›
  unfolding Let_def
  by (simp, smt (verit) assms division_leq_pos interval_width_positive mult_eq_0_iff 
          nonzero_mult_div_cancel_right width_Min width_img_Max zero_le_divide_iff) 

lemma lipschitz_on_implies_lipschitzI_on':
  fixes f :: ‹real ⇒ real›
    and F  :: ‹real interval ⇒ real interval›
  assumes   non_empty: ‹S ≠ {}›  
   and         finite: ‹finite S›
   and non_zero_width: ‹0 < Min (width ` S)›
   and interval_ext_F: ‹F is_interval_extension_of f›
 shows ‹∃  L. L-lipschitzI_on S F›
  unfolding lipschitzI_on_def
  apply(rule exI[of _ "(Max (width ` (F ` S)))/(Min (width ` S))"])
  apply(rule conjI)
  subgoal 
    apply(rule divide_nonneg_nonneg)
    subgoal 
      using assms interval_width_positive
      by (metis (mono_tags, lifting) Max_in finite_imageI imageE image_is_empty) 
    subgoal 
      using assms interval_width_positive
      by(auto)[1]
    done 
  subgoal 
    by (meson assms lipschitz_on_implies_lipschitzI_on_pre) 
  done 


lemma natural_extension_transfer_lipschitz:
  assumes  positive_N: ‹0 < N› 
  and inc_isontonic_F: ‹inclusion_isotonic F›
  and  interval_ext_F: ‹F is_natural_interval_extension_of f›
  and     lipschitz_f: ‹C-lipschitz_on (set_of X) f› 
shows     ‹C-lipschitzI_on (set (uniform_subdivision X N)) F›
proof(cases "0 < width X")
  case True
  then show ?thesis    
  apply(subst lipschitzI_onI)
  subgoal 
    using assms
     each_subdivision_width_order'[of F f N _ X ]
     each_subdivision_width_order[of F C "set (uniform_subdivision X N)" f X N ]
     uniform_subdivision_le[of N X ]
    unfolding lipschitz_on_def is_natural_interval_extension_of_def 
              inclusion_isotonic_def 
    dist_real_def abs_real_def width_def mk_interval'
    apply(auto split:if_splits)[1]
    by (smt (z3) Interval_id interval_of.abs_eq interval_of_in_eq less_eq_interval_def lower_bounds lower_in_interval upper_bounds)
  subgoal 
    using assms lipschitz_on_nonneg by auto 
  subgoal by simp 
  done 
next
  case False
    have width_zero: ‹width X = 0›
    using False 
    by (meson interval_width_positive linorder_not_le nle_le) 
  have us_X: ‹set (uniform_subdivision X N) = {X}›
    using width_zero width_zero_subdivision
    using positive_N by blast 
  then show ?thesis
    using width_zero 
    apply(simp add:assms)
     apply(subst lipschitzI_onI)
    subgoal    using assms
     each_subdivision_width_order'[of F f N _ X ]
     each_subdivision_width_order[of F C "set (uniform_subdivision X N)" f X N ]
     uniform_subdivision_le[of N X ]
    unfolding lipschitz_on_def is_natural_interval_extension_of_def 
              inclusion_isotonic_def 
    dist_real_def abs_real_def width_def mk_interval'
    apply(auto split:if_splits)[1]
    by (meson interval_ext_F natural_interval_extension_implies_interval_extension) 
 subgoal 
    using assms lipschitz_on_nonneg by auto 
  subgoal by simp 
  done 
qed


lemma lipschitz_on_division_lipschitz_on:
  assumes lipschitz_f: "C-lipschitz_on (set_of X) f " 
    and non_empty: "uniform_subdivision  X N ≠ []" 
    and subdivision: "Xs ∈ set(uniform_subdivision (X::real interval) N)"
  shows "∃ L . L-lipschitz_on (set_of Xs) f"
proof - 
  fix L
  have subset: "Xs ≤ X" 
    using assms(3) uniform_subdivision_le[of N X] 
    by (metis (no_types, lifting) bot_nat_0.extremum_strict
        bot_nat_0.not_eq_extremum in_set_conv_nth length_map list.size(3) map_nth 
        uniform_subdivision_def)
  show ?thesis 
    by (meson assms(1) interval_set_leq_eq lipschitz_on_subset subset)
qed 

lemma lipschitz_on_lischitz_on_subdivisions:
 assumes lipschitz_f: "C-lipschitz_on (set_of X) f " 
    and non_empty: "uniform_subdivision  X N ≠ []" 
    and non_zero: "0 < N"
  shows "∃ L . ∀ Xs ∈ set(uniform_subdivision (X::real interval) N). L-lipschitz_on (set_of Xs) f"
proof - 
  have subset: " ∀ Xs ∈ set(uniform_subdivision (X::real interval) N) . Xs ≤ X" 
    using assms uniform_subdivision_le[of N X] by blast
  show  "∃ L. ∀Xs∈set (uniform_subdivision X N). L-lipschitz_on (set_of Xs) f"
  proof -
    obtain L where L: "L = C" using lipschitz_f by auto
    have "L-lipschitz_on (set_of Xs) f" if "Xs ∈ set (uniform_subdivision X N)" for Xs
    proof -
      show ?thesis using lipschitz_on_division_lipschitz_on[of C X f N Xs, simplified assms, simplified] L 
        by (meson interval_set_leq_eq lipschitz_f lipschitz_on_subset subset that) 
    qed
    thus ?thesis by auto
  qed
qed

lemma lipschitz_on_lischitz_on_subdivisions_n:
 assumes lipschitz_f: "C-lipschitz_on (set_of X) f " 
    and non_empty: "uniform_subdivision  X N ≠ []" 
    and non_zero: "0 < N"
  shows "∃ L . ∀ N > 0 . ∀ Xs ∈ set(uniform_subdivision (X::real interval) N). L-lipschitz_on (set_of Xs) f"
proof - 
  have subset: " ∀ Xs ∈ set(uniform_subdivision (X::real interval) N) . Xs ≤ X" 
    using assms uniform_subdivision_le[of N X] by blast
  show  "∃ L.  ∀ N > 0 . ∀Xs∈set (uniform_subdivision X N). L-lipschitz_on (set_of Xs) f"
  proof -
    obtain L where L: "L = C" using lipschitz_f by auto
    have "L-lipschitz_on (set_of Xs) f" if "Xs ∈ set (uniform_subdivision X N)" for Xs
    proof -
      show ?thesis using lipschitz_on_division_lipschitz_on[of C X f N Xs, simplified assms, simplified] L 
        by (meson interval_set_leq_eq lipschitz_f lipschitz_on_subset subset that) 
    qed
    thus ?thesis 
      by (meson interval_set_leq_eq lipschitz_f lipschitz_on_subset uniform_subdivision_le)
  qed
qed

lemma lipschitzI_on_division_lipschitzI_on:
  assumes lipschitz_f: "C-lipschitzI_on (set(uniform_subdivision X N)) F " 
    and non_empty: "uniform_subdivision  X N ≠ []" 
    and subdivision: "Xs ∈ set(uniform_subdivision (X::real interval) N)"
  shows "∃ L . L-lipschitzI_on {Xs} F"
proof - 
  fix L
  have subset: "Xs ≤ X" 
    using assms(3) uniform_subdivision_le[of N X] 
    by (smt (verit, del_insts) gr_zeroI list.map_disc_iff list.size(3) map_nth non_empty uniform_subdivision_def)
  show ?thesis 
    by (meson empty_subsetI insert_subset lipschitzI_on_le lipschitz_f subdivision)
qed 

lemma lipschitzI_on_lipschitzI_on_subdivisions:
  fixes X :: "real interval"
 assumes lipschitz_f: "C-lipschitzI_on (set(uniform_subdivision X N)) F "  
    and non_zero: "0 < N"
  shows "∃ L . ∀ Xs ∈ set(uniform_subdivision X N). L-lipschitzI_on {Xs} F"
proof - 
  have subset: " ∀ Xs ∈ set(uniform_subdivision (X::real interval) N) . Xs ≤ X" 
    using assms uniform_subdivision_le[of N X] by blast
  show  "∃L. ∀Xs∈set (uniform_subdivision X N). L-lipschitzI_on {Xs} F"
  proof -
    obtain L where L: "L = C" using lipschitz_f by auto
    have "L-lipschitzI_on {Xs} F" if "Xs ∈ set (uniform_subdivision X N)" for Xs
    proof -
      show ?thesis using assms 
        by (simp add: L lipschitzI_on_def that) 
    qed
    thus ?thesis by auto
  qed
qed

section ‹Lipschitz Convergence›

lemma isotonic_lipschitz_refinement':
  assumes positive_N:  ‹0 < N› 
  and inc_isontonic_F: ‹inclusion_isotonic F›
  and interval_ext_F:  ‹F is_interval_extension_of f›
  and lipschitz_f:     ‹C-lipschitz_on (set_of X) f›
shows ‹∃ L. width_set (set_of_interval_list (map F (uniform_subdivision X N))) - width_set (f ` (set_of X)) ≤ 2 * (L * width X / real N)› 
proof (cases "0 < width X")
  case True
  have us_eq_set_of_X: ‹(set_of_interval_list (uniform_subdivision X N)) = set_of X›
    by (simp add: Lipschitz_Subdivisions_Refinements.set_of_interval_list_set_eq_interval_list_union_contiguous 
                 contiguous_uniform_subdivision non_empty_subdivision positive_N union_set)
  have lipschitz_f': ‹C-lipschitz_on (set_of_interval_list (uniform_subdivision X N)) f›
    by (simp add: lipschitz_f us_eq_set_of_X)
  have us_nonempty: ‹uniform_subdivision  X N ≠ [] ›     
    by (simp add: assms(1) non_empty_subdivision)  
  have us_nonempty_set: ‹set (uniform_subdivision X N) ≠ {}›     
    by (simp add: us_nonempty)
  have us_finite: ‹finite (set (uniform_subdivision X N))›     
    by simp 
  have sorted_lower: ‹sorted_wrt_lower (uniform_subdivision X N)›
    by (simp add: contiguous_sorted_wrt_lower contiguous_uniform_subdivision) 
  have sorted_upper: ‹sorted_wrt_upper (uniform_subdivision X N)›
    by (simp add: contiguous_sorted_wrt_upper contiguous_uniform_subdivision) 
  have lipschitzI: ‹∃L. L-lipschitzI_on (set (uniform_subdivision X N)) F›
    using lipschitz_on_implies_lipschitzI_on'[of "set (uniform_subdivision X N)" F f, simplified 
                                                 us_nonempty_set us_finite interval_ext_F]
          uniform_subdivision_min_nonzero[of N X, simplified positive_N True, simplified]
    by(simp)
  have set_of_interval_eq: ‹(set_of_interval_list (uniform_subdivision X N)) = (set_of (interval_list_union (uniform_subdivision X N)))›
    by (simp add: Lipschitz_Subdivisions_Refinements.set_of_interval_list_set_eq_interval_list_union_contiguous 
                  contiguous_uniform_subdivision us_nonempty) 
  have width_bounded: ‹∃ L. Max (excess_width F f ` set (uniform_subdivision X N)) ≤ 2 * (L * width X / real N)›
    using 
          each_subdivision_excess_width_order[of F _ "(set (uniform_subdivision X N))" f X N C, 
            simplified inc_isontonic_F interval_ext_F positive_N lipschitz_f'[simplified set_of_interval_eq], simplified] 
         max_subdivision_excess_width_order[of F _ "(set (uniform_subdivision X N))" f X N C, 
            simplified inc_isontonic_F interval_ext_F positive_N lipschitz_f', simplified] 
  proof -
    assume a1: "⋀C. C-lipschitzI_on (set (uniform_subdivision X N)) F ⟹ 
      Max (excess_width F f ` set (uniform_subdivision X N)) ≤ C * width X / real N"
    have "∀r ra rb. (r::real) / rb * ra = r * ra / rb"
      by fastforce
    then show ?thesis
      using a1 by (metis ‹∃L. L-lipschitzI_on (set (uniform_subdivision X N)) F› 
          divide_numeral_1 le_divide_eq_numeral1(1) mult_numeral_1 order_antisym_conv order_refl)
  qed 
 have width_limit:‹∃ L.    width_set (set_of_interval_list (map F (uniform_subdivision X N))) 
                          - width_set (f ` (set_of X))
                        ≤ 2 * (L * width X / real N)›
    using width_bounded
          map_inclusion_isotonic_excess_width_bounded(1)[of "uniform_subdivision X N" F f C, 
             simplified us_nonempty interval_ext_F inc_isontonic_F sorted_lower sorted_upper lipschitz_f', simplified]
    by (metis (no_types, lifting) us_eq_set_of_X inc_isontonic_F interval_ext_F lipschitzI lipschitz_f' list.set_map 
              max_subdivision_excess_width_order order.refl positive_N)
  then show ?thesis
    by simp 
next
  case False
  have width_zero: ‹width X = 0›
    using False 
    by (meson interval_width_positive linorder_not_le nle_le) 
  have us_nonempty: ‹uniform_subdivision X N ≠ [] ›     
    by (simp add: assms(1) non_empty_subdivision)  
  have set_of_interval_eq: ‹(set_of (interval_list_union (uniform_subdivision X N))) = (set_of_interval_list (uniform_subdivision X N))›
    by (simp add: Lipschitz_Subdivisions_Refinements.set_of_interval_list_set_eq_interval_list_union_contiguous 
                  contiguous_uniform_subdivision us_nonempty) 
  have w_zero_1: ‹width_set (set_of_interval_list (map F (uniform_subdivision X N))) = 0›
    by (metis (full_types) Lipschitz_Subdivisions_Refinements.set_of_interval_list_set_eq_interval_list_union_contiguous 
        contiguous_uniform_subdivision interval_ext_F map_replicate non_empty_subdivision positive_N 
        uniform_subdivision_width_zero_replicate_eq union_set width_eq_wdith_set width_zero width_zero_interval_extension)
  have w_zero_2: ‹ width_set (f ` (set_of X)) = 0›
    using set_of_interval_list_zero_width[of N X, simplified positive_N width_zero, simplified]
          width_zero width_zero_lower_upper[of X, simplified width_zero, simplified]
    by (metis diff_ge_0_iff_ge inc_isontonic_F inf_le_sup_image_real interval_ext_F lipschitz_f nle_le 
              width_inclusion_isotonic_approx width_set_def width_zero_interval_extension) 
  then show ?thesis
    using width_zero w_zero_1 w_zero_2  
    by simp 
qed

lemma isotonic_lipschitz_refinementI:
  assumes positive_N:  ‹0 < N› 
  and inc_isontonic_F: ‹inclusion_isotonic F›
  and interval_ext_F:  ‹F is_interval_extension_of f›
  and lipschitz_f:     ‹L-lipschitz_on (set_of X) f› 
  and lipschitz_F:     ‹C-lipschitzI_on (set (uniform_subdivision X N)) F›
shows ‹width_set (set_of_interval_list (map F (uniform_subdivision X N))) - width_set (f ` (set_of X)) ≤ 2 * (C * width X / real N)› 
proof (cases "0 < width X")
  case True
  have us_eq_set_of_X: ‹(set_of_interval_list (uniform_subdivision X N)) = set_of X›
    by (simp add: Lipschitz_Subdivisions_Refinements.set_of_interval_list_set_eq_interval_list_union_contiguous 
                 contiguous_uniform_subdivision non_empty_subdivision positive_N union_set)
  have lipschitz_f': ‹L-lipschitz_on (set_of_interval_list (uniform_subdivision X N)) f›
    by (simp add: lipschitz_f us_eq_set_of_X)
  have us_nonempty: ‹uniform_subdivision  X N ≠ [] ›     
    by (simp add: assms(1) non_empty_subdivision)  
  have us_nonempty_set: ‹set (uniform_subdivision X N) ≠ {}›     
    by (simp add: us_nonempty)
  have us_finite: ‹finite (set (uniform_subdivision X N))›     
    by simp 
  have sorted_lower: ‹sorted_wrt_lower (uniform_subdivision X N)›
    by (simp add: contiguous_sorted_wrt_lower contiguous_uniform_subdivision) 
  have sorted_upper: ‹sorted_wrt_upper (uniform_subdivision X N)›
    by (simp add: contiguous_sorted_wrt_upper contiguous_uniform_subdivision) 
  have lipschitzI: ‹C-lipschitzI_on (set (uniform_subdivision X N)) F›
    using lipschitz_F by blast
  have set_of_interval_eq: ‹(set_of_interval_list (uniform_subdivision X N)) = (set_of (interval_list_union (uniform_subdivision X N)))›
    by (simp add: Lipschitz_Subdivisions_Refinements.set_of_interval_list_set_eq_interval_list_union_contiguous 
                  contiguous_uniform_subdivision us_nonempty) 
  have width_bounded: ‹Max (excess_width F f ` set (uniform_subdivision X N)) ≤ 2 * (C * width X / real N)›
    using 
          each_subdivision_excess_width_order[of F C "(set (uniform_subdivision X N))" f X N _, 
            simplified inc_isontonic_F interval_ext_F positive_N lipschitz_f'[simplified set_of_interval_eq], simplified] 
         max_subdivision_excess_width_order[of F C "(set (uniform_subdivision X N))" f X N _, 
            simplified inc_isontonic_F interval_ext_F positive_N lipschitz_f', simplified]
    by (smt (verit) divide_nonneg_nonneg interval_width_positive lipschitzI_on_def lipschitz_F lipschitz_f' of_nat_0_less_iff positive_N split_mult_pos_le) 
 have width_limit:‹width_set (set_of_interval_list (map F (uniform_subdivision X N))) 
                          - width_set (f ` (set_of X))
                        ≤ 2 * (C * width X / real N)›
    using width_bounded
    by (metis assms(3) inc_isontonic_F lipschitz_F lipschitz_f' map_inclusion_isotonic_excess_width_bounded(1) max_subdivision_excess_width_order order_le_less positive_N sorted_lower sorted_upper us_eq_set_of_X us_nonempty) 
    then show ?thesis
    by simp 
next
  case False
  have width_zero: ‹width X = 0›
    using False 
    by (meson interval_width_positive linorder_not_le nle_le) 
  have us_nonempty: ‹uniform_subdivision X N ≠ [] ›     
    by (simp add: assms(1) non_empty_subdivision)  
  have set_of_interval_eq: ‹(set_of (interval_list_union (uniform_subdivision X N))) = (set_of_interval_list (uniform_subdivision X N))›
    by (simp add: Lipschitz_Subdivisions_Refinements.set_of_interval_list_set_eq_interval_list_union_contiguous 
                  contiguous_uniform_subdivision us_nonempty) 
  have w_zero_1: ‹width_set (set_of_interval_list (map F (uniform_subdivision X N))) = 0›
    by (metis (full_types) Lipschitz_Subdivisions_Refinements.set_of_interval_list_set_eq_interval_list_union_contiguous 
        contiguous_uniform_subdivision interval_ext_F map_replicate non_empty_subdivision positive_N 
        uniform_subdivision_width_zero_replicate_eq union_set width_eq_wdith_set width_zero width_zero_interval_extension)
  have w_zero_2: ‹ width_set (f ` (set_of X)) = 0›
    using set_of_interval_list_zero_width[of N X, simplified positive_N width_zero, simplified]
          width_zero width_zero_lower_upper[of X, simplified width_zero, simplified]
    by (simp add: set_of_eq width_set_def) 
  then show ?thesis 
    using width_zero w_zero_1 w_zero_2  
    by simp 
qed

lemma isotonic_lipschitz_refinement:
  assumes positive_N:  ‹0 < N› 
  and inc_isontonic_F: ‹inclusion_isotonic F›
  and interval_ext_F:  ‹F is_interval_extension_of f›
  and lipschitz_f:     ‹L-lipschitz_on (set_of X) f› 
  and lipschitz_F:     ‹C-lipschitzI_on (set (uniform_subdivision X N)) F›
shows ‹excess_width_set (refinement_set F N) f X ≤ 2 * (C * width X / real N)›
  using isotonic_lipschitz_refinementI[of N F f L X C, simplified assms, simplified] 
  unfolding excess_width_set_def refinement_set_def by simp
       
end