section {* Auxiliary Lemmas *}
theory ODE_Auxiliarities
imports
  "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
  "~~/src/HOL/Library/Float"
begin

lemma norm_sub_leD1: "norm (a - b) \<le> c \<Longrightarrow> norm a \<le> norm b + c"
  by (metis add.commute diff_le_eq norm_triangle_ineq2 order_trans)

lemma norm_sub_leD2: "norm (a - b) \<le> c \<Longrightarrow> norm b \<le> norm a + c"
  by (rule norm_sub_leD1) (simp add: norm_minus_commute)

lemma atLeastAtMost_eq_cball:
  fixes a b::real
  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
  by (auto simp: dist_real_def field_simps split: split_if_asm)

lemma greaterThanLessThan_eq_ball:
  fixes a b::real
  shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
  by (auto simp: dist_real_def field_simps split: split_if_asm)

lemma closure_greaterThanLessThan[simp]:
  fixes a b::real
  shows "a < b \<Longrightarrow> closure {a <..< b} = {a .. b}"
  by (simp add: closure_ball greaterThanLessThan_eq_ball atLeastAtMost_eq_cball)

lemma closure_lessThan[simp]:
  fixes b::real
  shows "closure {..<b} = {..b}"
proof -
  have "{..<b} = {..b - 1} \<union> {b - 1 <..< b}"
    by auto
  also have "closure \<dots> = {..b}"
    by auto
  finally show ?thesis .
qed

lemma closure_greaterThan[simp]:
  fixes a::real
  shows "closure {a<..} = {a..}"
proof -
  have "{a<..} = {a + 1..} \<union> {a <..< a + 1}"
    by auto
  also have "closure \<dots> = {a..}"
    by auto
  finally show ?thesis .
qed

lemma closure_atLeastLessThan[simp]:
  fixes a b::real
  assumes "a < b"
  shows "closure {a ..< b} = {a .. b}"
proof -
  have "{a ..< b} = {a .. (a + b)/2} \<union> {(a + b)/2 <..< b}"
    using assms by auto
  also have "closure \<dots> = {a .. b}"
    using assms by auto
  finally show ?thesis .
qed

lemma closure_greaterThanAtMost[simp]:
  fixes a b::real
  assumes "a < b"
  shows "closure {a <.. b} = {a .. b}"
proof -
  have "{a <.. b} = {a <..< (a + b)/2} \<union> {(a + b)/2 .. b}"
    using assms by auto
  also have "closure \<dots> = {a .. b}"
    using assms by auto
  finally show ?thesis .
qed

text {* TODO: rather take an @{term "eventually P (at_right 0)"} variant of @{thm eventually_nhds_metric}*}
lemma has_derivative_within_alt3:
    "(f has_derivative f') (at x within s) =
     (bounded_linear f' \<and>
      (\<forall>e>0. eventually (\<lambda>d. \<forall>y\<in>s. norm (y - x) \<le> d \<longrightarrow>
        norm (f y - f x - f' (y - x)) \<le> e * norm (y - x)) (at_right 0)))"
  unfolding has_derivative_within filterlim_def le_nhds_metric_le eventually_filtermap
    eventually_at dist_norm diff_add_eq_diff_diff
  apply (auto simp add: linear_0 bounded_linear.linear pos_divide_le_eq)
  apply (drule_tac x = e in spec)
  apply auto
  apply (rule_tac x = d in exI)
  apply auto
  apply (case_tac "y = x") apply simp
  apply (metis bounded_linear.pos_bounded mult_zero_left norm_le_zero_iff norm_zero)
  apply auto
  apply (drule_tac x = e in spec)
  apply auto
  apply (rule_tac x = "d/2" in exI)
  apply auto
  done

text {* TODO: rather take an @{term "eventually P (at_right 0)"} variant of @{thm eventually_nhds_metric}*}
lemma continuous_on_eq_eventually:
  "continuous_on s f = (\<forall>x \<in> s. \<forall>e>0. eventually (\<lambda>d. \<forall>y\<in>s. dist y x \<le> d \<longrightarrow> dist (f y) (f x) < e) (at_right 0))"
  apply (auto simp: continuous_on_eq_continuous_within continuous_within_eps_delta
    eventually_at_le)
  apply (drule bspec) apply assumption
  apply (drule_tac x = "e" in spec)
  apply auto
  apply (rule_tac x = "d/2" in exI)
  apply auto
  apply (case_tac "y = x") apply simp
  apply (drule_tac x=y in bspec) apply assumption
  apply (auto simp: dist_real_def not_less)
  apply (drule bspec) apply assumption
  apply (drule_tac x = "e" in spec)
  apply auto
  done

text {* TODO: what about the variants @{thm DERIV_nonneg_imp_nondecreasing}, which have the
  slightly stronger @{term isCont} assumption *}
lemma has_vector_derivative_nonneg_imp_nondecreasing_open:
  fixes a::real and b::real and f::"real => real"
  assumes "a \<le> b" and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
      and "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> f' x \<ge> 0"
      and con: "continuous_on {a..b} f"
  shows "f a \<le> f b"
proof (rule ccontr, cases "a = b")
  assume "~ f a \<le> f b" and "a = b"
  then show False by auto
next
  assume A: "~ f a \<le> f b"
  assume B: "a ~= b"
  with assms have "\<exists>x\<in>{a<..<b}. f b - f a = (b - a) *\<^sub>R f' x"
    by (intro mvt) (auto simp: has_vector_derivative_def)
  then obtain z where z: "a < z" "z < b" and C: "f b - f a = (b - a) * f' z"
    by auto
  with A have "a < b" "f b < f a" by auto
  with C have "\<not> f' z \<ge> 0" by (auto simp add: not_le algebra_simps)
    (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono add_left_mono linear order_refl)
  with assms z show False by simp
qed

lemma mvt_more_general:
  fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
  assumes "a < b"
    and f_cont: "continuous_on {a .. b} f"
    and phi_cont: "continuous_on {a .. b} \<phi>"
    and f': "\<And>x. x \<in> {a<..<b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
    and phi': "\<And>x. x \<in> {a<..<b} \<Longrightarrow> (\<phi> has_vector_derivative \<phi>'(x)) (at x)"
    and bnd: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> norm (f'(x)) \<le> \<phi>' x"
  shows "norm (f b - f a) \<le> \<phi> b - \<phi> a"
proof -
  {
    fix x assume x: "a < x" "x < b"
    have "0 \<le> norm (f' x)" by simp
    also have "\<dots> \<le> \<phi>' x" using x by (auto intro!: bnd)
    finally have "0 \<le> \<phi>' x" .
  } note phi'_nonneg = this
  have phi_mono: "\<And>x y. x \<in> {a .. b} \<Longrightarrow> y \<in> {a .. b} \<Longrightarrow> x \<le> y \<Longrightarrow> \<phi> x \<le> \<phi> y"
    using _ phi'
    by (rule has_vector_derivative_nonneg_imp_nondecreasing_open)
      (auto intro: continuous_on_subset[OF phi_cont] phi'_nonneg)
  note f_tendsto = assms(2)[simplified continuous_on, rule_format]
  note phi_tendsto = assms(3)[simplified continuous_on, rule_format]
  {
    fix e::real assume "e > 0"
    def e2 \<equiv> "e / 2" with `e > 0` have "e2 > 0" by simp
    let ?le = "\<lambda>x1. norm (f x1 - f a) \<le> \<phi> x1 - \<phi> a + e * (x1 - a) + e"
    def A \<equiv> "{x2. a \<le> x2 \<and> x2 \<le> b \<and> (\<forall>x1\<in>{a ..< x2}. ?le x1)}"
    {
      fix x2
      assume a: "a \<le> x2" "x2 \<le> b" and le: "\<forall>x1\<in>{a..<x2}. ?le x1"
      have "?le x2" using `e > 0`
      proof cases
        assume "x2 \<noteq> a" with a have "a < x2" by simp
        have "at x2 within {a <..<x2}\<noteq> bot"
          using `a < x2`
          by (auto simp: trivial_limit_within islimpt_in_closure)
        moreover
        have "((\<lambda>x1. (\<phi> x1 - \<phi> a) + e * (x1 - a) + e) ---> (\<phi> x2 - \<phi> a) + e * (x2 - a) + e) (at x2 within {a <..<x2})"
          "((\<lambda>x1. norm (f x1 - f a)) ---> norm (f x2 - f a)) (at x2 within {a <..<x2})"
          using a
          by (auto intro!: tendsto_eq_intros f_tendsto phi_tendsto
            intro: tendsto_within_subset[where S="{a .. b}"])
        moreover
        have "eventually (\<lambda>x. x > a) (at x2 within {a <..<x2})"
          by (auto simp: eventually_at_filter)
        hence "eventually ?le (at x2 within {a <..<x2})"
          unfolding eventually_at_filter
          by eventually_elim (insert le, auto)
        ultimately
        show ?thesis
          by (rule tendsto_le)
      qed simp
    } note le_cont = this
    have "a \<in> A"
      using assms by (auto simp: A_def)
    hence [simp]: "A \<noteq> {}" by auto
    have A_ivl: "\<And>x1 x2. x2 \<in> A \<Longrightarrow> x1 \<in> {a ..x2} \<Longrightarrow> x1 \<in> A"
      by (simp add: A_def)
    have [simp]: "bdd_above A" by (auto simp: A_def)
    def y \<equiv> "Sup A"
    have "y \<le> b"
      unfolding y_def
      by (simp add: cSup_le_iff) (simp add: A_def)
    have y_all_le: "\<forall>x1\<in>{a..<y}. ?le x1"
      --"TODO: nicht auch leichter?!"
      apply (auto simp: A_def less_cSup_iff)
      apply (rule le_cont)
      apply simp using `y \<le> b` apply simp
      apply (auto simp add: y_def less_cSup_iff)
    proof -
      case goal1
      have "x1a \<in> A"
        apply (rule A_ivl)
        apply fact using goal1 apply simp
        done
      thus ?case
        apply (simp add: A_def)
        apply (rule le_cont)
        apply simp
        apply (smt `y \<le> b` `bdd_above A` cSup_upper goal1(1) goal1(2) goal1(4) y_def)
        apply simp
        done
    qed
    have "y \<in> A"
      apply (auto simp: A_def)
      apply (metis `a \<in> A` `bdd_above A` cSup_upper y_def)
      apply (metis `y \<le> b`)
      using y_all_le apply simp
      done
    hence "A = {a .. y}"
      apply (auto )
      apply (simp add: A_def)
      apply (simp add: y_def cSup_upper)
      apply (simp add: A_def)
      done
    have "a \<le> y"
      using `y \<in> A` by (auto simp: A_def)
    from le_cont[OF `a \<le> y` `y \<le> b` y_all_le] have le_y: "?le y" .
    {
      assume "a \<noteq> y" with `a \<le> y` have "a < y" by simp
      have "y = b"
      proof (rule ccontr)
        assume "y \<noteq> b"
        hence "y < b" using `y \<le> b` by simp
        from f' `a < y` `y < b` have "(f has_vector_derivative f' y) (at y within {a<..<b})"
          by (subst at_within_open) auto
        then have "eventually (\<lambda>d. \<forall>x1 \<in> {a<..<b}. norm (x1 - y) \<le> d \<longrightarrow> norm (f x1 - f y - (x1 - y) *\<^sub>R f' y) \<le> e2 * \<bar>x1 - y\<bar>) (at_right 0)"
          using `e2 > 0`
          by (auto simp: has_derivative_within_alt3 has_vector_derivative_def)
        moreover
        from phi' `a < y` `y < b` have "(\<phi> has_vector_derivative \<phi>' y) (at y within {a<..<b})"
          by (subst at_within_open) auto
        then have "eventually (\<lambda>d. \<forall>x1\<in>{a<..<b}. norm (x1 - y) \<le> d \<longrightarrow> norm (\<phi> x1 - \<phi> y - (x1 - y) *\<^sub>R \<phi>' y) \<le> e2 * \<bar>x1 - y\<bar>) (at_right 0)"
          using `e2 > 0`
          by (auto simp: has_derivative_within_alt3 has_vector_derivative_def)
        ultimately
        have 1: "eventually (\<lambda>d. \<forall>x1\<in>{y..<b}. norm (x1 - y) \<le> d \<longrightarrow> norm (f x1 - f y) \<le> (\<phi> x1 - \<phi> y) + e * \<bar>x1 - y\<bar>) (at_right 0)"
        proof eventually_elim
          case elim
          thus ?case
          proof safe
            fix x1 assume x1: "x1 \<in> {y..< b}" "norm (x1 - y) \<le> d"
            hence x1': "x1 \<in> {a <..< b}" using `a < y` by simp
            have "norm (f x1 - f y) \<le> norm (f' y) * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
              using elim(1)[rule_format, OF x1' x1(2), THEN norm_sub_leD1] by (auto simp: ac_simps)
            also have *: "norm (f' y) \<le> \<phi>' y" using bnd `a < y` `y < b` by simp
            also
            from elim(2)[rule_format, OF x1' x1(2), THEN norm_sub_leD2] have "\<phi>' y * \<bar>x1 - y\<bar> \<le> abs (\<phi> x1 - \<phi> y) + e2 * \<bar>x1 - y\<bar>"
              using order_trans[OF norm_ge_zero *]
              by (simp add: abs_mult ac_simps)
            also have "abs (\<phi> x1 - \<phi> y) = \<phi> x1 - \<phi> y"
              using x1 `a < y`
              by (intro abs_of_nonneg) (auto simp: algebra_simps intro!: phi_mono)
            finally have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e2 * \<bar>x1 - y\<bar> + e2 * \<bar>x1 - y\<bar>"
              by (auto simp: mult_right_mono)
            thus "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e * \<bar>x1 - y\<bar>" by (simp add: e2_def)
          qed
        qed
        have 2: "eventually (\<lambda>d::real. d > 0) (at_right 0)"
          by (auto simp: eventually_at_filter)
        have 3: "eventually (\<lambda>d::real. y + d < b) (at_right 0)"
          using _ `y < b`
          by (rule order_tendstoD) (auto intro!: tendsto_eq_intros)
        from eventually_happens[OF eventually_conj[OF 1 eventually_conj[OF 2 3]]]
        obtain d where d: "d > 0" "\<forall>x1\<in>{y..<b}. norm (x1 - y) \<le> d \<longrightarrow> norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e * \<bar>x1 - y\<bar>"
          "y + d < b"
          by auto
        hence "y + d \<in> A"
        proof -
          from `a < y` `0 < d` have "a < y + d" by simp
          moreover
          note `y + d < b`
          moreover
          note y_all_le
          moreover
          {
            fix x1 assume x1: "y \<le> x1" "x1 < y + d"
            have "norm (f x1 - f a) \<le> norm (f x1 - f y) + norm (f y - f a)"
              by (rule order_trans[OF _ norm_triangle_ineq]) simp
            also have "norm (f x1 - f y) \<le> \<phi> x1 - \<phi> y + e * \<bar>x1 - y\<bar>"
              using d x1 by auto
            also note le_y
            finally have "?le x1"
              using x1 by (auto simp: algebra_simps)
          }
          ultimately show "y + d \<in> A"
            by (auto simp: A_def)
        qed
        hence "y + d \<le> y"
          unfolding y_def
          by (rule cSup_upper) simp
        thus False using `d > 0` by simp
      qed
    } moreover {
      assume "a = y"
      with `a < b` have "y < b" by simp
      with `a = y` f_cont[unfolded continuous_on_eq_eventually] `e > 0`
        phi_cont[unfolded continuous_on_eq_eventually]
      have 1: "eventually (\<lambda>d. \<forall>x\<in>{a..b}. dist x y \<le> d \<longrightarrow> dist (f x) (f y) < e) (at_right 0)"
        by auto
      have 2: "eventually (\<lambda>d::real. d > 0) (at_right 0)"
        by (auto simp: eventually_at_filter)
      have 3: "eventually (\<lambda>d::real. y + d < b) (at_right 0)"
        using _ `y < b`
        by (rule order_tendstoD) (auto intro!: tendsto_eq_intros)
      from eventually_happens[OF eventually_conj[OF 1 eventually_conj[OF 2 3]]]
      obtain d where d: "0 < d" "y + d < b"
        "\<And>xa. xa\<in>{a..b} \<Longrightarrow> dist xa y \<le> d \<Longrightarrow> norm (f xa - f y) < e"
        by (auto simp: dist_norm)
      hence "y + d \<in> A"
      proof -
        from `a = y` `0 < d` have "a < y + d" by simp
        moreover
        note `y + d < b`
        moreover
        {
          fix x1 assume x1: "y \<le> x1" "x1 < y + d"
          have "norm (f x1 - f a) = norm (f x1 - f y)"
            by (simp add: `a = y`)
          also have "norm (f x1 - f y) < e"
            using x1 `a = y` d by (auto simp :dist_real_def intro!: d)
          also have "e \<le> e + \<phi> x1 - \<phi> a"
            using x1 `y < b` `y + d < b`
            by (auto simp add: `a = y` algebra_simps intro!: phi_mono)
          also have "e \<le> e * (x1 - a) + e"
            using `0 < e` `a = y` d x1
            by (auto intro!: mult_nonneg_nonneg simp: algebra_simps)
          finally have "?le x1" by (simp add: algebra_simps less_imp_le)
        }
        ultimately show "y + d \<in> A"
          by (auto simp: A_def `a = y`)
      qed
      hence "y + d \<le> y"
        unfolding y_def
        by (rule cSup_upper) simp
      hence "y = b"
        using `d > 0` by simp
    } ultimately have "y = b"
      by auto
    with le_y have "norm (f b - f a) \<le> \<phi> b - \<phi> a + e * (b - a + 1)"
      by (simp add: algebra_simps)
  } note * = this
  {
    fix e::real assume "e > 0"
    hence "norm (f b - f a) \<le> \<phi> b - \<phi> a + e"
      using *[of "e / (b - a + 1)"] `a < b` by simp
  } thus ?thesis
    by (rule field_le_epsilon)
qed

subsection {* Reals *}

subsection {* Vector Spaces *}

lemma scaleR_dist_distrib_left:
  fixes b c::"'a::real_normed_vector"
  shows "abs a * dist b c = dist (scaleR a b) (scaleR a c)"
  unfolding dist_norm scaleR_diff_right[symmetric] norm_scaleR ..

lemma ex_norm_eq_1: "\<exists>x. norm (x::'a::euclidean_space) = 1"
  by (metis vector_choose_size zero_le_one)

subsection {* Intervals *}

lemma image_mult_atLeastAtMost:
  "(\<lambda>x. x * c::real) ` {x..y} = (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
  apply (cases "c = 0")
   apply force
  apply (auto simp: field_simps not_less intro!: image_eqI[where x="inverse c * xa" for xa])
  done

lemma image_add_atLeastAtMost:
  "op + c ` {x..y::real} = {c + x .. c + y}"
  by (auto intro: image_eqI[where x="xa - c" for xa])

lemma min_zero_mult_nonneg_le: "0 \<le> h' \<Longrightarrow> h' \<le> h \<Longrightarrow> min 0 (h * k::real) \<le> h' * k"
  by (metis dual_order.antisym le_cases min_le_iff_disj mult_eq_0_iff mult_le_0_iff mult_right_mono_neg)

lemma max_zero_mult_nonneg_le: "0 \<le> h' \<Longrightarrow> h' \<le> h \<Longrightarrow> h' * k \<le> max 0 (h * k::real)"
  by (metis dual_order.antisym le_cases le_max_iff_disj mult_eq_0_iff mult_right_mono zero_le_mult_iff)

lemma closed_segment_real:
  fixes a b::real
  shows "closed_segment a b = (if a \<le> b then {a .. b} else {b .. a})"
proof (auto simp: closed_segment_def)
  case goal1
  thus ?case
    by (auto simp: algebra_simps intro!: mult_right_mono)
next
  case goal2
  hence "(1 - u) * a \<le> (1 - u) * b"
    by (auto intro!: mult_left_mono)
  thus ?case
    by (auto simp: algebra_simps)
next
  case goal3
  thus ?case
    by (cases "a = b") (auto simp: field_simps intro!: exI[where x= "(a - x) / (a - b)"])
next
  case goal4
  hence "(1 - u) * b \<le> (1 - u) * a"
    by (auto intro!: mult_left_mono)
  thus ?case
    by (auto simp: algebra_simps)
next
  case goal5
  thus ?case
    by (auto simp: algebra_simps intro!: mult_right_mono)
next
  case goal6
  thus ?case
    by (cases "a = b") (auto simp: field_simps intro!: exI[where x= "(a - x) / (a - b)"])
qed

lemma open_segment_real:
  fixes a b::real
  shows "open_segment a b = (if a < b then {a <..< b} else if a > b then {b <..< a} else {b})"
  apply (cases "a = b")
  defer
proof (auto simp: open_segment_def)
  case goal1
  thus ?case
    by (auto simp: algebra_simps intro!: mult_right_mono)
next
  case goal2
  hence "(1 - u) * a < (1 - u) * b"
    by auto
  thus ?case
    by (auto simp: algebra_simps)
next
  case goal3
  thus ?case
    by (cases "a = b") (auto simp: field_simps intro!: exI[where x= "(a - x) / (a - b)"])
next
  case goal4
  hence "(1 - u) * b < (1 - u) * a"
    by (auto intro!: mult_left_mono)
  thus ?case
    by (auto simp: algebra_simps)
next
  case goal5
  thus ?case
    by (auto simp: algebra_simps intro!: mult_right_mono)
next
  case goal6
  thus ?case
    by (cases "a = b") (auto simp: field_simps intro!: exI[where x= "(a - x) / (a - b)"])
next
  case goal7
  thus ?case
    by (auto simp: algebra_simps)
next
  case goal8
  thus ?case
    by (auto intro!: exI[where x="1/2"] simp: algebra_simps)
qed

lemma linear_compose: "(\<lambda>xa. a + xa * b) = (\<lambda>x. a + x) o (\<lambda>x. x * b)"
  by auto

lemma image_linear_atLeastAtMost: "(\<lambda>xa. a + xa * b) ` {c..d::real} =
  (if c \<le> d then if b > 0 then {a + c * b .. a + d * b} else {a + d * b .. a + c * b} else {})"
  by (simp add: linear_compose image_comp [symmetric] image_mult_atLeastAtMost image_add_atLeastAtMost)

lemma insert_atMost[simp]: "insert t {..t::'a::preorder} = {..t}" by auto

lemma insert_atLeastAtMost[simp]:
  "s \<ge> 0 \<Longrightarrow> insert t {t..s + t::'a::ordered_ab_group_add} = {t .. s + t}" by auto

lemma uminus_uminus_image[simp]:
  fixes x::"'a::group_add set"
  shows "uminus ` uminus ` x = x"
  by force

lemma Ball_singleton: "Ball {x} f = f x"
  by simp

lemma is_real_interval_union: fixes X Y::"real set"
  shows "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> (X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {}) \<Longrightarrow> is_interval (X \<union> Y)"
  unfolding is_interval_def Basis_real_def Ball_singleton real_inner_1_right
  by safe (metis (mono_tags, hide_lams) all_not_in_conv disjoint_iff_not_equal le_cases)+

lemma is_interval_translation:
  shows "is_interval X \<Longrightarrow> is_interval (op + x ` X)"
  unfolding is_interval_def
  apply safe
  apply (rule image_eqI[where x="xb - x" for xb])
  apply fastforce
  unfolding algebra_simps
  by (smt diff_add_cancel inner_left_distrib)

lemma is_interval_neg_translation:
  shows "is_interval X \<Longrightarrow> is_interval (op - x ` X)"
  unfolding is_interval_def
  apply safe
  apply (rule_tac x="x - xb" in image_eqI)
  apply fastforce
  unfolding algebra_simps
  by (smt diff_add_cancel inner_left_distrib)

lemma
  fixes a::"'a::ordered_euclidean_space"
  shows is_interval_ci: "is_interval {a..}"
    and is_interval_ic: "is_interval {..a}"
  by (force simp: is_interval_def eucl_le[where 'a='a])+

lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
  using is_interval_neg_translation[of x 0] is_interval_neg_translation[of "uminus ` x" 0]
  by (auto simp: diff_0[abs_def] )


subsection {* Euclidean Components *}

lemma sqrt_le_rsquare:
  assumes "\<bar>x\<bar> \<le> sqrt y"
  shows "x\<^sup>2 \<le> y"
  using assms real_sqrt_le_iff[of "x\<^sup>2"] by simp

lemma setsum_ge_element:
  fixes f::"'a \<Rightarrow> ('b::ordered_comm_monoid_add)"
  assumes "finite s"
  assumes "i \<in> s"
  assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<ge> 0"
  assumes "el = f i"
  shows "el \<le> setsum f s"
proof -
  have "el = setsum f {i}" by (simp add: assms)
  also have "... \<le> setsum f s" using assms by (intro setsum_mono2) auto
  finally show ?thesis .
qed

lemma norm_nth_le:
  fixes x::"'a::euclidean_space"
  assumes "i \<in> Basis"
  shows "norm (x \<bullet> i) \<le> norm x"
  unfolding norm_conv_dist euclidean_dist_l2[of x] setL2_def
  by (auto intro!: real_le_rsqrt setsum_ge_element assms)

lemma norm_Pair_le:
  shows "norm (x, y) \<le> norm x + norm y"
  unfolding norm_Pair
  by (metis norm_ge_zero sqrt_sum_squares_le_sum)

lemma norm_Pair_ge1:
  shows "norm x \<le> norm (x, y)"
  unfolding norm_Pair
  by (metis real_sqrt_sum_squares_ge1)

lemma norm_Pair_ge2:
  shows "norm y \<le> norm (x, y)"
  unfolding norm_Pair
  by (metis real_sqrt_sum_squares_ge2)

subsection {* Operator Norm *}

lemma onorm_scaleR_left_lemma:
  assumes r: "bounded_linear r"
  shows "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
proof (rule onorm_bound)
  show "0 \<le> onorm r * norm f"
    by (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le r)
next
  fix x
  have "norm (r x *\<^sub>R f) = norm (r x) * norm f"
    by simp
  also have "\<dots> \<le> onorm r * norm x * norm f"
    by (intro mult_right_mono onorm r norm_ge_zero)
  finally show "norm (r x *\<^sub>R f) \<le> onorm r * norm f * norm x"
    by (simp add: ac_simps)
qed

lemmas bounded_linear_scaleR_const = bounded_linear_scaleR_left[THEN bounded_linear_compose]

lemma onorm_scaleR_left:
  assumes f: "bounded_linear r"
  shows "onorm (\<lambda>x. r x *\<^sub>R f) = onorm r * norm f"
proof (cases "f = 0")
  assume "f \<noteq> 0"
  show ?thesis
  proof (rule order_antisym)
    show "onorm (\<lambda>x. r x *\<^sub>R f) \<le> onorm r * norm f"
      using f by (rule onorm_scaleR_left_lemma)
  next
    have bl1: "bounded_linear (\<lambda>x. r x *\<^sub>R f)"
      by (metis bounded_linear_scaleR_const f)
    have "bounded_linear (\<lambda>x. r x * norm f)"
      by (metis bounded_linear_mult_const f)
    from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"]
    have "onorm r \<le> onorm (\<lambda>x. r x * norm f) * inverse (norm f)"
      using `f \<noteq> 0`
      by (simp add: inverse_eq_divide)
    also have "onorm (\<lambda>x. r x * norm f) \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
      by (rule onorm_bound) (auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm])
    finally show "onorm r * norm f \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
      using `f \<noteq> 0`
      by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
  qed
qed (simp add: onorm_zero)

lemma onorm_id_le: "onorm (\<lambda>x. x) \<le> 1"
  by (rule onorm_bound) simp_all

lemma onorm_id: "onorm (\<lambda>x. x::'a::{real_normed_vector, perfect_space}) = 1"
proof (rule antisym[OF onorm_id_le])
  have "{0::'a} \<noteq> UNIV" by (metis not_open_singleton open_UNIV)
  then obtain x :: 'a where "x \<noteq> 0" by fast
  hence "1 \<le> norm x / norm x"
    by simp
  also have "\<dots> \<le> onorm (\<lambda>x::'a. x)"
    by (rule le_onorm) (rule bounded_linear_ident)
  finally show "1 \<le> onorm (\<lambda>x::'a. x)" .
qed

lemma onorm_setsum_le:
  assumes "finite S"
  assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
  shows "onorm (\<lambda>x. setsum (\<lambda>s. f s x) S) \<le> setsum (\<lambda>s. onorm (f s)) S"
  using assms
  by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_setsum)

lemma onorm_componentwise:
  assumes "bounded_linear f"
  shows "onorm f \<le> (\<Sum>i\<in>Basis. norm (f i))"
proof -
  {
    fix i::'a
    assume "i \<in> Basis"
    hence "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> onorm (\<lambda>x. (x \<bullet> i)) * norm (f i)"
      by (auto intro!: onorm_scaleR_left_lemma)
    also have "\<dots> \<le>  norm i * norm (f i)"
      by (rule mult_right_mono) (auto simp: ac_simps Cauchy_Schwarz_ineq2 intro!: onorm_le)
    finally have "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> norm (f i)" using `i \<in> Basis`
      by simp
  } hence "onorm (\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<le> (\<Sum>i\<in>Basis. norm (f i))"
    by (auto intro!: order_trans[OF onorm_setsum_le] bounded_linear_scaleR_const setsum_mono)
  also have "(\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) = (\<lambda>x. f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i))"
    by (simp add: linear_setsum bounded_linear.linear assms linear_simps)
  also have "\<dots> = f"
    by (simp add: euclidean_representation)
  finally show ?thesis .
qed

lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]

subsection {* Limits *}

lemma not_in_closure_trivial_limitI: "x \<notin> closure s \<Longrightarrow> trivial_limit (at x within s)"
  using not_trivial_limit_within[of x s]
  apply auto
  by (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)

lemma tendsto_If:
  assumes tendsto:
    "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow> (f ---> l x) (at x within s \<union> (closure s \<inter> closure t))"
    "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow> (g ---> l x) (at x within t \<union> (closure s \<inter> closure t))"
  assumes "x \<in> s \<union> t"
  shows "((\<lambda>x. if x \<in> s then f x else g x) ---> l x) (at x within s \<union> t)"
proof (rule Lim_Un, safe intro!: topological_tendstoI)
  fix S::"'b set"
  assume S: "open S"
  assume l: "l x \<in> S"
  let ?thesis = "\<lambda>t. eventually (\<lambda>x. (if x \<in> s then f x else g x) \<in> S) (at x within t)"
  {
    assume x: "x \<in> s" hence "x \<in> s \<union> (closure s \<inter> closure t)" by auto
    from topological_tendstoD[OF tendsto(1)[OF this] S l]
    have "?thesis s" unfolding eventually_at_filter
      by eventually_elim auto
  } moreover {
    assume c: "x \<notin> closure s"
    have "?thesis s"
      by (metis (no_types, lifting) c not_in_closure_trivial_limitI trivial_limit_eventually)
  } moreover {
    assume s: "x \<in> closure s" "x \<notin> s"
    hence t: "x \<in> t" "x \<in> closure t"
      using assms closure_subset[of t] by auto
    from s t have c1: "x \<in> s \<union> (closure s \<inter> closure t)"
      and c2: "x \<in> t \<union> (closure s \<inter> closure t)"by auto
    from topological_tendstoD[OF tendsto(1)[OF c1] S l]
      topological_tendstoD[OF tendsto(2)[OF c2] S l]
    have "?thesis s"
      unfolding eventually_at_filter
      by eventually_elim auto
  } ultimately show "?thesis s" by blast
  {
    assume x: "x \<in> closure s" "x \<in> closure t"
    hence c1: "x \<in> s \<union> (closure s \<inter> closure t)"
      and c2: "x \<in> t \<union> (closure s \<inter> closure t)"
      by auto
    from topological_tendstoD[OF tendsto(1)[OF c1] S l]
      topological_tendstoD[OF tendsto(2)[OF c2] S l]
    have "?thesis t" unfolding eventually_at_filter
      by eventually_elim auto
  } moreover {
    assume c: "x \<notin> closure t"
    have "?thesis t"
      by (metis (no_types, lifting) c not_in_closure_trivial_limitI trivial_limit_eventually)
  } moreover {
    assume c: "x \<notin> closure s"
    hence c': "x \<in> t \<union> (closure s \<inter> closure t)"
      using assms closure_subset[of s]
      by auto
    from c have "eventually (\<lambda>x. x \<in> - closure s) (at x within t)"
      apply (intro topological_tendstoD)
      apply (auto intro: tendsto_ident_at)
      done
    hence "?thesis t"
      using topological_tendstoD[OF tendsto(2)[OF c'] S l] closure_subset[of s]
      unfolding eventually_at_filter
      apply eventually_elim
      apply auto
      apply (metis closure_subset contra_subsetD)+
      done
  } ultimately show "?thesis t" by blast
qed


subsection {* Continuity *}

lemma continuous_on_fst[continuous_intros]: "continuous_on X fst"
  unfolding continuous_on_def
  by (intro ballI tendsto_intros)

lemma continuous_on_snd[continuous_intros]: "continuous_on X snd"
  unfolding continuous_on_def
  by (intro ballI tendsto_intros)

lemma continuous_at_fst[continuous_intros]:
  fixes x::"'a::euclidean_space \<times> 'b::euclidean_space"
  shows "continuous (at x) fst"
  unfolding continuous_def netlimit_at
  by (intro tendsto_intros)

lemma continuous_at_snd[continuous_intros]:
  fixes x::"'a::euclidean_space \<times> 'b::euclidean_space"
  shows "continuous (at x) snd"
  unfolding continuous_def netlimit_at
  by (intro tendsto_intros)

lemma continuous_at_Pair[continuous_intros]:
  fixes x::"'a::euclidean_space \<times> 'b::euclidean_space"
  assumes "continuous (at x) f"
  assumes "continuous (at x) g"
  shows "continuous (at x) (\<lambda>x. (f x, g x))"
  using assms unfolding continuous_def
  by (intro tendsto_intros)

lemma continuous_on_Pair[continuous_intros]:
  assumes "continuous_on S f"
  assumes "continuous_on S g"
  shows "continuous_on S (\<lambda>x. (f x, g x))"
  using assms unfolding continuous_on_def
  by (auto intro: tendsto_intros)

lemma continuous_Sigma:
  assumes defined: "y \<in> Pi T X"
  assumes f_cont: "continuous_on (Sigma T X) f"
  assumes y_cont: "continuous_on T y"
  shows "continuous_on T (\<lambda>x. f (x, y x))"
  using continuous_on_compose2[OF continuous_on_subset[where t="(\<lambda>x. (x, y x)) ` T", OF f_cont]
                                  continuous_on_Pair[OF continuous_on_id y_cont]] defined
  by auto

lemma IVT'_closed_segment_real:
  fixes f :: "real \<Rightarrow> real"
  assumes y: "y \<in> closed_segment (f a) (f b)"
  assumes *: "continuous_on (closed_segment a b) f"
  shows "\<exists>x \<in> closed_segment a b. f x = y"
proof -
  {
    assume "a \<le> b"
    {
      assume "f a \<le> f b"
      hence ?thesis
        using IVT'[of f a y b] `a \<le> b` assms by (auto simp: closed_segment_real)
    } moreover {
      assume "f b < f a"
      hence ?thesis
        using IVT'[of "-f" a "-y" b] `a \<le> b` assms
        by (force simp: closed_segment_real intro!: continuous_on_minus)
    } ultimately have ?thesis by arith
  } moreover {
    assume "b < a"
    {
      assume "f b < f a"
      hence ?thesis
        using IVT'[of f b y a] `b < a` assms by (auto simp: closed_segment_real)
    } moreover {
      assume "f b \<ge> f a"
      hence ?thesis
        using IVT'[of "-f" b "-y" a] `b < a` assms
        by (force simp: closed_segment_real intro!: continuous_on_minus)
    } ultimately have ?thesis by arith
  } ultimately show ?thesis by arith
qed

subsection {* Differentiability *}

lemma differentiable_Pair [simp]:
  "f differentiable at x within s \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. (f x, g x)) differentiable at x within s"
  unfolding differentiable_def by (blast intro: has_derivative_Pair)

lemma (in bounded_linear)
  differentiable:
  assumes "g differentiable (at x within s)"
  shows " (\<lambda>x. f (g x)) differentiable (at x within s)"
  using assms[simplified frechet_derivative_works]
  by (intro differentiableI) (rule has_derivative)

lemmas
  differentiable_mult_right[intro] = bounded_linear.differentiable[OF bounded_linear_mult_right] and
  differentiable_mult_left[intro] = bounded_linear.differentiable[OF bounded_linear_mult_left] and
  differentiable_inner_right[intro] = bounded_linear.differentiable[OF bounded_linear_inner_right] and
  differentiable_inner_left[intro] = bounded_linear.differentiable[OF bounded_linear_inner_left]

lemma (in bounded_bilinear)
  differentiable:
  assumes f: "f differentiable at x within s" and g: "g differentiable at x within s"
  shows "(\<lambda>x. prod (f x) (g x)) differentiable at x within s"
  using assms[simplified frechet_derivative_works]
  by (intro differentiableI) (rule FDERIV)

lemmas
  differentiable_mult[intro] = bounded_bilinear.differentiable[OF bounded_bilinear_mult] and
  differentiable_scaleR[intro] = bounded_bilinear.differentiable[OF bounded_bilinear_scaleR]

lemma differentiable_transform_within_weak:
  assumes "x \<in> s" "\<And>x'. x'\<in>s \<Longrightarrow> g x' = f x'" "f differentiable at x within s"
  shows "g differentiable at x within s"
  using assms by (intro differentiable_transform_within[OF zero_less_one, where g=g]) auto

lemma differentiable_compose_at:
  "f differentiable (at x) \<Longrightarrow> g differentiable (at (f x)) \<Longrightarrow> (\<lambda>x. g (f x)) differentiable (at x)"
  unfolding o_def[symmetric]
  by (rule differentiable_chain_at)

lemma differentiable_compose_within:
  "f differentiable (at x within s) \<Longrightarrow> g differentiable (at(f x) within (f ` s)) \<Longrightarrow>
  (\<lambda>x. g (f x)) differentiable (at x within s)"
  unfolding o_def[symmetric]
  by (rule differentiable_chain_within)

lemma differentiable_setsum[intro, simp]:
  assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
  shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net"
proof-
 guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] ..
 thus ?thesis unfolding differentiable_def apply-
   apply(rule,rule has_derivative_setsum[where f'=f'])
   by auto
qed

subsection {* Derivatives *}

lemma has_derivative_singletonI: "bounded_linear g \<Longrightarrow> (f has_derivative g) (at x within {x})"
  by (rule has_derivativeI_sandwich[where e=1]) (auto intro!: bounded_linear_scaleR_left)

lemma vector_derivative_eq_rhs: "(f has_vector_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_vector_derivative g') F"
  by simp

lemma has_derivative_transform:
  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
  assumes "(f has_derivative f') (at x within s)"
  shows "(g has_derivative f') (at x within s)"
  using assms by (intro has_derivative_transform_within[OF zero_less_one, where g=g]) auto

lemma has_derivative_within_If_eq:
  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
    (bounded_linear f' \<and>
     ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)
           else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
      ---> 0) (at x within s))"
  (is "_ = (_ \<and> (?if ---> 0) _)")
proof -
  have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
           ((if P y then f y else g y) -
            ((if P x then f x else g x) + f' (y - x)))) = ?if"
    by (auto simp: inverse_eq_divide)
  thus ?thesis by (auto simp: has_derivative_within)
qed

lemma has_derivative_If:
  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow> (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow> (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
  assumes x_in: "x \<in> s \<union> t"
  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
proof -
  from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)" by (auto simp add: has_derivative_within)
  from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)" by (auto simp add: has_derivative_within)
  have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
    apply default
    using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in
    apply force+
    done
  show ?thesis
    unfolding has_derivative_within_If_eq
    apply rule
    apply (rule bl)
    apply (rule tendsto_If[OF _ _ x_in])
    using f' g' closure_subset[of t] closure_subset[of s]
    apply (auto simp add: has_derivative_within inverse_eq_divide connect connect' set_mp)
    done
qed

lemma has_vector_derivative_If:
  assumes x_in: "x \<in> s \<union> t"
  assumes "u = s \<union> t"
  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow> (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow> (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
  shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative (if x \<in> s then f' x else g' x)) (at x within u)"
  unfolding has_vector_derivative_def assms
  apply (rule has_derivative_If[THEN has_derivative_eq_rhs])
  apply (rule f'[unfolded has_vector_derivative_def]) apply assumption
  apply (rule g'[unfolded has_vector_derivative_def]) apply assumption
  using x_in
  apply (auto simp: assms)
  done

lemma has_derivative_If_in_closed:
  assumes f':"\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)"
  assumes g':"\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)"
  assumes connect: "\<And>x. x \<in> s \<inter> t \<Longrightarrow> f x = g x" "\<And>x. x \<in> s \<inter> t \<Longrightarrow> f' x = g' x"
  assumes "closed t" "closed s" "x \<in> s \<union> t"
  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
  apply (rule has_derivative_If)
  using assms
  apply auto
  apply (metis Int_lower2 Un_absorb2)+
  done

lemma has_derivative_If_containing_closures:
  assumes f': "x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)"
  assumes g': "x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)"
  assumes connect: "x \<in> s \<Longrightarrow> x \<in> t \<Longrightarrow> f x = g x"
  assumes connect': "x \<in> s \<Longrightarrow> x \<in> t \<Longrightarrow> f' x = g' x"
  assumes x_in: "x \<in> s \<union> t"
  assumes contains: "closure s \<inter> closure t \<subseteq> s" "closure s \<inter> closure t \<subseteq> t"
  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
  apply (rule has_derivative_If)
  using assms
  apply (auto )
  by (metis Int_iff subset_eq sup.orderE)+

lemma linear_continuation:
  assumes f':"\<And>x. x \<in> {a .. b} \<Longrightarrow> (f has_vector_derivative f' x) (at x within {a .. b})"
  assumes g':"\<And>x. x \<in> {b .. c} \<Longrightarrow> (g has_vector_derivative g' x) (at x within {b .. c})"
  assumes connect: "f b = g b" "f' b = g' b"
  assumes x: "x \<in> {a .. c}"
  assumes abc:"a \<le> b" "b \<le> c"
  shows "((\<lambda>x. if x \<le> b then f x else g x) has_vector_derivative
  (\<lambda>x. if x \<le> b then f' x else g' x) x) (at x within {a .. c})"
  (is "(?h has_vector_derivative ?h' x) _")
proof -
  have un: "{a .. b} \<union> {b .. c} = {a .. c}" using assms by auto
  note has_derivative_If_in_closed[derivative_intros]
  note f'[simplified has_vector_derivative_def, derivative_intros]
  note g'[simplified has_vector_derivative_def, derivative_intros]
  have if': "((\<lambda>x. if x \<in> {a .. b} then f x else g x) has_vector_derivative
    (\<lambda>x. if x \<le> b then f' x else g' x) x) (at x within {a .. b}\<union>{b .. c})"
    unfolding has_vector_derivative_def
    using assms
    apply -
    apply (rule derivative_eq_intros refl | assumption)+
    apply auto
    done
  show ?thesis
    unfolding has_vector_derivative_def
    by (rule has_derivative_transform[OF x _ if'[simplified un has_vector_derivative_def]]) simp
qed

lemma exists_linear_continuation:
  assumes f':"\<And>x. x \<in> {a .. b} \<Longrightarrow> (f has_vector_derivative f' x) (at x within {a .. b})"
  shows "\<exists>fc. (\<forall>x. x \<in> {a .. b} \<longrightarrow> (fc has_vector_derivative f' x) (at x)) \<and>
    (\<forall>x. x \<in> {a .. b} \<longrightarrow> fc x = f x)"
proof (rule, safe)
  fix x assume "x \<in> {a .. b}" hence "a \<le> b" by simp
  let ?line = "\<lambda>a x. f a + (x - a) *\<^sub>R f' a"
  let ?fc = "(\<lambda>x. if x \<in> {a .. b} then f x else if x \<in> {..a} then ?line a x else ?line b x)"
  have [simp]:
    "\<And>x. x \<in> {a .. b} \<Longrightarrow> (b \<le> x \<longleftrightarrow> x = b)" "\<And>x. x \<in> {a .. b} \<Longrightarrow> (x \<le> a \<longleftrightarrow> x = a)"
    "\<And>x. x \<le> a \<Longrightarrow> (b \<le> x \<longleftrightarrow> x = b)" using `a \<le> b` by auto
  note has_derivative_If_in_closed[derivative_intros] f'[simplified has_vector_derivative_def, derivative_intros]
  have "(?fc has_vector_derivative f' x) (at x within {a .. b} \<union> ({..a} \<union> {b..}))"
    using `x \<in> {a .. b}` `a \<le> b`
    by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def
      simp del: atMost_iff atLeastAtMost_iff)
  moreover have "{a .. b} \<union> ({..a} \<union> {b..}) = UNIV" by auto
  ultimately show "(?fc has_vector_derivative f' x) (at x)" by simp
  show "?fc x = f x" using `x \<in> {a .. b}` by simp
qed


lemma Pair_has_vector_derivative:
  assumes f: "(f has_vector_derivative f') (at x within s)"
      and g: "(g has_vector_derivative g') (at x within s)"
  shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
  using assms by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)

lemma has_vector_derivative_imp:
  assumes "x \<in> s"
  assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
  assumes f'g':"f' = g'"
  assumes "x = y" "s = t"
  assumes f': "(f has_vector_derivative f') (at x within s)"
  shows "(g has_vector_derivative g') (at y within t)"
  unfolding has_vector_derivative_def has_derivative_within'
proof (safe)
  fix e::real
  assume "0 < e"
  with assms f' have "\<exists>d>0. \<forall>x'\<in>s.
    0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
    norm (g x' - g y - (x' - y) *\<^sub>R g') / norm (x' - x) < e"
    by (auto simp add: has_vector_derivative_def has_derivative_within')
  then guess d ..
  with assms show "\<exists>d>0. \<forall>x'\<in>t. 0 < norm (x' - y) \<and> norm (x' - y) < d \<longrightarrow>
    norm (g x' - g y - (x' - y) *\<^sub>R g') / norm (x' - y) < e"
    by auto
next
  show "bounded_linear (\<lambda>x. x *\<^sub>R g')"
    using has_derivative_bounded_linear[OF f'[simplified has_vector_derivative_def], simplified f'g'] assms
    by simp
qed

lemma has_vector_derivative_cong:
  assumes "x \<in> s"
  assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
  assumes f'g':"f' = g'"
  assumes "x = y" "s = t"
  shows "(f has_vector_derivative f') (at x within s) =
    (g has_vector_derivative g') (at y within t)"
proof
  assume "(f has_vector_derivative f') (at x within s)"
  from has_vector_derivative_imp this assms
  show "(g has_vector_derivative g') (at y within t)"
    by blast
next
  assume g': "(g has_vector_derivative g') (at y within t)"
  show "(f has_vector_derivative f') (at x within s)"
    using assms g'
    by (intro has_vector_derivative_imp[where f=g and g=f and f'=g' and g'=f'])
      auto
qed

lemma has_derivative_within_union:
  assumes "(f has_derivative g) (at x within s)"
  assumes "(f has_derivative g) (at x within t)"
  shows  "(f has_derivative g) (at x within (s \<union> t))"
proof cases
  assume "at x within (s \<union> t) = bot"
  thus ?thesis using assms by (simp_all add: has_derivative_def)
next
  assume st: "at x within (s \<union> t) \<noteq> bot"
  thus ?thesis
    using assms
    apply (auto simp: Lim_within_union has_derivative_def)
    apply (cases "at x within s = bot", simp_all add: netlimit_within)
    apply (cases "at x within t = bot", simp_all add: netlimit_within)
    done
qed

lemma has_vector_derivative_within_union:
  assumes "(f has_vector_derivative g) (at x within s)"
  assumes "(f has_vector_derivative g) (at x within t)"
  shows  "(f has_vector_derivative g) (at x within (s \<union> t))"
using assms
by (auto simp: has_vector_derivative_def intro: has_derivative_within_union)

lemma vector_derivative_within_closed_interval:
  fixes f::"real \<Rightarrow> 'a::euclidean_space"
  assumes "a < b" and "x \<in> {a .. b}"
  assumes "(f has_vector_derivative f') (at x within {a .. b})"
  shows "vector_derivative f (at x within {a .. b}) = f'"
  apply(rule vector_derivative_unique_within_closed_interval)
  using vector_derivative_works[unfolded differentiable_def]
  using assms by (auto simp add: has_vector_derivative_def)

lemma
  has_vector_derivative_at_within_open_subset:
  assumes "\<And>x. x \<in> T \<Longrightarrow> (f has_vector_derivative f' x) (at x within T)"
  assumes "x \<in> S" "open S" "S \<subseteq> T"
  shows "(f has_vector_derivative f' x) (at x)"
proof -
  from at_within_open[OF assms(2,3), symmetric]
  show "(f has_vector_derivative f' x) (at x)"
    using `S \<subseteq> T`
    by (auto intro!: has_vector_derivative_within_subset[OF _ `S \<subseteq> T`] assms)
qed


text {* TODO: include this into the attribute DERIV-intros?! *}

lemma DERIV_compose_FDERIV:
  fixes f::"real\<Rightarrow>real"
  assumes "DERIV f (g x) :> f'"
  assumes "(g has_derivative g') (at x within s)"
  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
  using assms has_derivative_compose[of g g' x s f "op * f'"]
  by (auto simp: has_field_derivative_def ac_simps)

lemmas has_derivative_sin[derivative_intros] = DERIV_sin[THEN DERIV_compose_FDERIV]
  and  has_derivative_cos[derivative_intros] = DERIV_cos[THEN DERIV_compose_FDERIV]
  and  has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV]
  and  has_derivative_ln[derivative_intros] = DERIV_ln[THEN DERIV_compose_FDERIV]

lemma has_derivative_continuous_on:
  "(\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
  by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def)

lemma has_vector_derivative_continuous_on:
  "(\<And>x. x \<in> s \<Longrightarrow> (f has_vector_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
  by (auto intro!: differentiable_imp_continuous_on differentiableI simp: has_vector_derivative_def
    differentiable_on_def)

lemma taylor_up_within:
  assumes INIT: "n>0" "\<And>t. t \<in> {a .. b} \<Longrightarrow> diff 0 t = f t"
  and DERIV: "\<And>m t. m < n \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
    ((diff m) has_vector_derivative (diff (Suc m) t)) (at t within {a .. b})"
  and INTERV: "a \<le> c" "c < b"
  shows "\<exists>t. c < t & t < b &
    f b = (\<Sum>m<n. (diff m c / real (fact m)) * (b - c)^m)+
      (diff n t / real (fact n)) * (b - c)^n" (is "?taylor f diff")
proof -
  from exists_linear_continuation[of a b, OF DERIV]
  have "\<forall>m. \<exists>d'. m < n \<longrightarrow>
    (\<forall>x \<in> {a .. b}. (d' has_vector_derivative diff (Suc m) x) (at x) \<and> d' x = diff m x)"
    by (metis atLeastAtMost_iff)
  then guess d' unfolding choice_iff .. note d' = this
  let ?diff = "\<lambda>m. if m = n then diff m else d' m"
  have "?taylor (?diff 0) ?diff" using d'
    by (intro taylor_up[OF _ _ _ `a \<le> c`])
       (auto simp: has_field_derivative_def has_vector_derivative_def INIT INTERV mult_commute_abs)
  thus "?taylor f diff" using d' INTERV INIT by auto
qed

lemma taylor_up_within_vector:
  fixes f::"real \<Rightarrow> 'a::euclidean_space"
  assumes INIT: "n>0" "\<And>t. t \<in> {a .. b} \<Longrightarrow> diff 0 t = f t"
  and DERIV: "\<And>m t. m < n \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
    ((diff m) has_vector_derivative (diff (Suc m) t)) (at t within {a .. b})"
  and INTERV: "a \<le> c" "c < b"
  shows "\<exists>t. (\<forall>i\<in>Basis::'a set. c < t i & t i < b) \<and>
    f b = setsum (%m. (b - c)^m *\<^sub>R (diff m c /\<^sub>R real (fact m))) {..<n} +
      setsum (\<lambda>x. (((b - c) ^ n *\<^sub>R diff n (t x) /\<^sub>R real (fact n)) \<bullet> x) *\<^sub>R x) Basis"
proof -
  obtain t where t: "\<forall>i\<in>Basis::'a set. t i > c \<and> t i < b \<and>
    f b \<bullet> i =
      (\<Sum>m<n. diff m c \<bullet> i / real (fact m) * (b - c) ^ m) +
      diff n (t i) \<bullet> i / real (fact n) * (b - c) ^ n"
  proof (atomize_elim, rule bchoice, safe)
    fix i::'a
    assume "i \<in> Basis"
    have DERIV_0: "\<And>t. t \<in> {a .. b} \<Longrightarrow> (diff 0) t \<bullet> i = f t \<bullet> i" using INIT by simp
    have DERIV_Suc: "\<And>m t. m < n \<Longrightarrow> a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow>
      ((\<lambda>t. (diff m) t \<bullet> i) has_vector_derivative (diff (Suc m) t \<bullet> i)) (at t within {a .. b})"
      using DERIV by (auto intro!: derivative_eq_intros simp: has_vector_derivative_def)
    from taylor_up_within[OF INIT(1) DERIV_0 DERIV_Suc INTERV]
    show "\<exists>t>c. t < b \<and> f b \<bullet> i =
      (\<Sum>m<n. diff m c \<bullet> i / real (fact m) * (b - c) ^ m) +
      diff n t \<bullet> i / real (fact n) * (b - c) ^ n" by simp
  qed
  have "f b = (\<Sum>i\<in>Basis. (f b \<bullet> i) *\<^sub>R i)" by (rule euclidean_representation[symmetric])
  also have "\<dots> =
      (\<Sum>i\<in>Basis. ((\<Sum>m<n. (b - c) ^ m *\<^sub>R (diff m c /\<^sub>R real (fact m))) \<bullet> i) *\<^sub>R i) +
      (\<Sum>x\<in>Basis. (((b - c) ^ n *\<^sub>R diff n (t x) /\<^sub>R real (fact n)) \<bullet> x) *\<^sub>R x)"
    using t by (simp add: setsum.distrib inner_setsum_left inverse_eq_divide algebra_simps)
  finally show ?thesis using t by (auto simp: euclidean_representation)
qed

lemma mvt_closed_segmentE:
  fixes f::"real\<Rightarrow>real"
  assumes "\<And>x. x \<in> closed_segment a b \<Longrightarrow> (f has_vector_derivative f' x) (at x within closed_segment a b)"
  obtains y where "y \<in> closed_segment a b"  "f b - f a = (b - a) * f' y"
proof cases
  assume "a \<le> b"
  with mvt_very_simple[of a b f "\<lambda>x i. i *\<^sub>R f' x"] assms
  obtain y where "y \<in> closed_segment a b"  "f b - f a = (b - a) * f' y"
    by (auto simp: has_vector_derivative_def closed_segment_real)
  thus ?thesis ..
next
  assume "\<not> a \<le> b"
  with mvt_very_simple[of b a f "\<lambda>x i. i *\<^sub>R f' x"] assms
  obtain y where "y \<in> closed_segment a b"  "f b - f a = (b - a) * f' y"
    by (force simp: has_vector_derivative_def closed_segment_real algebra_simps)
  thus ?thesis ..
qed

lemma mvt_more_general_open_segment:
  fixes a :: "real"
    and b :: "real"
    and f :: "real \<Rightarrow> 'a::real_normed_vector"
    and f' :: "real \<Rightarrow> 'a"
  assumes "continuous_on (closed_segment a b) f"
  assumes "continuous_on (closed_segment a b) g"
    and "\<And>x. x \<in> open_segment a b \<Longrightarrow> (f has_vector_derivative f' x) (at x within open_segment a b)"
    and "\<And>x. x \<in> open_segment a b \<Longrightarrow> (g has_vector_derivative g' x) (at x within open_segment a b)"
    and "\<And>x. x \<in> open_segment a b \<Longrightarrow> norm (f' x) \<le> g' x"
  shows "norm (f b - f a) \<le> abs (g b - g a)"
proof -
  {
    assume "a = b"
    hence ?thesis by simp
  } moreover {
    assume "a < b"
    with assms
    have "continuous_on {a .. b} f"
      and "continuous_on {a .. b} g"
      and "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
      and "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
      and "\<And>x. x\<in>{a<..<b} \<Longrightarrow> norm (f' x) \<le> g' x"
      by (auto simp: open_segment_real closed_segment_real at_within_open[where S="{a<..<b}"])
    from mvt_more_general[OF `a < b` this]
    have ?thesis
      apply (auto)
      by (metis abs_of_nonneg norm_ge_zero order_trans)
  } moreover {
    assume "b < a"
    with assms
    have "continuous_on {b .. a} f"
      and "continuous_on {b .. a} g"
      and "\<And>x. x\<in>{b<..<a} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
      and "\<And>x. x\<in>{b<..<a} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
      and "\<And>x. x\<in>{b<..<a} \<Longrightarrow> norm (f' x) \<le> g' x"
      by (auto simp: open_segment_real closed_segment_real at_within_open[where S="{b<..<a}"])
    from mvt_more_general[OF `b < a` this]
    have ?thesis
      apply auto
      by (metis abs_of_nonneg norm_ge_zero norm_minus_commute order_trans real_norm_def)
  } ultimately show ?thesis by arith
qed

subsection {* Integration *}

lemmas content_real[simp]

lemma integral_real_singleton[simp]:
  "integral {a::real} f = 0"
  using integral_refl[of a f] by simp
lemmas integrable_continuous[intro, simp]
  and integrable_continuous_real[intro, simp]

lemma integral_combine2:
  fixes f :: "real \<Rightarrow> 'a::banach"
  assumes "a \<le> c" and "c \<le> b" and "f integrable_on {a..b}"
  shows "integral {c..b} f + integral {a..c} f = integral {a..b} f"
  using integral_combine[OF assms] by (simp add: ac_simps)

lemma indefinite_integral2_continuous:
  fixes f::"real\<Rightarrow>'a::banach"
  assumes "f integrable_on {a..b}"
  shows "continuous_on {a..b} (\<lambda>x. integral {x..b} f)"
proof -
  have "\<forall>x \<in> {a .. b}. integral {a..b} f - integral {a..x} f = integral {x..b} f"
    using assms
    by (auto simp: algebra_simps integral_combine2)
  thus ?thesis
    by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous assms)
qed

lemma integral2_has_vector_derivative:
  fixes f :: "real \<Rightarrow> 'a::banach"
  assumes "continuous_on {a .. b} f"
    and "x \<in> {a .. b}"
  shows "((\<lambda>u. integral {u .. b} f) has_vector_derivative - f x) (at x within {a .. b})"
proof -
  have *: "((\<lambda>u. integral {a .. b} f - integral {a .. u} f) has_vector_derivative - f x) (at x within {a .. b})"
    unfolding has_vector_derivative_def
    apply (rule derivative_eq_intros)
    apply (rule derivative_intros)
    apply (subst has_vector_derivative_def[symmetric])
    apply (rule integral_has_vector_derivative)
    using assms by auto
  show ?thesis
    using assms
    by (auto simp: algebra_simps integral_combine2 intro!: has_vector_derivative_imp[OF _ _ _ _ _ *])
qed

lemma mvt_integral:
  fixes f::"'a::euclidean_space\<Rightarrow>'b::euclidean_space"
  assumes f'[derivative_intros]: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
  assumes f'_cont: "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>t. f' t i)"
  assumes line_in: "\<And>t. t \<in> {0..1} \<Longrightarrow> x + t *\<^sub>R y \<in> S"
  shows "f (x + y) - f x = integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) y)" (is ?th1)
   and  "f (x + y) - f x = (\<Sum>a\<in>Basis. (y \<bullet> a) *\<^sub>R integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) a))" (is ?th2)
proof -
  from assms have subset: "(\<lambda>xa. x + xa *\<^sub>R y) ` {0..1} \<subseteq> S" by auto
  note has_derivative_subset[OF _ subset, derivative_intros]
  note has_derivative_in_compose[where f="(\<lambda>xa. x + xa *\<^sub>R y)" and g = f, derivative_intros]
  note continuous_on_compose2[where f="(\<lambda>xa. x + xa *\<^sub>R y)", continuous_intros]
  note continuous_on_subset[OF _ subset, continuous_intros]
  have "\<And>t. t \<in> {0..1} \<Longrightarrow>
    ((\<lambda>t. f (x + t *\<^sub>R y)) has_vector_derivative f' (x + t *\<^sub>R y) y) (at t within {0..1})"
    using assms
    by (auto simp: has_vector_derivative_def linear_cmul[OF has_derivative_linear[OF f'], symmetric]
      intro!: derivative_eq_intros)
  from fundamental_theorem_of_calculus[rule_format, OF _ this]
  show ?th1
    by (auto intro!: integral_unique[symmetric])

  also have "integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) y) =
    integral {0..1} (\<lambda>t. (\<Sum>i\<in>Basis. (f' (x + t *\<^sub>R y) y \<bullet> i) *\<^sub>R i))"
    by (simp add: euclidean_representation)
  also have "\<dots> = integral {0..1}
     (\<lambda>t. \<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R (f' (x + t *\<^sub>R y) i))"
  proof (rule integral_spike[OF negligible_empty], safe)
    fix t::real assume t: "t \<in> {0 .. 1}"
    have "(\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R f' (x + t *\<^sub>R y) i) =
      (\<Sum>i\<in>Basis. \<Sum>a\<in>Basis. (y \<bullet> a) *\<^sub>R (f' (x + t *\<^sub>R y) a \<bullet> i) *\<^sub>R i)"
      by (subst setsum.commute[symmetric])
        (simp only: scaleR_setsum_right[symmetric] euclidean_representation)
    also have "\<dots> = (\<Sum>i\<in>Basis. (f' (x + t *\<^sub>R y) y \<bullet> i) *\<^sub>R i)"
      by (subst Derivative.linear_componentwise[OF has_derivative_linear[OF f'], OF line_in[OF t]])
        (simp add: scaleR_setsum_left)
    finally
    show "(\<Sum>i\<in>Basis. (y \<bullet> i) *\<^sub>R f' (x + t *\<^sub>R y) i) = (\<Sum>i\<in>Basis. (f' (x + t *\<^sub>R y) y \<bullet> i) *\<^sub>R i)" .
  qed
  also have "\<dots> = (\<Sum>a\<in>Basis. integral {0..1} (\<lambda>t. (y \<bullet> a) *\<^sub>R f' (x + t *\<^sub>R y) a))"
    by (subst integral_setsum) (auto intro!: continuous_intros f'_cont)
  also have "\<dots> = (\<Sum>a\<in>Basis. (y \<bullet> a) *\<^sub>R integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) a))"
    using assms
    by (intro setsum.cong[OF refl], subst integral_cmul)
      (auto intro!: continuous_intros f'_cont simp: integral_cmul)
  finally show ?th2 .
qed

lemma integral_mult:
  fixes K::real
  shows "f integrable_on X \<Longrightarrow> K * integral X f = integral X (\<lambda>x. K * f x)"
  unfolding real_scaleR_def[symmetric]
  apply (subst integral_cmul)
  by auto

lemma integrable_mult:
  fixes K::real
  shows "f integrable_on X \<Longrightarrow> (\<lambda>x. K * f x) integrable_on X "
  unfolding real_scaleR_def[symmetric]
  apply (subst integrable_cmul)
  by auto

lemma integrable_continuous_closed_segment:
  fixes f :: "real \<Rightarrow> 'a::banach"
  assumes "continuous_on (closed_segment a b) f"
  shows "f integrable_on (closed_segment a b)"
  using assms
  by (auto simp: closed_segment_real intro!: integrable_continuous_real)

subsection {* conditionally complete lattice *}

lemma bounded_imp_bdd_above: "bounded S \<Longrightarrow> bdd_above (S :: 'a::ordered_euclidean_space set)"
  by (auto intro: bdd_above_mono dest!: bounded_subset_cbox)

lemma bounded_imp_bdd_below: "bounded S \<Longrightarrow> bdd_below (S :: 'a::ordered_euclidean_space set)"
  by (auto intro: bdd_below_mono dest!: bounded_subset_cbox)

lemma bdd_above_cmult:
  "0 \<le> (a :: 'a :: ordered_semiring) \<Longrightarrow> bdd_above S \<Longrightarrow> bdd_above ((\<lambda>x. a * x) ` S)"
  by (metis bdd_above_def bdd_aboveI2 mult_left_mono)

lemma Sup_real_mult:
  fixes a::real
  assumes "0 \<le> a"
  assumes "S \<noteq> {}" "bdd_above S"
  shows "a * Sup S = Sup ((\<lambda>x. a * x) ` S)"
  using assms
proof cases
  assume "a = 0" with `S \<noteq> {}` show ?thesis
    by (simp add: cSUP_const)
next
  assume "a \<noteq> 0"
  with `0 \<le> a` have "0 < a"
    by simp
  show ?thesis
  proof (intro antisym)
    have "Sup S \<le> Sup (op * a ` S) / a" using assms
      by (intro cSup_least mult_imp_le_div_pos cSup_upper)
         (auto simp: bdd_above_cmult assms `0 < a` less_imp_le)
    thus "a * Sup S \<le> Sup (op * a ` S)"
      by (simp add: ac_simps pos_le_divide_eq[OF `0<a`])
  qed (insert assms `0 < a`, auto intro!: cSUP_least cSup_upper)
qed

subsection {* Linorder *}

context linordered_idom
begin

lemma mult_right_le_one_le:
  "0 \<le> x \<Longrightarrow> y \<le> 1 \<Longrightarrow> x * y \<le> x"
  by (auto simp add: mult_le_cancel_left2)

lemma mult_left_le_one_le:
  "0 \<le> x \<Longrightarrow> y \<le> 1 \<Longrightarrow> y * x \<le> x"
  by (auto simp add: mult_le_cancel_right2)

end

subsection {* Banach on type class *}

lemma banach_fix_type:
  fixes f::"'a::complete_space\<Rightarrow>'a"
  assumes c:"0 \<le> c" "c < 1"
      and lipschitz:"\<forall>x. \<forall>y. dist (f x) (f y) \<le> c * dist x y"
  shows "\<exists>!x. (f x = x)"
  using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
  by auto

subsection {* Float *}

definition "trunc p s =
  (let d = truncate_down p s in
  let u = truncate_up p s in
  let ed = abs (s - d) in
  let eu = abs (u - s) in
  if abs (s - d) < abs (u - s) then (d, truncate_up p ed) else (u, truncate_up p eu))"

lemma trunc_nonneg: "0 \<le> s \<Longrightarrow> 0 \<le> trunc p s"
  by (auto simp: trunc_def Let_def zero_prod_def truncate_down_def round_down_nonneg
    intro!: truncate_up_le)

definition "trunc_err p f = f - (fst (trunc p f))"

lemma trunc_err_eq:
  "fst (trunc p f) + (trunc_err p f) = f"
  by (auto simp: trunc_err_def)

lemma trunc_err_le:
  "abs (trunc_err p f) \<le> snd (trunc p f)"
  apply (auto simp: trunc_err_def trunc_def Let_def)
  apply (metis truncate_up)
  by (metis abs_minus_commute truncate_up)

lemma trunc_err_eq_zero_iff:
  "trunc_err p f = 0 \<longleftrightarrow> snd (trunc p f) = 0"
  apply (auto simp: trunc_err_def trunc_def Let_def)
  apply (metis abs_le_zero_iff eq_iff_diff_eq_0 truncate_up)
  apply (metis abs_le_zero_iff eq_iff_diff_eq_0 truncate_up)
  done

lemma mantissa_Float_0[simp]: "mantissa (Float 0 e) = 0"
  by (metis float_of_real float_zero mantissa_eq_zero_iff zero_float_def)


subsection {* Lists *}

lemma listsum_nonneg:
  assumes nn: "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<ge> (0::'a::{monoid_add, ordered_ab_semigroup_add}))"
  shows "0 \<le> listsum (map f xs)"
proof -
  have "0 = listsum (map (\<lambda>_. 0) xs)"
    by (induct xs) auto
  also have "\<dots> \<le> listsum (map f xs)"
    by (rule listsum_mono) (rule assms)
  finally show ?thesis .
qed


subsection {* Set(sum) *}

lemma setsum_eq_nonzero: "finite A \<Longrightarrow> (\<Sum>a\<in>A. f a) = (\<Sum>a\<in>{a\<in>A. f a \<noteq> 0}. f a)"
  by (subst setsum.mono_neutral_cong_right) auto

lemma singleton_subsetI:"i \<in> B \<Longrightarrow> {i} \<subseteq> B"
  by auto


subsection {* Max *}

lemma max_transfer[transfer_rule]:
  assumes [transfer_rule]: "(rel_fun A (rel_fun A (op =))) (op \<le>) (op \<le>)"
  shows "(rel_fun A (rel_fun A A)) max max"
  unfolding max_def[abs_def]
  by transfer_prover

lemma max_power2: fixes a b::real shows "(max (abs a) (abs b))\<^sup>2 = max (a\<^sup>2) (b\<^sup>2)"
  by (auto simp: max_def real_abs_le_square_iff)

end
