Theory Bounded_Continuous_Function

section ‹Bounded Continuous Functions›

theory Bounded_Continuous_Function
imports Integration
begin

subsection ‹Definition›

definition bcontfun :: "('a::topological_space ⇒ 'b::metric_space) set"
  where "bcontfun = {f. continuous_on UNIV f ∧ bounded (range f)}"

typedef (overloaded) ('a, 'b) bcontfun =
    "bcontfun :: ('a::topological_space ⇒ 'b::metric_space) set"
  by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)

lemma bcontfunE:
  assumes "f ∈ bcontfun"
  obtains y where "continuous_on UNIV f" "⋀x. dist (f x) u ≤ y"
  using assms unfolding bcontfun_def
  by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI)

lemma bcontfunE':
  assumes "f ∈ bcontfun"
  obtains y where "continuous_on UNIV f" "⋀x. dist (f x) undefined ≤ y"
  using assms bcontfunE
  by metis

lemma bcontfunI: "continuous_on UNIV f ⟹ (⋀x. dist (f x) u ≤ b) ⟹ f ∈ bcontfun"
  unfolding bcontfun_def
  by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE)

lemma bcontfunI': "continuous_on UNIV f ⟹ (⋀x. dist (f x) undefined ≤ b) ⟹ f ∈ bcontfun"
  using bcontfunI by metis

lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)"
  using Rep_bcontfun[of x]
  by (auto simp: bcontfun_def intro: continuous_on_subset)

(* TODO: Generalize to uniform spaces? *)
instantiation bcontfun :: (topological_space, metric_space) metric_space
begin

definition dist_bcontfun :: "('a, 'b) bcontfun ⇒ ('a, 'b) bcontfun ⇒ real"
  where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"

definition uniformity_bcontfun :: "(('a, 'b) bcontfun × ('a, 'b) bcontfun) filter"
  where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"

definition open_bcontfun :: "('a, 'b) bcontfun set ⇒ bool"
  where "open_bcontfun S = (∀x∈S. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ S)"

lemma dist_bounded:
  fixes f :: "('a, 'b) bcontfun"
  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) ≤ dist f g"
proof -
  have "Rep_bcontfun f ∈ bcontfun" by (rule Rep_bcontfun)
  from bcontfunE'[OF this] obtain y where y:
    "continuous_on UNIV (Rep_bcontfun f)"
    "⋀x. dist (Rep_bcontfun f x) undefined ≤ y"
    by auto
  have "Rep_bcontfun g ∈ bcontfun" by (rule Rep_bcontfun)
  from bcontfunE'[OF this] obtain z where z:
    "continuous_on UNIV (Rep_bcontfun g)"
    "⋀x. dist (Rep_bcontfun g x) undefined ≤ z"
    by auto
  show ?thesis
    unfolding dist_bcontfun_def
  proof (intro cSUP_upper bdd_aboveI2)
    fix x
    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) ≤
      dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined"
      by (rule dist_triangle2)
    also have "… ≤ y + z"
      using y(2)[of x] z(2)[of x] by (rule add_mono)
    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) ≤ y + z" .
  qed simp
qed

lemma dist_bound:
  fixes f :: "('a, 'b) bcontfun"
  assumes "⋀x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) ≤ b"
  shows "dist f g ≤ b"
  using assms by (auto simp: dist_bcontfun_def intro: cSUP_least)

lemma dist_bounded_Abs:
  fixes f g :: "'a ⇒ 'b"
  assumes "f ∈ bcontfun" "g ∈ bcontfun"
  shows "dist (f x) (g x) ≤ dist (Abs_bcontfun f) (Abs_bcontfun g)"
  by (metis Abs_bcontfun_inverse assms dist_bounded)

lemma const_bcontfun: "(λx::'a. b::'b) ∈ bcontfun"
  by (auto intro: bcontfunI continuous_on_const)

lemma dist_fun_lt_imp_dist_val_lt:
  assumes "dist f g < e"
  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
  using dist_bounded assms by (rule le_less_trans)

lemma dist_val_lt_imp_dist_fun_le:
  assumes "∀x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
  shows "dist f g ≤ e"
  unfolding dist_bcontfun_def
proof (intro cSUP_least)
  fix x
  show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) ≤ e"
    using assms[THEN spec[where x=x]] by (simp add: dist_norm)
qed simp

instance
proof
  fix f g h :: "('a, 'b) bcontfun"
  show "dist f g = 0 ⟷ f = g"
  proof
    have "⋀x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) ≤ dist f g"
      by (rule dist_bounded)
    also assume "dist f g = 0"
    finally show "f = g"
      by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
  qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
  show "dist f g ≤ dist f h + dist g h"
  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
    fix x
    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) ≤
      dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)"
      by (rule dist_triangle2)
    also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) ≤ dist f h"
      by (rule dist_bounded)
    also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) ≤ dist g h"
      by (rule dist_bounded)
    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) ≤ dist f h + dist g h"
      by simp
  qed
qed (rule open_bcontfun_def uniformity_bcontfun_def)+

end

lemma closed_Pi_bcontfun:
  fixes I :: "'a::metric_space set"
    and X :: "'a ⇒ 'b::complete_space set"
  assumes "⋀i. i ∈ I ⟹ closed (X i)"
  shows "closed (Abs_bcontfun ` (Pi I X ∩ bcontfun))"
  unfolding closed_sequential_limits
proof safe
  fix f l
  assume seq: "∀n. f n ∈ Abs_bcontfun ` (Pi I X ∩ bcontfun)" and lim: "f ⇢ l"
  have lim_fun: "∀e>0. ∃N. ∀n≥N. ∀x. dist (Rep_bcontfun (f n) x) (Rep_bcontfun l x) < e"
    using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim]
    by (intro uniformly_cauchy_imp_uniformly_convergent[where P="λ_. True", simplified])
      (metis dist_fun_lt_imp_dist_val_lt)+
  show "l ∈ Abs_bcontfun ` (Pi I X ∩ bcontfun)"
  proof (rule, safe)
    fix x assume "x ∈ I"
    then have "closed (X x)"
      using assms by simp
    moreover have "eventually (λxa. Rep_bcontfun (f xa) x ∈ X x) sequentially"
    proof (rule always_eventually, safe)
      fix i
      from seq[THEN spec, of i] ‹x ∈ I›
      show "Rep_bcontfun (f i) x ∈ X x"
        by (auto simp: Abs_bcontfun_inverse)
    qed
    moreover note sequentially_bot
    moreover have "(λn. Rep_bcontfun (f n) x) ⇢ Rep_bcontfun l x"
      using lim_fun by (blast intro!: metric_LIMSEQ_I)
    ultimately show "Rep_bcontfun l x ∈ X x"
      by (rule Lim_in_closed_set)
  qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse)
qed


subsection ‹Complete Space›

instance bcontfun :: (metric_space, complete_space) complete_space
proof
  fix f :: "nat ⇒ ('a, 'b) bcontfun"
  assume "Cauchy f"  ― ‹Cauchy equals uniform convergence›
  then obtain g where limit_function:
    "∀e>0. ∃N. ∀n≥N. ∀x. dist (Rep_bcontfun (f n) x) (g x) < e"
    using uniformly_convergent_eq_cauchy[of "λ_. True"
      "λn. Rep_bcontfun (f n)"]
    unfolding Cauchy_def
    by (metis dist_fun_lt_imp_dist_val_lt)

  then obtain N where fg_dist:  ― ‹for an upper bound on @{term g}›
    "∀n≥N. ∀x. dist (g x) ( Rep_bcontfun (f n) x) < 1"
    by (force simp add: dist_commute)
  from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where
    f_bound: "∀x. dist (Rep_bcontfun (f N) x) undefined ≤ b"
    by force
  have "g ∈ bcontfun"  ― ‹The limit function is bounded and continuous›
  proof (intro bcontfunI)
    show "continuous_on UNIV g"
      using bcontfunE[OF Rep_bcontfun] limit_function
      by (intro continuous_uniform_limit[where f="λn. Rep_bcontfun (f n)" and F="sequentially"])
        (auto simp add: eventually_sequentially trivial_limit_def dist_norm)
  next
    fix x
    from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"
      by (simp add: dist_norm norm_minus_commute)
    with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"]
    show "dist (g x) undefined ≤ 1 + b" using f_bound[THEN spec, of x]
      by simp
  qed
  show "convergent f"
  proof (rule convergentI, subst lim_sequentially, safe)
    ― ‹The limit function converges according to its norm›
    fix e :: real
    assume "e > 0"
    then have "e/2 > 0" by simp
    with limit_function[THEN spec, of"e/2"]
    have "∃N. ∀n≥N. ∀x. dist (Rep_bcontfun (f n) x) (g x) < e/2"
      by simp
    then obtain N where N: "∀n≥N. ∀x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto
    show "∃N. ∀n≥N. dist (f n) (Abs_bcontfun g) < e"
    proof (rule, safe)
      fix n
      assume "N ≤ n"
      with N show "dist (f n) (Abs_bcontfun g) < e"
        using dist_val_lt_imp_dist_fun_le[of
          "f n" "Abs_bcontfun g" "e/2"]
          Abs_bcontfun_inverse[OF ‹g ∈ bcontfun›] ‹e > 0› by simp
    qed
  qed
qed


subsection ‹Supremum norm for a normed vector space›

instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
begin

definition "-f = Abs_bcontfun (λx. -(Rep_bcontfun f x))"

definition "f + g = Abs_bcontfun (λx. Rep_bcontfun f x + Rep_bcontfun g x)"

definition "f - g = Abs_bcontfun (λx. Rep_bcontfun f x - Rep_bcontfun g x)"

definition "0 = Abs_bcontfun (λx. 0)"

definition "scaleR r f = Abs_bcontfun (λx. r *⇩R Rep_bcontfun f x)"

lemma plus_cont:
  fixes f g :: "'a ⇒ 'b"
  assumes f: "f ∈ bcontfun"
    and g: "g ∈ bcontfun"
  shows "(λx. f x + g x) ∈ bcontfun"
proof -
  from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "⋀x. dist (f x) undefined ≤ y"
    by auto
  moreover
  from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "⋀x. dist (g x) undefined ≤ z"
    by auto
  ultimately show ?thesis
  proof (intro bcontfunI)
    fix x
    have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)"
      by simp
    also have "… ≤ dist (f x) 0 + dist (g x) 0"
      by (rule dist_triangle_add)
    also have "… ≤ dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
      unfolding zero_bcontfun_def using assms
      by (metis add_mono const_bcontfun dist_bounded_Abs)
    finally show "dist (f x + g x) 0 ≤ dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
  qed (simp add: continuous_on_add)
qed

lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x"
  by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun)

lemma uminus_cont:
  fixes f :: "'a ⇒ 'b"
  assumes "f ∈ bcontfun"
  shows "(λx. - f x) ∈ bcontfun"
proof -
  from bcontfunE[OF assms, of 0] obtain y
    where "continuous_on UNIV f" "⋀x. dist (f x) 0 ≤ y"
    by auto
  then show ?thesis
  proof (intro bcontfunI)
    fix x
    assume "⋀x. dist (f x) 0 ≤ y"
    then show "dist (- f x) 0 ≤ y"
      by (subst dist_minus[symmetric]) simp
  qed (simp add: continuous_on_minus)
qed

lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
  by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun)

lemma minus_cont:
  fixes f g :: "'a ⇒ 'b"
  assumes f: "f ∈ bcontfun"
    and g: "g ∈ bcontfun"
  shows "(λx. f x - g x) ∈ bcontfun"
  using plus_cont [of f "- g"] assms
  by (simp add: uminus_cont fun_Compl_def)

lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
  by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun)

lemma scaleR_cont:
  fixes a :: real
    and f :: "'a ⇒ 'b"
  assumes "f ∈ bcontfun"
  shows " (λx. a *⇩R f x) ∈ bcontfun"
proof -
  from bcontfunE[OF assms, of 0] obtain y
    where "continuous_on UNIV f" "⋀x. dist (f x) 0 ≤ y"
    by auto
  then show ?thesis
  proof (intro bcontfunI)
    fix x
    assume "⋀x. dist (f x) 0 ≤ y"
    then show "dist (a *⇩R f x) 0 ≤ ¦a¦ * y"
      by (metis norm_cmul_rule_thm norm_conv_dist)
  qed (simp add: continuous_intros)
qed

lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *⇩R g) x = a *⇩R Rep_bcontfun g x"
  by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)

instance
  by standard
    (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
      Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
      plus_cont const_bcontfun minus_cont scaleR_cont)

end

instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
begin

definition norm_bcontfun :: "('a, 'b) bcontfun ⇒ real"
  where "norm_bcontfun f = dist f 0"

definition "sgn (f::('a,'b) bcontfun) = f /⇩R norm f"

instance
proof
  fix a :: real
  fix f g :: "('a, 'b) bcontfun"
  show "dist f g = norm (f - g)"
    by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
      Abs_bcontfun_inverse const_bcontfun dist_norm)
  show "norm (f + g) ≤ norm f + norm g"
    unfolding norm_bcontfun_def
  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
    fix x
    have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) ≤
      dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0"
      by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm
        le_less_linear less_irrefl norm_triangle_lt)
    also have "dist (Rep_bcontfun f x) 0 ≤ dist f 0"
      using dist_bounded[of f x 0]
      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
    also have "dist (Rep_bcontfun g x) 0 ≤ dist g 0" using dist_bounded[of g x 0]
      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
    finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) ≤ dist f 0 + dist g 0" by simp
  qed
  show "norm (a *⇩R f) = ¦a¦ * norm f"
  proof -
    have "¦a¦ * Sup (range (λx. dist (Rep_bcontfun f x) 0)) =
      (SUP i:range (λx. dist (Rep_bcontfun f x) 0). ¦a¦ * i)"
    proof (intro continuous_at_Sup_mono bdd_aboveI2)
      fix x
      show "dist (Rep_bcontfun f x) 0 ≤ norm f" using dist_bounded[of f x 0]
        by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
          const_bcontfun)
    qed (auto intro!: monoI mult_left_mono continuous_intros)
    moreover
    have "range (λx. dist (Rep_bcontfun (a *⇩R f) x) 0) =
      (λx. ¦a¦ * x) ` (range (λx. dist (Rep_bcontfun f x) 0))"
      by auto
    ultimately
    show "norm (a *⇩R f) = ¦a¦ * norm f"
      by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse
        zero_bcontfun_def const_bcontfun image_image)
  qed
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)

end

lemma bcontfun_normI: "continuous_on UNIV f ⟹ (⋀x. norm (f x) ≤ b) ⟹ f ∈ bcontfun"
  by (metis bcontfunI dist_0_norm dist_commute)

lemma norm_bounded:
  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
  shows "norm (Rep_bcontfun f x) ≤ norm f"
  using dist_bounded[of f x 0]
  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
    const_bcontfun)

lemma norm_bound:
  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
  assumes "⋀x. norm (Rep_bcontfun f x) ≤ b"
  shows "norm f ≤ b"
  using dist_bound[of f 0 b] assms
  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun)


subsection ‹Continuously Extended Functions›

definition clamp :: "'a::euclidean_space ⇒ 'a ⇒ 'a ⇒ 'a" where
  "clamp a b x = (∑i∈Basis. (if x∙i < a∙i then a∙i else if x∙i ≤ b∙i then x∙i else b∙i) *⇩R i)"

definition ext_cont :: "('a::euclidean_space ⇒ 'b::real_normed_vector) ⇒ 'a ⇒ 'a ⇒ ('a, 'b) bcontfun"
  where "ext_cont f a b = Abs_bcontfun ((λx. f (clamp a b x)))"

lemma ext_cont_def':
  "ext_cont f a b = Abs_bcontfun (λx.
    f (∑i∈Basis. (if x∙i < a∙i then a∙i else if x∙i ≤ b∙i then x∙i else b∙i) *⇩R i))"
  unfolding ext_cont_def clamp_def ..

lemma clamp_in_interval:
  assumes "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i"
  shows "clamp a b x ∈ cbox a b"
  unfolding clamp_def
  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)

lemma dist_clamps_le_dist_args:
  fixes x :: "'a::euclidean_space"
  assumes "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i"
  shows "dist (clamp a b y) (clamp a b x) ≤ dist y x"
proof -
  from box_ne_empty(1)[of a b] assms have "(∀i∈Basis. a ∙ i ≤ b ∙ i)"
    by (simp add: cbox_def)
  then have "(∑i∈Basis. (dist (clamp a b y ∙ i) (clamp a b x ∙ i))⇧2) ≤
    (∑i∈Basis. (dist (y ∙ i) (x ∙ i))⇧2)"
    by (auto intro!: setsum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
  then show ?thesis
    by (auto intro: real_sqrt_le_mono
      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
qed

lemma clamp_continuous_at:
  fixes f :: "'a::euclidean_space ⇒ 'b::metric_space"
    and x :: 'a
  assumes "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i"
    and f_cont: "continuous_on (cbox a b) f"
  shows "continuous (at x) (λx. f (clamp a b x))"
  unfolding continuous_at_eps_delta
proof safe
  fix x :: 'a
  fix e :: real
  assume "e > 0"
  moreover have "clamp a b x ∈ cbox a b"
    by (simp add: clamp_in_interval assms)
  moreover note f_cont[simplified continuous_on_iff]
  ultimately
  obtain d where d: "0 < d"
    "⋀x'. x' ∈ cbox a b ⟹ dist x' (clamp a b x) < d ⟹ dist (f x') (f (clamp a b x)) < e"
    by force
  show "∃d>0. ∀x'. dist x' x < d ⟶
    dist (f (clamp a b x')) (f (clamp a b x)) < e"
    by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans])
qed

lemma clamp_continuous_on:
  fixes f :: "'a::euclidean_space ⇒ 'b::metric_space"
  assumes "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i"
    and f_cont: "continuous_on (cbox a b) f"
  shows "continuous_on UNIV (λx. f (clamp a b x))"
  using assms
  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)

lemma clamp_bcontfun:
  fixes f :: "'a::euclidean_space ⇒ 'b::real_normed_vector"
  assumes "⋀i. i ∈ Basis ⟹ a ∙ i ≤ b ∙ i"
    and continuous: "continuous_on (cbox a b) f"
  shows "(λx. f (clamp a b x)) ∈ bcontfun"
proof -
  have "bounded (f ` (cbox a b))"
    by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded])
  then obtain c where f_bound: "∀x∈f ` cbox a b. norm x ≤ c"
    by (auto simp add: bounded_pos)
  show "(λx. f (clamp a b x)) ∈ bcontfun"
  proof (intro bcontfun_normI)
    fix x
    show "norm (f (clamp a b x)) ≤ c"
      using clamp_in_interval[OF assms(1), of x] f_bound
      by (simp add: ext_cont_def)
  qed (simp add: clamp_continuous_on assms)
qed

lemma integral_clamp:
  "integral {t0::real..clamp t0 t1 x} f =
    (if x < t0 then 0 else if x ≤ t1 then integral {t0..x} f else integral {t0..t1} f)"
  by (auto simp: clamp_def)


declare [[coercion Rep_bcontfun]]

lemma ext_cont_cancel[simp]:
  fixes x a b :: "'a::euclidean_space"
  assumes x: "x ∈ cbox a b"
    and "continuous_on (cbox a b) f"
  shows "ext_cont f a b x = f x"
  using assms
  unfolding ext_cont_def
proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun])
  show "f (clamp a b x) = f x"
    using x unfolding clamp_def mem_box
    by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less)
qed (auto simp: cbox_def)

lemma ext_cont_cong:
  assumes "t0 = s0"
    and "t1 = s1"
    and "⋀t. t ∈ (cbox t0 t1) ⟹ f t = g t"
    and "continuous_on (cbox t0 t1) f"
    and "continuous_on (cbox s0 s1) g"
    and ord: "⋀i. i ∈ Basis ⟹ t0 ∙ i ≤ t1 ∙ i"
  shows "ext_cont f t0 t1 = ext_cont g s0 s1"
  unfolding assms ext_cont_def
  using assms clamp_in_interval[OF ord]
  by (subst Rep_bcontfun_inject[symmetric]) simp

end