Theory Ordinary_Differential_Equations.Flow

section ‹Flow›
theory Flow
imports
  Picard_Lindeloef_Qualitative
  "HOL-Library.Diagonal_Subsequence"
  "../Library/Bounded_Linear_Operator"
  "../Library/Multivariate_Taylor"
  "../Library/Interval_Integral_HK"
begin

text ‹TODO: extend theorems for dependence on initial time›

subsection ‹simp rules for integrability (TODO: move)›

lemma blinfun_ext: "x = y  (i. blinfun_apply x i = blinfun_apply y i)"
  by transfer auto

notation id_blinfun ("1L")

lemma blinfun_inverse_left:
  fixes f::"'a::euclidean_space L 'a" and f'
  shows "f oL f' = 1L  f' oL f = 1L"
  by transfer
    (auto dest!: bounded_linear.linear simp: id_def[symmetric]
      linear_inverse_left)

lemma onorm_zero_blinfun[simp]: "onorm (blinfun_apply 0) = 0"
  by transfer (simp add: onorm_zero)

lemma blinfun_compose_1_left[simp]: "x oL 1L = x"
  and blinfun_compose_1_right[simp]: "1L oL y = y"
  by (auto intro!: blinfun_eqI)


named_theorems integrable_on_simps

lemma integrable_on_refl_ivl[intro, simp]: "g integrable_on {b .. (b::'b::ordered_euclidean_space)}"
  and integrable_on_refl_closed_segment[intro, simp]: "h integrable_on closed_segment a a"
  using integrable_on_refl by auto

lemma integrable_const_ivl_closed_segment[intro, simp]: "(λx. c) integrable_on closed_segment a (b::real)"
  by (auto simp: closed_segment_eq_real_ivl)

lemma integrable_ident_ivl[intro, simp]: "(λx. x) integrable_on closed_segment a (b::real)"
  and integrable_ident_cbox[intro, simp]: "(λx. x) integrable_on cbox a (b::real)"
  by (auto simp: closed_segment_eq_real_ivl ident_integrable_on)

lemma content_closed_segment_real:
  fixes a b::real
  shows "content (closed_segment a b) = abs (b - a)"
  by (auto simp: closed_segment_eq_real_ivl)

lemma integral_const_closed_segment:
  fixes a b::real
  shows "integral (closed_segment a b) (λx. c) = abs (b - a) *R c"
  by (auto simp: closed_segment_eq_real_ivl content_closed_segment_real)

lemmas [integrable_on_simps] =
  integrable_on_empty ― ‹empty›
  integrable_on_refl integrable_on_refl_ivl integrable_on_refl_closed_segment ― ‹singleton›
  integrable_const integrable_const_ivl integrable_const_ivl_closed_segment ― ‹constant›
  ident_integrable_on integrable_ident_ivl integrable_ident_cbox ― ‹identity›

lemma integrable_cmul_real:
  fixes K::real
  shows "f integrable_on X  (λx. K * f x) integrable_on X "
  unfolding real_scaleR_def[symmetric]
  by (rule integrable_cmul)

lemmas [integrable_on_simps] =
  integrable_0
  integrable_neg
  integrable_cmul
  integrable_cmul_real
  integrable_on_cmult_iff
  integrable_on_cmult_left
  integrable_on_cmult_right
  integrable_on_cmult_iff
  integrable_on_cmult_left_iff
  integrable_on_cmult_right_iff
  integrable_on_cdivide_iff
  integrable_diff
  integrable_add
  integrable_sum

lemma dist_cancel_add1: "dist (t0 + et) t0 = norm et"
  by (simp add: dist_norm)

lemma double_nonneg_le:
  fixes a::real
  shows "a * 2  b  a  0  a  b"
  by arith


subsection ‹Nonautonomous IVP on maximal existence interval›

context ll_on_open_it
begin

context
fixes x0
assumes iv_defined: "t0  T" "x0  X"
begin

lemmas closed_segment_iv_subset_domain = closed_segment_subset_domainI[OF iv_defined(1)]

lemma
  local_unique_solutions:
  obtains t u L
  where
    "0 < t" "0 < u"
    "cball t0 t  existence_ivl t0 x0"
    "cball x0 (2 * u)  X"
    "t'. t'  cball t0 t  L-lipschitz_on (cball x0 (2 * u)) (f t')"
    "x. x  cball x0 u  (flow t0 x usolves_ode f from t0) (cball t0 t) (cball x u)"
    "x. x  cball x0 u  cball x u  X"
proof -
  from local_unique_solution[OF iv_defined] obtain et ex B L
    where "0 < et" "0 < ex" "cball t0 et  T" "cball x0 ex  X"
      "unique_on_cylinder t0 (cball t0 et) x0 ex f B L"
    by metis
  then interpret cyl: unique_on_cylinder t0 "cball t0 et" x0 ex "cball x0 ex" f B L
    by auto

  from cyl.solution_solves_ode order_refl cball x0 ex  X
  have "(cyl.solution solves_ode f) (cball t0 et) X"
    by (rule solves_ode_on_subset)
  then have "cball t0 et  existence_ivl t0 x0"
    by (rule existence_ivl_maximal_interval) (insert cball t0 et  T 0 < et, auto)

  have "cball t0 et = {t0 - et .. t0 + et}"
    using et > 0 by (auto simp: dist_real_def)
  then have cylbounds[simp]: "cyl.tmin = t0 - et" "cyl.tmax = t0 + et"
    unfolding cyl.tmin_def cyl.tmax_def
    using 0 < et
    by auto

  define et' where "et'  et / 2"
  define ex' where "ex'  ex / 2"

  have "et' > 0" "ex' > 0" using 0 < et 0 < ex by (auto simp: et'_def ex'_def)
  moreover
  from cball t0 et  existence_ivl t0 x0 have "cball t0 et'  existence_ivl t0 x0"
    by (force simp: et'_def dest!: double_nonneg_le)
  moreover
  from this have "cball t0 et'  T" using existence_ivl_subset[of x0] by simp
  have  "cball x0 (2 * ex')  X" "t'. t'  cball t0 et'  L-lipschitz_on (cball x0 (2 * ex')) (f t')"
    using cyl.lipschitz 0 < et cball x0 ex  X
    by (auto simp: ex'_def et'_def intro!:)
  moreover
  {
    fix x0'::'a
    assume x0': "x0'  cball x0 ex'"
    {
      fix b
      assume d: "dist x0' b  ex'"
      have "dist x0 b  dist x0 x0' + dist x0' b"
        by (rule dist_triangle)
      also have "  ex' + ex'"
        using x0' d by simp
      also have "  ex" by (simp add: ex'_def)
      finally have "dist x0 b  ex" .
    } note triangle = this
    have subs1: "cball t0 et'  cball t0 et"
      and subs2: "cball x0' ex'  cball x0 ex"
      and subs: "cball t0 et' × cball x0' ex'  cball t0 et × cball x0 ex"
      using 0 < ex 0 < et x0'
      by (auto simp: ex'_def et'_def triangle dest!: double_nonneg_le)

    have subset_X: "cball x0' ex'  X"
      using cball x0 ex  X subs2 0 < ex' by force
    then have "x0'  X" using 0 < ex' by force
    have x0': "t0  T" "x0'  X" by fact+
    have half_intros: "a  ex'  a  ex" "a  et'  a  et"
      and halfdiv_intro: "a * 2  ex / B  a  ex' / B" for a
      using 0 < ex 0 < et
      by (auto simp: ex'_def et'_def)

    interpret cyl': solution_in_cylinder t0 "cball t0 et'" x0' ex' f "cball x0' ex'" B
      using 0 < et' 0 < ex' 0 < et cyl.norm_f cyl.continuous subs1 cball t0 et  T
      apply unfold_locales
      apply (auto simp: split_beta' dist_cancel_add1 intro!: triangle
        continuous_intros cyl.norm_f order_trans[OF _ cyl.e_bounded] halfdiv_intro)
      by (simp add: ex'_def et'_def dist_commute)

    interpret cyl': unique_on_cylinder t0 "cball t0 et'" x0' ex' "cball x0' ex'" f B L
      using cyl.lipschitz[simplified] subs subs1
      by (unfold_locales)
         (auto simp: triangle intro!: half_intros lipschitz_on_subset[OF _ subs2])
    from cyl'.solution_usolves_ode
    have "(flow t0 x0' usolves_ode f from t0) (cball t0 et') (cball x0' ex')"
      apply (rule usolves_ode_solves_odeI)
      subgoal
        apply (rule cyl'.solves_ode_on_subset_domain[where Y=X])
        subgoal
          apply (rule solves_ode_on_subset[where S="existence_ivl t0 x0'" and Y=X])
          subgoal by (rule flow_solves_ode[OF x0'])
          subgoal
            using subs2 cball x0 ex  X 0 < et' cball t0 et'  T
            by (intro existence_ivl_maximal_interval[OF solves_ode_on_subset[OF cyl'.solution_solves_ode]])
              auto
          subgoal by force
          done
        subgoal by (force simp: x0'  X iv_defined)
        subgoal using 0 < et' by force
        subgoal by force
        subgoal by force
        done
      subgoal by (force simp: x0'  X iv_defined cyl'.solution_iv)
      done
    note this subset_X
  } ultimately show thesis ..
qed

lemma Picard_iterate_mem_existence_ivlI:
  assumes "t  T"
  assumes "compact C" "x0  C" "C  X"
  assumes "y s. s  {t0 -- t}  y t0 = x0  y  {t0--s}  C  continuous_on {t0--s} y 
      x0 + ivl_integral t0 s (λt. f t (y t))  C"
  shows "t  existence_ivl t0 x0" "s. s  {t0 -- t}  flow t0 x0 s  C"
proof -
  have "{t0 -- t}  T"
    by (intro closed_segment_subset_domain iv_defined assms)
  from lipschitz_on_compact[OF compact_segment {t0 -- t}  T compact C C  X]
  obtain L where L: "s. s  {t0 -- t}  L-lipschitz_on C (f s)" by metis
  interpret uc: unique_on_closed t0 "{t0 -- t}" x0 f C L
    using assms closed_segment_iv_subset_domain
    by unfold_locales
      (auto intro!: L compact_imp_closed compact C continuous_on_f continuous_intros
        simp: split_beta)
  have "{t0 -- t}  existence_ivl t0 x0"
    using assms closed_segment_iv_subset_domain
    by (intro maximal_existence_flow[OF solves_ode_on_subset[OF uc.solution_solves_ode]])
      auto
  thus "t  existence_ivl t0 x0"
    using assms by auto
  show "flow t0 x0 s  C" if "s  {t0 -- t}" for s
  proof -
    have "flow t0 x0 s = uc.solution s" "uc.solution s  C"
      using solves_odeD[OF uc.solution_solves_ode] that assms
      by (auto simp: closed_segment_iv_subset_domain
        intro!:  maximal_existence_flowI(2)[where K="{t0 -- t}"])
    thus ?thesis by simp
  qed
qed

lemma flow_has_vderiv_on: "(flow t0 x0 has_vderiv_on (λt. f t (flow t0 x0 t))) (existence_ivl t0 x0)"
  by (rule solves_ode_vderivD[OF flow_solves_ode[OF iv_defined]])

lemmas flow_has_vderiv_on_compose[derivative_intros] =
  has_vderiv_on_compose2[OF flow_has_vderiv_on, THEN has_vderiv_on_eq_rhs]

end

lemma unique_on_intersection:
  assumes sols: "(x solves_ode f) U X" "(y solves_ode f) V X"
  assumes iv_mem: "t0  U" "t0  V" and subs: "U  T" "V  T"
  assumes ivls: "is_interval U" "is_interval V"
  assumes iv: "x t0 = y t0"
  assumes mem: "t  U" "t  V"
  shows "x t = y t"
proof -
  from
    maximal_existence_flow(2)[OF sols(1) refl          ivls(1) iv_mem(1) subs(1) mem(1)]
    maximal_existence_flow(2)[OF sols(2) iv[symmetric] ivls(2) iv_mem(2) subs(2) mem(2)]
  show ?thesis by simp
qed

lemma unique_solution:
  assumes sols: "(x solves_ode f) U X" "(y solves_ode f) U X"
  assumes iv_mem: "t0  U" and subs: "U  T"
  assumes ivls: "is_interval U"
  assumes iv: "x t0 = y t0"
  assumes mem: "t  U"
  shows "x t = y t"
  by (metis unique_on_intersection assms)

lemma
  assumes s: "s  existence_ivl t0 x0"
  assumes t: "t + s  existence_ivl s (flow t0 x0 s)"
  shows flow_trans: "flow t0 x0 (s + t) = flow s (flow t0 x0 s) (s + t)"
    and existence_ivl_trans: "s + t  existence_ivl t0 x0"
proof -
  note ll_on_open_it_axioms
  moreover
  from ll_on_open_it_axioms
  have iv_defined: "t0  T" "x0  X"
    and iv_defined': "s  T" "flow t0 x0 s  X"
    using ll_on_open_it.mem_existence_ivl_iv_defined s t
    by blast+

  have "{t0--s}  existence_ivl t0 x0"
    by (simp add: s segment_subset_existence_ivl iv_defined)

  have "s  existence_ivl s (flow t0 x0 s)"
    by (rule ll_on_open_it.existence_ivl_initial_time; fact)
  have "{s--t + s}  existence_ivl s (flow t0 x0 s)"
    by (rule ll_on_open_it.segment_subset_existence_ivl; fact)

  have unique: "flow t0 x0 u = flow s (flow t0 x0 s) u"
    if "u  {s--t + s}" "u  {t0--s}" for u
    using
      ll_on_open_it_axioms
      ll_on_open_it.flow_solves_ode[OF ll_on_open_it_axioms iv_defined]
      ll_on_open_it.flow_solves_ode[OF ll_on_open_it_axioms iv_defined']
      s
    apply (rule ll_on_open_it.unique_on_intersection)
    using s  existence_ivl s (flow t0 x0 s) existence_ivl_subset
      flow t0 x0 s  X s  T iv_defined s t ll_on_open_it.in_existence_between_zeroI
      that ll_on_open_it_axioms ll_on_open_it.mem_existence_ivl_subset
    by (auto simp: is_interval_existence_ivl)

  let ?un = "{t0 -- s}  {s -- t + s}"
  let ?if = "λt. if t  {t0 -- s} then flow t0 x0 t else flow s (flow t0 x0 s) t"
  have "(?if solves_ode (λt. if t  {t0 -- s} then f t else f t)) ?un (X  X)"
    apply (rule connection_solves_ode)
    subgoal by (rule solves_ode_on_subset[OF flow_solves_ode[OF iv_defined] {t0--s}  _ order_refl])
    subgoal
      by (rule solves_ode_on_subset[OF ll_on_open_it.flow_solves_ode[OF ll_on_open_it_axioms iv_defined']
          {s--t + s}  _ order_refl])
    subgoal by simp
    subgoal by simp
    subgoal by (rule unique) auto
    subgoal by simp
    done
  then have ifsol: "(?if solves_ode f) ?un X"
    by simp
  moreover
  have "?un  existence_ivl t0 x0"
    using existence_ivl_subset[of x0]
      ll_on_open_it.existence_ivl_subset[OF ll_on_open_it_axioms, of s "flow t0 x0 s"]
      {t0 -- s}  _ {s--t + s}  _
    by (intro existence_ivl_maximal_interval[OF ifsol]) (auto intro!: is_real_interval_union)
  then show "s + t  existence_ivl t0 x0"
    by (auto simp: ac_simps)
  have "(flow t0 x0 solves_ode f) ?un X"
    using {t0--s}  _ {s -- t + s}  _
    by (intro solves_ode_on_subset[OF flow_solves_ode ?un  _ order_refl] iv_defined)
  moreover have "s  ?un"
    by simp
  ultimately have "?if (s + t) = flow t0 x0 (s + t)"
    apply (rule ll_on_open_it.unique_solution)
    using existence_ivl_subset[of x0]
      ll_on_open_it.existence_ivl_subset[OF ll_on_open_it_axioms, of s "flow t0 x0 s"]
      {t0 -- s}  _ {s--t + s}  _
    by (auto intro!: is_real_interval_union simp: ac_simps)
  with unique[of "s + t"]
  show "flow t0 x0 (s + t) = flow s (flow t0 x0 s) (s + t)"
    by (auto split: if_splits simp: ac_simps)
qed

lemma
  assumes t: "t  existence_ivl t0 x0"
  shows flows_reverse: "flow t (flow t0 x0 t) t0 = x0"
    and existence_ivl_reverse: "t0  existence_ivl t (flow t0 x0 t)"
proof -
  have iv_defined: "t0  T" "x0  X"
    using mem_existence_ivl_iv_defined t by blast+
  show "t0  existence_ivl t (flow t0 x0 t)"
    using assms
    by (metis (no_types, opaque_lifting) closed_segment_commute closed_segment_subset_interval
        ends_in_segment(2) general.csol(2-4)
        general.existence_ivl_maximal_segment general.is_interval_existence_ivl
        is_interval_closed_segment_1 iv_defined ll_on_open_it.equals_flowI
        local.existence_ivl_initial_time local.flow_initial_time local.ll_on_open_it_axioms)
  then have "flow t (flow t0 x0 t) (t + (t0 - t)) = flow t0 x0 (t + (t0 - t))"
    by (intro flow_trans[symmetric]) (auto simp: t iv_defined)
  then show "flow t (flow t0 x0 t) t0 = x0"
    by (simp add: iv_defined)
qed

lemma flow_has_derivative:
  assumes "t  existence_ivl t0 x0"
  shows "(flow t0 x0 has_derivative (λi. i *R f t (flow t0 x0 t))) (at t)"
proof -
  have "(flow t0 x0 has_derivative (λi. i *R f t (flow t0 x0 t))) (at t within existence_ivl t0 x0)"
    using flow_has_vderiv_on
    by (auto simp: has_vderiv_on_def has_vector_derivative_def assms mem_existence_ivl_iv_defined[OF assms])
  then show ?thesis
    by (simp add: at_within_open[OF assms open_existence_ivl])
qed


lemma flow_has_vector_derivative:
  assumes "t  existence_ivl t0 x0"
  shows "(flow t0 x0 has_vector_derivative f t (flow t0 x0 t)) (at t)"
  using flow_has_derivative[OF assms]
  by (simp add: has_vector_derivative_def)

lemma flow_has_vector_derivative_at_0:
  assumes"t  existence_ivl t0 x0"
  shows "((λh. flow t0 x0 (t + h)) has_vector_derivative f t (flow t0 x0 t)) (at 0)"
proof -
  from flow_has_vector_derivative[OF assms]
  have
    "((+) t has_vector_derivative 1) (at 0)"
    "(flow t0 x0 has_vector_derivative f t (flow t0 x0 t)) (at (t + 0))"
    by (auto intro!: derivative_eq_intros)
  from vector_diff_chain_at[OF this]
  show ?thesis by (simp add: o_def)
qed

lemma
  assumes "t  existence_ivl t0 x0"
  shows closed_segment_subset_existence_ivl: "closed_segment t0 t  existence_ivl t0 x0"
    and ivl_subset_existence_ivl: "{t0 .. t}  existence_ivl t0 x0"
    and ivl_subset_existence_ivl': "{t .. t0}  existence_ivl t0 x0"
  using assms in_existence_between_zeroI
  by (auto simp: closed_segment_eq_real_ivl)

lemma flow_fixed_point:
  assumes t: "t  existence_ivl t0 x0"
  shows "flow t0 x0 t = x0 + ivl_integral t0 t (λt. f t (flow t0 x0 t))"
proof -
  have "(flow t0 x0 has_vderiv_on (λs. f s (flow t0 x0 s))) {t0 -- t}"
    using closed_segment_subset_existence_ivl[OF t]
    by (auto intro!: has_vector_derivative_at_within flow_has_vector_derivative
      simp: has_vderiv_on_def)
  from fundamental_theorem_of_calculus_ivl_integral[OF this]
  have "((λt. f t (flow t0 x0 t)) has_ivl_integral flow t0 x0 t - x0) t0 t"
    by (simp add: mem_existence_ivl_iv_defined[OF assms])
  from this[THEN ivl_integral_unique]
  show ?thesis by simp
qed

lemma flow_continuous: "t  existence_ivl t0 x0  continuous (at t) (flow t0 x0)"
  by (metis has_derivative_continuous flow_has_derivative)

lemma flow_tendsto: "t  existence_ivl t0 x0  (ts  t) F 
    ((λs. flow t0 x0 (ts s))  flow t0 x0 t) F"
  by (rule isCont_tendsto_compose[OF flow_continuous])

lemma flow_continuous_on: "continuous_on (existence_ivl t0 x0) (flow t0 x0)"
  by (auto intro!: flow_continuous continuous_at_imp_continuous_on)

lemma flow_continuous_on_intro:
  "continuous_on s g 
  (xa. xa  s  g xa  existence_ivl t0 x0) 
  continuous_on s (λxa. flow t0 x0 (g xa))"
  by (auto intro!: continuous_on_compose2[OF flow_continuous_on])

lemma f_flow_continuous:
  assumes "t  existence_ivl t0 x0"
  shows "isCont (λt. f t (flow t0 x0 t)) t"
  by (rule continuous_on_interior)
    (insert existence_ivl_subset assms,
      auto intro!: flow_in_domain flow_continuous_on continuous_intros
        simp: interior_open open_existence_ivl)

lemma exponential_initial_condition:
  assumes y0: "t  existence_ivl t0 y0"
  assumes z0: "t  existence_ivl t0 z0"
  assumes "Y  X"
  assumes remain: "s. s  closed_segment t0 t  flow t0 y0 s  Y"
    "s. s  closed_segment t0 t  flow t0 z0 s  Y"
  assumes lipschitz: "s. s  closed_segment t0 t  K-lipschitz_on Y (f s)"
  shows "norm (flow t0 y0 t - flow t0 z0 t)  norm (y0 - z0) * exp ((K + 1) * abs (t - t0))"
proof cases
  assume "y0 = z0"
  thus ?thesis
    by simp
next
  assume ne: "y0  z0"
  define K' where "K'  K + 1"
  from lipschitz have "K'-lipschitz_on Y (f s)" if "s  {t0 -- t}" for s
    using that
    by (auto simp: lipschitz_on_def K'_def
      intro!: order_trans[OF _ mult_right_mono[of K "K + 1"]])

  from mem_existence_ivl_iv_defined[OF y0] mem_existence_ivl_iv_defined[OF z0]
  have "t0  T" and inX: "y0  X" "z0  X" by auto

  from remain[of t0] inX t0  T have "y0  Y" "z0  Y" by auto

  define v where "v  λt. norm (flow t0 y0 t - flow t0 z0 t)"
  {
    fix s
    assume s: "s  {t0 -- t}"
    with s
      closed_segment_subset_existence_ivl[OF y0]
      closed_segment_subset_existence_ivl[OF z0]
    have
      y0': "s  existence_ivl t0 y0" and
      z0': "s  existence_ivl t0 z0"
      by (auto simp: closed_segment_eq_real_ivl)
    have integrable:
      "(λt. f t (flow t0 y0 t)) integrable_on {t0--s}"
      "(λt. f t (flow t0 z0 t)) integrable_on {t0--s}"
      using closed_segment_subset_existence_ivl[OF y0']
        closed_segment_subset_existence_ivl[OF z0']
        y0  X z0  X t0  T
      by (auto intro!: continuous_at_imp_continuous_on f_flow_continuous
        integrable_continuous_closed_segment)
    hence int: "flow t0 y0 s - flow t0 z0 s =
        y0 - z0 + ivl_integral t0 s (λt. f t (flow t0 y0 t) - f t (flow t0 z0 t))"
      unfolding v_def
      using flow_fixed_point[OF y0'] flow_fixed_point[OF z0']
        s
      by (auto simp: algebra_simps ivl_integral_diff)
    have "v s  v t0 + K' *  integral {t0 -- s} (λt. v t)"
      using closed_segment_subset_existence_ivl[OF y0'] closed_segment_subset_existence_ivl[OF z0'] s
        using closed_segment_closed_segment_subset[OF _ _ s, of _ t0, simplified]
      by (subst integral_mult)
        (auto simp: integral_mult v_def int inX t0  T
          simp del: Henstock_Kurzweil_Integration.integral_mult_right
          intro!: norm_triangle_le ivl_integral_norm_bound_integral
            integrable_continuous_closed_segment continuous_intros
            continuous_at_imp_continuous_on flow_continuous f_flow_continuous
            lipschitz_on_normD[OF _  K'-lipschitz_on _ _] remain)
  } note le = this
  have cont: "continuous_on {t0 -- t} v"
    using closed_segment_subset_existence_ivl[OF y0] closed_segment_subset_existence_ivl[OF z0] inX
    by (auto simp: v_def t0  T
      intro!: continuous_at_imp_continuous_on continuous_intros flow_continuous)
  have nonneg: "t. v t  0"
    by (auto simp: v_def)
  from ne have pos: "v t0 > 0"
    by (auto simp: v_def t0  T inX)
  have lippos: "K' > 0"
  proof -
    have "0  dist (f t0 y0) (f t0 z0)" by simp
    also from lipschitz_onD[OF lipschitz y0  Y z0  Y, of t0]ne
    have "  K * dist y0 z0"
      by simp
    finally have "0  K"
      by (metis dist_le_zero_iff ne zero_le_mult_iff)
    thus ?thesis by (simp add: K'_def)
  qed
  from le cont nonneg pos 0 < K'
  have "v t  v t0 * exp (K' * abs (t - t0))"
    by (rule gronwall_general_segment) simp_all
  thus ?thesis
    by (simp add: v_def K'_def t0  T inX)
qed

lemma
  existence_ivl_cballs:
  assumes iv_defined: "t0  T" "x0  X"
  obtains t u L
  where
    "y. y  cball x0 u  cball t0 t  existence_ivl t0 y"
    "s y. y  cball x0 u  s  cball t0 t  flow t0 y s  cball y u"
    "L-lipschitz_on (cball t0 t×cball x0 u) (λ(t, x). flow t0 x t)"
    "y. y  cball x0 u  cball y u  X"
    "0 < t" "0 < u"
proof -
  note iv_defined
  from local_unique_solutions[OF this]
  obtain t u L where tu: "0 < t" "0 < u"
    and subsT: "cball t0 t  existence_ivl t0 x0"
    and subs': "cball x0 (2 * u)  X"
    and lipschitz: "s. s  cball t0 t  L-lipschitz_on (cball x0 (2*u)) (f s)"
    and usol: "y. y  cball x0 u  (flow t0 y usolves_ode f from t0) (cball t0 t) (cball y u)"
    and subs: "y. y  cball x0 u  cball y u  X"
    by metis
  {
    fix y assume y: "y  cball x0 u"
    from subs[OF y] 0 < u have "y  X" by auto
    note iv' = t0  T y  X
    from usol[OF y, THEN usolves_odeD(1)]
    have sol1: "(flow t0 y solves_ode f) (cball t0 t) (cball y u)" .
    from sol1 order_refl subs[OF y]
    have sol: "(flow t0 y solves_ode f) (cball t0 t) X"
      by (rule solves_ode_on_subset)
    note * = maximal_existence_flow[OF sol flow_initial_time
        is_interval_cball_1 _ order_trans[OF subsT existence_ivl_subset],
        unfolded centre_in_cball, OF iv' less_imp_le[OF 0 < t]]
    have eivl: "cball t0 t  existence_ivl t0 y"
      by (rule *)
    have "flow t0 y s  cball y u" if "s  cball t0 t" for s
      by (rule solves_odeD(2)[OF sol1 that])
    note eivl this
  } note * = this
  note *
  moreover
  have cont_on_f_flow:
    "x1 S. S  cball t0 t  x1  cball x0 u  continuous_on S (λt. f t (flow t0 x1 t))"
    using subs[of x0] u > 0 *(1) iv_defined
    by (auto intro!: continuous_at_imp_continuous_on f_flow_continuous)
  have "bounded ((λ(t, x). f t x) ` (cball t0 t × cball x0 (2 * u)))"
    using subs' subsT existence_ivl_subset[of x0]
    by (auto intro!: compact_imp_bounded compact_continuous_image compact_Times
      continuous_intros simp: split_beta')
  then obtain B where B: "s y. s  cball t0 t  y  cball x0 (2 * u)  norm (f s y)  B" "B > 0"
    by (auto simp: bounded_pos cball_def)
  have flow_in_cball: "flow t0 x1 s  cball x0 (2 * u)"
    if s: "s  cball t0 t" and x1: "x1  cball x0 u"
    for s::real and x1
  proof -
    from *(2)[OF x1 s] have "flow t0 x1 s  cball x1 u" .
    also have "  cball x0 (2 * u)"
      using x1
      by (auto intro!: dist_triangle_le[OF add_mono, of _ x1 u _ u, simplified]
        simp: dist_commute)
    finally show ?thesis .
  qed
  have "(B + exp ((L + 1) * ¦t¦))-lipschitz_on (cball t0 t×cball x0 u) (λ(t, x). flow t0 x t)"
  proof (rule lipschitz_onI, safe)
    fix t1 t2 :: real and x1 x2
    assume t1: "t1  cball t0 t" and t2: "t2  cball t0 t"
      and x1: "x1  cball x0 u" and x2: "x2  cball x0 u"
    have t1_ex: "t1  existence_ivl t0 x1"
      and t2_ex: "t2  existence_ivl t0 x1" "t2  existence_ivl t0 x2"
      and "x1  cball x0 (2*u)" "x2  cball x0 (2*u)"
      using *(1)[OF x1] *(1)[OF x2] t1 t2 x1 x2 tu by auto
    have "dist (flow t0 x1 t1) (flow t0 x2 t2) 
      dist (flow t0 x1 t1) (flow t0 x1 t2) + dist (flow t0 x1 t2) (flow t0 x2 t2)"
      by (rule dist_triangle)
    also have "dist (flow t0 x1 t2) (flow t0 x2 t2)  dist x1 x2 * exp ((L + 1) * ¦t2 - t0¦)"
      unfolding dist_norm
    proof (rule exponential_initial_condition[where Y = "cball x0 (2 * u)"])
      fix s assume "s  closed_segment t0 t2" hence s: "s  cball t0 t"
        using t2
        by (auto simp: dist_real_def closed_segment_eq_real_ivl split: if_split_asm)
      show "flow t0 x1 s  cball x0 (2 * u)"
        by (rule flow_in_cball[OF s x1])
      show "flow t0 x2 s  cball x0 (2 * u)"
        by (rule flow_in_cball[OF s x2])
      show "L-lipschitz_on (cball x0 (2 * u)) (f s)" if "s  closed_segment t0 t2" for s
        using that centre_in_cball convex_contains_segment less_imp_le t2 tu(1)
        by (blast intro!: lipschitz)
    qed (fact)+
    also have "  dist x1 x2 * exp ((L + 1) * ¦t¦)"
      using u > 0 t2
      by (auto
        intro!: mult_left_mono add_nonneg_nonneg lipschitz[THEN lipschitz_on_nonneg]
        simp: cball_eq_empty cball_eq_sing' dist_real_def)
    also
    have "x1  X"
      using x1 subs[of x0] u > 0
      by auto
    have *: "¦t0 - t1¦  t  x  {t0--t1}  ¦t0 - x¦  t"
      "¦t0 - t2¦  t  x  {t0--t2}  ¦t0 - x¦  t"
      "¦t0 - t1¦  t  ¦t0 - t2¦  t  x  {t1--t2}  ¦t0 - x¦  t"
      for x
      using t1 t2 t1_ex x1 flow_in_cball[OF _ x1]
      by (auto simp: closed_segment_eq_real_ivl split: if_splits)

    have integrable:
      "(λt. f t (flow t0 x1 t)) integrable_on {t0--t1}"
      "(λt. f t (flow t0 x1 t)) integrable_on {t0--t2}"
      "(λt. f t (flow t0 x1 t)) integrable_on {t1--t2}"
      using t1 t2 t1_ex x1 flow_in_cball[OF _ x1]
      by (auto intro!: order_trans[OF integral_bound[where B=B]] cont_on_f_flow B
        integrable_continuous_closed_segment
        intro: *
        simp: dist_real_def integral_minus_sets')

    have *: "¦t0 - t1¦  t  ¦t0 - t2¦  t  s  {t1--t2}  ¦t0 - s¦  t" for s
      by (auto simp: closed_segment_eq_real_ivl split: if_splits)
    note [simp] = t1_ex t2_ex x1  X integrable
    have "dist (flow t0 x1 t1) (flow t0 x1 t2)  dist t1 t2 * B"
      using t1 t2 x1 flow_in_cball[OF _ x1] t0  T
        ivl_integral_combine[of "λt. f t (flow t0 x1 t)" t2 t0 t1]
        ivl_integral_combine[of "λt. f t (flow t0 x1 t)" t1 t0 t2]
      by (auto simp: flow_fixed_point dist_norm add.commute closed_segment_commute
          norm_minus_commute ivl_integral_minus_sets' ivl_integral_minus_sets
        intro!: order_trans[OF ivl_integral_bound[where B=B]] cont_on_f_flow B dest: *)
    finally
    have "dist (flow t0 x1 t1) (flow t0 x2 t2) 
        dist t1 t2 * B + dist x1 x2 * exp ((L + 1) * ¦t¦)"
      by arith
    also have "  dist (t1, x1) (t2, x2) * B + dist (t1, x1) (t2, x2) * exp ((L + 1) * ¦t¦)"
      using B > 0
      by (auto intro!: add_mono mult_right_mono simp: dist_prod_def)
    finally show "dist (flow t0 x1 t1) (flow t0 x2 t2)
        (B + exp ((L + 1) * ¦t¦)) * dist (t1, x1) (t2, x2)"
      by (simp add: algebra_simps)
  qed (simp add: 0 < B less_imp_le)
  ultimately
  show thesis using subs tu ..
qed

context
fixes x0
assumes iv_defined: "t0  T" "x0  X"
begin

lemma existence_ivl_notempty: "existence_ivl t0 x0  {}"
  using existence_ivl_initial_time iv_defined
  by auto

lemma initial_time_bounds:
  shows "bdd_above (existence_ivl t0 x0)  t0 < Sup (existence_ivl t0 x0)" (is "?a  _")
    and "bdd_below (existence_ivl t0 x0)  Inf (existence_ivl t0 x0) < t0" (is "?b  _")
proof -
  from local_unique_solutions[OF iv_defined]
  obtain te where te: "te > 0" "cball t0 te  existence_ivl t0 x0"
    by metis
  then
  show "t0 < Sup (existence_ivl t0 x0)" if bdd: "bdd_above (existence_ivl t0 x0)"
    using less_cSup_iff[OF existence_ivl_notempty bdd, of t0] iv_defined
    by (auto simp: dist_real_def intro!: bexI[where x="t0 + te"])

  from te show "Inf (existence_ivl t0 x0) < t0" if bdd: "bdd_below (existence_ivl t0 x0)"
    unfolding cInf_less_iff[OF existence_ivl_notempty bdd, of t0]
    by (auto simp: dist_real_def iv_defined intro!: bexI[where x="t0 - te"])
qed

lemma
  flow_leaves_compact_ivl_right:
  assumes bdd: "bdd_above (existence_ivl t0 x0)"
  defines "b  Sup (existence_ivl t0 x0)"
  assumes "b  T"
  assumes "compact K"
  assumes "K  X"
  obtains t where "t  t0" "t  existence_ivl t0 x0" "flow t0 x0 t  K"
proof (atomize_elim, rule ccontr, auto)
  note iv_defined
  note ne = existence_ivl_notempty
  assume K[rule_format]: "t. t  existence_ivl t0 x0  t0  t  flow t0 x0 t  K"
  have b_upper: "t  b" if "t  existence_ivl t0 x0" for t
    unfolding b_def
    by (rule cSup_upper[OF that bdd])

  have less_b_iff: "y < b  (xexistence_ivl t0 x0. y < x)" for y
    unfolding b_def less_cSup_iff[OF ne bdd] ..
  have "t0  b"
    by (simp add: iv_defined b_upper)
  then have geI: "t  {t0--<b}  t0  t" for t
    by (auto simp: half_open_segment_real)
  have subset: "{t0 --< b}  existence_ivl t0 x0"
    using t0  b in_existence_between_zeroI
    by (auto simp: half_open_segment_real iv_defined less_b_iff)
  have sol: "(flow t0 x0 solves_ode f) {t0 --< b} K"
    apply (rule solves_odeI)
    apply (rule has_vderiv_on_subset[OF solves_odeD(1)[OF flow_solves_ode] subset])
    using subset iv_defined
    by (auto intro!: K geI)
  have cont: "continuous_on ({t0--b} × K) (λ(t, x). f t x)"
    using K  X closed_segment_subset_domainI[OF iv_defined(1) b  T]
    by (auto simp: split_beta intro!: continuous_intros)

  from initial_time_bounds(1)[OF bdd] have "t0  b" by (simp add: b_def)
  from solves_ode_half_open_segment_continuation[OF sol cont compact K t0  b]
  obtain l where lim: "(flow t0 x0  l) (at b within {t0--<b})"
    and limsol: "((λt. if t = b then l else flow t0 x0 t) solves_ode f) {t0--b} K" .
  have "b  existence_ivl t0 x0"
    using t0  b closed_segment_subset_domainI[OF t0  T b  T]
    by (intro existence_ivl_maximal_segment[OF solves_ode_on_subset[OF limsol order_refl K  X]])
      (auto simp: iv_defined)

  have "flow t0 x0 b  X"
    by (simp add: b  existence_ivl t0 x0 flow_in_domain iv_defined)

  from ll_on_open_it.local_unique_solutions[OF ll_on_open_it_axioms b  T flow t0 x0 b  X]
  obtain e where "e > 0" "cball b e  existence_ivl b (flow t0 x0 b)"
    by metis
  then have "e + b  existence_ivl b (flow t0 x0 b)"
    by (auto simp: dist_real_def)
  from existence_ivl_trans[OF b  existence_ivl t0 x0 e + b  existence_ivl _ _]
  have "b + e  existence_ivl t0 x0" .
  from b_upper[OF this] e > 0
  show False
    by simp
qed

lemma
  flow_leaves_compact_ivl_left:
  assumes bdd: "bdd_below (existence_ivl t0 x0)"
  defines "b  Inf (existence_ivl t0 x0)"
  assumes "b  T"
  assumes "compact K"
  assumes "K  X"
  obtains t where "t  t0" "t  existence_ivl t0 x0" "flow t0 x0 t  K"
proof -
  interpret rev: ll_on_open "(preflect t0 ` T)" "(λt. - f (preflect t0 t))" X ..
  from antimono_preflect bdd have bdd_rev: "bdd_above (rev.existence_ivl t0 x0)"
    unfolding rev_existence_ivl_eq
    by (rule bdd_above_image_antimono)
  note ne = existence_ivl_notempty
  have "Sup (rev.existence_ivl t0 x0) = preflect t0 b"
    using continuous_at_Inf_antimono[OF antimono_preflect _ ne bdd]
    by (simp add: continuous_preflect b_def rev_existence_ivl_eq)
  then have Sup_mem: "Sup (rev.existence_ivl t0 x0)  preflect t0 ` T"
    using b  T by auto

  have rev_iv: "t0  preflect t0 ` T" "x0  X" using iv_defined by auto
  from rev.flow_leaves_compact_ivl_right[OF rev_iv bdd_rev Sup_mem compact K K  X]
  obtain t where "t0  t" "t  rev.existence_ivl t0 x0" "rev.flow t0 x0 t  K" .

  then have "preflect t0 t  t0" "preflect t0 t  existence_ivl t0 x0" "flow t0 x0 (preflect t0 t)  K"
    by (auto simp: rev_existence_ivl_eq rev_flow_eq)
  thus ?thesis ..
qed

lemma
  sup_existence_maximal:
  assumes "t. t0  t  t  existence_ivl t0 x0  flow t0 x0 t  K"
  assumes "compact K" "K  X"
  assumes "bdd_above (existence_ivl t0 x0)"
  shows "Sup (existence_ivl t0 x0)  T"
  using flow_leaves_compact_ivl_right[of K] assms by force

lemma
  inf_existence_minimal:
  assumes "t. t  t0  t  existence_ivl t0 x0  flow t0 x0 t  K"
  assumes "compact K" "K  X"
  assumes "bdd_below (existence_ivl t0 x0)"
  shows "Inf (existence_ivl t0 x0)  T"
  using flow_leaves_compact_ivl_left[of K] assms
  by force

end

lemma
  subset_mem_compact_implies_subset_existence_interval:
  assumes ivl: "t0  T'" "is_interval T'" "T'  T"
  assumes iv_defined: "x0  X"
  assumes mem_compact: "t. t  T'  t  existence_ivl t0 x0  flow t0 x0 t  K"
  assumes K: "compact K" "K  X"
  shows "T'  existence_ivl t0 x0"
proof (rule ccontr)
  assume "¬ T'  existence_ivl t0 x0"
  then obtain t' where t': "t'  existence_ivl t0 x0" "t'  T'"
    by auto
  from assms have iv_defined: "t0  T" "x0  X" by auto
  show False
  proof (cases rule: not_in_connected_cases[OF connected_existence_ivl t'(1) existence_ivl_notempty[OF iv_defined]])
    assume bdd: "bdd_below (existence_ivl t0 x0)"
    assume t'_lower: "t'  y" if "y  existence_ivl t0 x0" for y
    have i: "Inf (existence_ivl t0 x0)  T'"
      using initial_time_bounds[OF iv_defined] iv_defined
      apply -
      by (rule mem_is_intervalI[of _ t' t0])
        (auto simp: ivl t' bdd intro!: t'_lower cInf_greatest[OF existence_ivl_notempty[OF iv_defined]])
    have *: "t  T'" if "t  t0" "t  existence_ivl t0 x0" for t
      by (rule mem_is_intervalI[OF is_interval T' i t0  T']) (auto intro!: cInf_lower that bdd)
    from inf_existence_minimal[OF iv_defined mem_compact K bdd, OF *]
    show False using i ivl by auto
  next
    assume bdd: "bdd_above (existence_ivl t0 x0)"
    assume t'_upper: "y  t'" if "y  existence_ivl t0 x0" for y
    have s: "Sup (existence_ivl t0 x0)  T'"
      using initial_time_bounds[OF iv_defined]
      apply -
      apply (rule mem_is_intervalI[of _ t0 t'])
      by (auto simp: ivl t' bdd intro!: t'_upper cSup_least[OF existence_ivl_notempty[OF iv_defined]])
    have *: "t  T'" if "t0  t" "t  existence_ivl t0 x0" for t
      by (rule mem_is_intervalI[OF is_interval T' t0  T' s]) (auto intro!: cSup_upper that bdd)
    from sup_existence_maximal[OF iv_defined mem_compact K bdd, OF *]
    show False using s ivl by auto
  qed
qed

lemma
  mem_compact_implies_subset_existence_interval:
  assumes iv_defined: "t0  T" "x0  X"
  assumes mem_compact: "t. t  T  t  existence_ivl t0 x0  flow t0 x0 t  K"
  assumes K: "compact K" "K  X"
  shows "T  existence_ivl t0 x0"
  by (rule subset_mem_compact_implies_subset_existence_interval; (fact | rule order_refl interval iv_defined))

lemma
  global_right_existence_ivl_explicit:
  assumes "b  t0"
  assumes b: "b  existence_ivl t0 x0"
  obtains d K where "d > 0" "K > 0"
    "ball x0 d  X"
    "y. y  ball x0 d  b  existence_ivl t0 y"
    "t y. y  ball x0 d  t  {t0 .. b} 
      dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * abs (t - t0))"
proof -
  note iv_defined = mem_existence_ivl_iv_defined[OF b]
  define seg where "seg  (λt. flow t0 x0 t) ` (closed_segment t0 b)"
  have [simp]: "x0  seg"
    by (auto simp: seg_def intro!: image_eqI[where x=t0] simp: closed_segment_eq_real_ivl iv_defined)
  have "seg  {}" by (auto simp: seg_def closed_segment_eq_real_ivl)
  moreover
  have "compact seg"
    using iv_defined b
    by (auto simp: seg_def closed_segment_eq_real_ivl
        intro!: compact_continuous_image continuous_at_imp_continuous_on flow_continuous;
      metis (erased, opaque_lifting) atLeastAtMost_iff closed_segment_eq_real_ivl
        closed_segment_subset_existence_ivl contra_subsetD order.trans)
  moreover note open_domain(2)
  moreover have "seg  X"
    using closed_segment_subset_existence_ivl b
    by (auto simp: seg_def intro!: flow_in_domain iv_defined)
  ultimately
  obtain e where e: "0 < e" "{x. infdist x seg  e}  X"
    thm compact_in_open_separated
    by (rule compact_in_open_separated)
  define A where "A  {x. infdist x seg  e}"

  have "A  X" using e by (simp add: A_def)

  have mem_existence_ivlI: "s. t0  s  s  b  s  existence_ivl t0 x0"
    by (rule in_existence_between_zeroI[OF b]) (auto simp: closed_segment_eq_real_ivl)

  have "compact A"
    unfolding A_def
    by (rule compact_infdist_le) fact+
  have "compact {t0 .. b}" "{t0 .. b}  T"
    subgoal by simp
    subgoal
      using mem_existence_ivlI mem_existence_ivl_subset[of _ x0] iv_defined b ivl_subset_existence_ivl
      by blast
    done
  from lipschitz_on_compact[OF this compact A A  X]
  obtain K' where K': "t. t  {t0 .. b}  K'-lipschitz_on A (f t)"
    by metis
  define K where "K  K' + 1"
  have "0 < K" "0  K"
    using assms lipschitz_on_nonneg[OF K', of t0]
    by (auto simp: K_def)
  have K: "t. t  {t0 .. b}  K-lipschitz_on A (f t)"
    unfolding K_def
    using _  lipschitz_on K' A _
    by (rule lipschitz_on_mono) auto

  have [simp]: "x0  A" using 0 < e by (auto simp: A_def)


  define d where "d  min e (e * exp (-K * (b - t0)))"
  hence d: "0 < d" "d  e" "d  e * exp (-K * (b - t0))"
    using e by auto

  have d_times_exp_le: "d * exp (K * (t - t0))  e" if "t0  t" "t  b" for t
  proof -
    from that have "d * exp (K * (t - t0))  d * exp (K * (b - t0))"
      using 0  K 0 < d
      by (auto intro!: mult_left_mono)
    also have "d * exp (K * (b - t0))  e"
      using d by (auto simp: exp_minus divide_simps)
    finally show ?thesis .
  qed
  have "ball x0 d  X" using d A  X
    by (auto simp: A_def dist_commute intro!: infdist_le2[where a=x0])
  note iv_defined
  {
    fix y
    assume y: "y  ball x0 d"
    hence "y  A" using d
      by (auto simp: A_def dist_commute intro!: infdist_le2[where a=x0])
    hence "y  X" using A  X by auto
    note y_iv = t0  T y  X
    have in_A: "flow t0 y t  A" if t: "t0  t" "t  existence_ivl t0 y" "t  b" for t
    proof (rule ccontr)
      assume flow_out: "flow t0 y t  A"
      obtain t' where t':
        "t0  t'"
        "t'  t"
        "t. t  {t0 .. t'}  flow t0 x0 t  A"
        "infdist (flow t0 y t') seg  e"
        "t. t  {t0 .. t'}  flow t0 y t  A"
      proof -
        let ?out = "((λt. infdist (flow t0 y t) seg) -` {e..})  {t0..t}"
        have "compact ?out"
          unfolding compact_eq_bounded_closed
        proof safe
          show "bounded ?out" by (auto intro!: bounded_closed_interval)
          have "continuous_on {t0 .. t} ((λt. infdist (flow t0 y t) seg))"
            using closed_segment_subset_existence_ivl t iv_defined
            by (force intro!: continuous_at_imp_continuous_on
              continuous_intros flow_continuous
              simp: closed_segment_eq_real_ivl)
          thus "closed ?out"
            by (simp add: continuous_on_closed_vimage)
        qed
        moreover
        have "t  (λt. infdist (flow t0 y t) seg) -` {e..}  {t0..t}"
          using flow_out t0  t
          by (auto simp: A_def)
        hence "?out  {}"
          by blast
        ultimately have "s?out. t?out. s  t"
          by (rule compact_attains_inf)
        then obtain t' where t':
          "s. e  infdist (flow t0 y s) seg  t0  s  s  t  t'  s"
          "e  infdist (flow t0 y t') seg"
          "t0  t'" "t'  t"
          by (auto simp: vimage_def Ball_def) metis
        have flow_in: "flow t0 x0 s  A" if s: "s  {t0 .. t'}" for s
        proof -
          from s have "s  closed_segment t0 b"
            using t  b t' by (auto simp: closed_segment_eq_real_ivl)
          then show ?thesis
            using s e > 0 by (auto simp: seg_def A_def)
        qed
        have "flow t0 y t'  A" if "t' = t0"
          using y d iv_defined that
          by (auto simp:  A_def y  X infdist_le2[where a=x0] dist_commute)
        moreover
        have "flow t0 y s  A" if s: "s  {t0 ..< t'}" for s
        proof -
          from s have "s  closed_segment t0 b"
            using t  b t' by (auto simp: closed_segment_eq_real_ivl)
          from t'(1)[of s]
          have "t' > s  t0  s  s  t  e > infdist (flow t0 y s) seg"
            by force
          then show ?thesis
            using s t' e > 0 by (auto simp: seg_def A_def)
        qed
        moreover
        note left_of_in = this
        have "closed A" using compact A by (auto simp: compact_eq_bounded_closed)
        have "((λs. flow t0 y s)  flow t0 y t') (at_left t')"
          using closed_segment_subset_existence_ivl[OF t(2)] t' y  X iv_defined
          by (intro flow_tendsto) (auto intro!: tendsto_intros simp: closed_segment_eq_real_ivl)
        with closed A _ _ have "t'  t0  flow t0 y t'  A"
        proof (rule Lim_in_closed_set)
          assume "t'  t0"
          hence "t' > t0" using t' by auto
          hence "eventually (λx. x  t0) (at_left t')"
            by (metis eventually_at_left less_imp_le)
          thus "eventually (λx. flow t0 y x  A) (at_left t')"
            unfolding eventually_at_filter
            by eventually_elim (auto intro!: left_of_in)
        qed simp
        ultimately have flow_y_in: "s  {t0 .. t'}  flow t0 y s  A" for s
          by (cases "s = t'"; fastforce)
        have
          "t0  t'"
          "t'  t"
          "t. t  {t0 .. t'}  flow t0 x0 t  A"
          "infdist (flow t0 y t') seg  e"
          "t. t  {t0 .. t'}  flow t0 y t  A"
          by (auto intro!: flow_in flow_y_in) fact+
        thus ?thesis ..
      qed
      {
        fix s assume s: "s  {t0 .. t'}"
        hence "t0  s" by simp
        have "s  b"
          using t t' s b
          by auto
        hence sx0: "s  existence_ivl t0 x0"
          by (simp add: t0  s mem_existence_ivlI)
        have sy: "s  existence_ivl t0 y"
          by (meson atLeastAtMost_iff contra_subsetD s t'(1) t'(2) that(2) ivl_subset_existence_ivl)
        have int: "flow t0 y s - flow t0 x0 s =
            y - x0 + (integral {t0 .. s} (λt. f t (flow t0 y t)) -
              integral {t0 .. s} (λt. f t (flow t0 x0 t)))"
          using iv_defined s
          unfolding flow_fixed_point[OF sx0] flow_fixed_point[OF sy]
          by (simp add: algebra_simps ivl_integral_def)
        have "norm (flow t0 y s - flow t0 x0 s)  norm (y - x0) +
          norm (integral {t0 .. s} (λt. f t (flow t0 y t)) -
            integral {t0 .. s} (λt. f t (flow t0 x0 t)))"
          unfolding int
          by (rule norm_triangle_ineq)
        also
        have "norm (integral {t0 .. s} (λt. f t (flow t0 y t)) -
            integral {t0 .. s} (λt. f t (flow t0 x0 t))) =
          norm (integral {t0 .. s} (λt. f t (flow t0 y t) - f t (flow t0 x0 t)))"
          using closed_segment_subset_existence_ivl[of s x0] sx0 closed_segment_subset_existence_ivl[of s y] sy
          by (subst Henstock_Kurzweil_Integration.integral_diff)
            (auto intro!: integrable_continuous_real continuous_at_imp_continuous_on
              f_flow_continuous
              simp: closed_segment_eq_real_ivl)
        also have "  (integral {t0 .. s} (λt. norm (f t (flow t0 y t) - f t (flow t0 x0 t))))"
          using closed_segment_subset_existence_ivl[of s x0] sx0 closed_segment_subset_existence_ivl[of s y] sy
          by (intro integral_norm_bound_integral)
            (auto intro!: integrable_continuous_real continuous_at_imp_continuous_on
            f_flow_continuous continuous_intros
              simp: closed_segment_eq_real_ivl)
      also have "  (integral {t0 .. s} (λt. K * norm ((flow t0 y t) - (flow t0 x0 t))))"
          using closed_segment_subset_existence_ivl[of s x0] sx0 closed_segment_subset_existence_ivl[of s y] sy
            iv_defined s t'(3,5) s  b
          by (auto simp del: Henstock_Kurzweil_Integration.integral_mult_right intro!: integral_le integrable_continuous_real
            continuous_at_imp_continuous_on lipschitz_on_normD[OF K]
            flow_continuous f_flow_continuous continuous_intros
            simp: closed_segment_eq_real_ivl)
        also have " = K * integral {t0 .. s} (λt. norm (flow t0 y t - flow t0 x0 t))"
          using closed_segment_subset_existence_ivl[of s x0] sx0 closed_segment_subset_existence_ivl[of s y] sy
          by (subst integral_mult)
             (auto intro!: integrable_continuous_real continuous_at_imp_continuous_on
               lipschitz_on_normD[OF K] flow_continuous f_flow_continuous continuous_intros
               simp: closed_segment_eq_real_ivl)
        finally
        have norm: "norm (flow t0 y s - flow t0 x0 s) 
          norm (y - x0) + K * integral {t0 .. s} (λt. norm (flow t0 y t - flow t0 x0 t))"
          by arith
        note norm s  b sx0 sy
      } note norm_le = this
      from norm_le(2) t' have "t'  closed_segment t0 b"
        by (auto simp: closed_segment_eq_real_ivl)
      hence "infdist (flow t0 y t') seg  dist (flow t0 y t') (flow t0 x0 t')"
        by (auto simp: seg_def infdist_le)
      also have "  norm (flow t0 y t' - flow t0 x0 t')"
        by (simp add: dist_norm)
      also have "  norm (y - x0) * exp (K * ¦t' - t0¦)"
        unfolding K_def
        apply (rule exponential_initial_condition[OF _ _ _ _ _ K'])
        subgoal by (metis atLeastAtMost_iff local.norm_le(4) order_refl t'(1))
        subgoal by (metis atLeastAtMost_iff local.norm_le(3) order_refl t'(1))
        subgoal using e by (simp add: A_def)
        subgoal by (metis closed_segment_eq_real_ivl t'(1,5))
        subgoal by (metis closed_segment_eq_real_ivl t'(1,3))
        subgoal by (simp add: closed_segment_eq_real_ivl local.norm_le(2) t'(1))
        done
      also have " < d * exp (K * (t - t0))"
        using y d t' t
        by (intro mult_less_le_imp_less)
           (auto simp: dist_norm[symmetric] dist_commute intro!: mult_mono 0  K)
      also have "  e"
        by (rule d_times_exp_le; fact)
      finally
      have "infdist (flow t0 y t') seg < e" .
      with infdist (flow t0 y t') seg  e show False
        by (auto simp: frontier_def)
    qed

    have "{t0..b}  existence_ivl t0 y"
    by (rule subset_mem_compact_implies_subset_existence_interval[OF
      _ is_interval_cc {t0..b}  T y  X in_A compact A A  X])
      (auto simp: t0  b)
    with t0  b have b_in: "b  existence_ivl t0 y"
      by force
    {
      fix t assume t: "t  {t0 .. b}"
      also have "{t0 .. b} = {t0 -- b}"
        by (auto simp: closed_segment_eq_real_ivl assms)
      also note closed_segment_subset_existence_ivl[OF b_in]
      finally have t_in: "t  existence_ivl t0 y" .

      note t
      also note {t0 .. b} = {t0 -- b}
      also note closed_segment_subset_existence_ivl[OF assms(2)]
      finally have t_in': "t  existence_ivl t0 x0" .
      have "norm (flow t0 y t - flow t0 x0 t)  norm (y - x0) * exp (K * ¦t - t0¦)"
        unfolding K_def
        using t closed_segment_subset_existence_ivl[OF b_in] 0 < e
        by (intro in_A exponential_initial_condition[OF t_in t_in' A  X _ _ K'])
          (auto simp: closed_segment_eq_real_ivl A_def seg_def)
      hence "dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * ¦t - t0¦)"
        by (auto simp: dist_norm[symmetric] dist_commute)
    }
    note b_in this
  } from d > 0 K > 0 ball x0 d  X this show ?thesis ..
qed

lemma
  global_left_existence_ivl_explicit:
  assumes "b  t0"
  assumes b: "b  existence_ivl t0 x0"
  assumes iv_defined: "t0  T" "x0  X"
  obtains d K where "d > 0" "K > 0"
    "ball x0 d  X"
    "y. y  ball x0 d  b  existence_ivl t0 y"
    "t y. y  ball x0 d  t  {b .. t0}  dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * abs (t - t0))"
proof -
  interpret rev: ll_on_open "(preflect t0 ` T)" "(λt. - f (preflect t0 t))" X ..
  have t0': "t0  preflect t0 ` T" "x0  X"
    by (auto intro!: iv_defined)
  from assms have "preflect t0 b  t0" "preflect t0 b  rev.existence_ivl t0 x0"
    by (auto simp: rev_existence_ivl_eq)
  from rev.global_right_existence_ivl_explicit[OF this]
  obtain d K where dK: "d > 0" "K > 0"
    "ball x0 d  X"
    "y. y  ball x0 d  preflect t0 b  rev.existence_ivl t0 y"
    "t y. y  ball x0 d  t  {t0 .. preflect t0 b}  dist (rev.flow t0 x0 t) (rev.flow t0 y t)  dist x0 y * exp (K * abs (t - t0))"
    by (auto simp: rev_flow_eq x0  X)

  have ex_ivlI: "dist x0 y < d  t  existence_ivl t0 y" if "b  t" "t  t0" for t y
    using that dK(4)[of y] dK(3) iv_defined
    by (auto simp: subset_iff rev_existence_ivl_eq[of ]
      closed_segment_eq_real_ivl iv_defined in_existence_between_zeroI)
  have "b  existence_ivl t0 y" if "dist x0 y < d" for y
    using that dK
    by (subst existence_ivl_eq_rev) (auto simp: iv_defined intro!: image_eqI[where x="preflect t0 b"])
  with dK have "d > 0" "K > 0"
    "ball x0 d  X"
    "y. y  ball x0 d  b  existence_ivl t0 y"
    "t y. y  ball x0 d  t  {b .. t0}  dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * abs (t - t0))"
    by (auto simp: flow_eq_rev iv_defined ex_ivlI x0  X subset_iff
      intro!: order_trans[OF dK(5)] image_eqI[where x="preflect t0 b"])
  then show ?thesis ..
qed

lemma
  global_existence_ivl_explicit:
  assumes a: "a  existence_ivl t0 x0"
  assumes b: "b  existence_ivl t0 x0"
  assumes le: "a  b"
  obtains d K where "d > 0" "K > 0"
    "ball x0 d  X"
    "y. y  ball x0 d  a  existence_ivl t0 y"
    "y. y  ball x0 d  b  existence_ivl t0 y"
    "t y. y  ball x0 d  t  {a .. b} 
      dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * abs (t - t0))"
proof -
  note iv_defined = mem_existence_ivl_iv_defined[OF a]
  define r where "r  Max {t0, a, b}"
  define l where "l  Min {t0, a, b}"
  have r: "r  t0" "r  existence_ivl t0 x0"
    using a b by (auto simp: max_def r_def iv_defined)
  obtain dr Kr where right:
    "0 < dr" "0 < Kr" "ball x0 dr  X"
    "y. y  ball x0 dr  r  existence_ivl t0 y"
    "y t. y  ball x0 dr  t  {t0..r}  dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (Kr * ¦t - t0¦)"
    by (rule global_right_existence_ivl_explicit[OF r]) blast

  have l: "l  t0" "l  existence_ivl t0 x0"
    using a b by (auto simp: min_def l_def iv_defined)
  obtain dl Kl where left:
    "0 < dl" "0 < Kl" "ball x0 dl  X"
    "y. y  ball x0 dl  l  existence_ivl t0 y"
    "y t. y  ball x0 dl  t  {l .. t0}  dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (Kl * ¦t - t0¦)"
    by (rule global_left_existence_ivl_explicit[OF l iv_defined]) blast

  define d where "d  min dr dl"
  define K where "K  max Kr Kl"

  note iv_defined
  have "0 < d" "0 < K" "ball x0 d  X"
    using left right by (auto simp: d_def K_def)
  moreover
  {
    fix y assume y: "y  ball x0 d"
    hence "y  X" using ball x0 d  X by auto
    from y
      closed_segment_subset_existence_ivl[OF left(4), of y]
      closed_segment_subset_existence_ivl[OF right(4), of y]
    have "a  existence_ivl t0 y" "b  existence_ivl t0 y"
      by (auto simp: d_def l_def r_def min_def max_def closed_segment_eq_real_ivl split: if_split_asm)
  }
  moreover
  {
    fix t y
    assume y: "y  ball x0 d"
      and t: "t  {a .. b}"
    from y have "y  X" using ball x0 d  X by auto
    have "dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * abs (t - t0))"
    proof cases
      assume "t  t0"
      hence "dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (Kr * abs (t - t0))"
        using y t
        by (intro right) (auto simp: d_def r_def)
      also have "exp (Kr * abs (t - t0))  exp (K * abs (t - t0))"
        by (auto simp: mult_left_mono K_def max_def mult_right_mono)
      finally show ?thesis by (simp add: mult_left_mono)
    next
      assume "¬t  t0"
      hence "dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (Kl * abs (t - t0))"
        using y t
        by (intro left) (auto simp: d_def l_def)
      also have "exp (Kl * abs (t - t0))  exp (K * abs (t - t0))"
        by (auto simp: mult_left_mono K_def max_def mult_right_mono)
      finally show ?thesis by (simp add: mult_left_mono)
    qed
  } ultimately show ?thesis ..
qed

lemma eventually_exponential_separation:
  assumes a: "a  existence_ivl t0 x0"
  assumes b: "b  existence_ivl t0 x0"
  assumes le: "a  b"
  obtains K where "K > 0" "F y in at x0. t{a..b}. dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * ¦t - t0¦)"
proof -
  from global_existence_ivl_explicit[OF assms]
  obtain d K where *: "d > 0" "K > 0"
    "ball x0 d  X"
    "y. y  ball x0 d  a  existence_ivl t0 y"
    "y. y  ball x0 d  b  existence_ivl t0 y"
    "t y. y  ball x0 d  t  {a .. b} 
      dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * abs (t - t0))"
    by auto
  note K > 0
  moreover
  have "eventually (λy. y  ball x0 d) (at x0)"
    using d > 0[THEN eventually_at_ball]
    by eventually_elim simp
  hence "eventually (λy. t{a..b}. dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * ¦t - t0¦)) (at x0)"
    by eventually_elim (safe intro!: *)
  ultimately show ?thesis ..
qed

lemma eventually_mem_existence_ivl:
  assumes b: "b  existence_ivl t0 x0"
  shows "F x in at x0. b  existence_ivl t0 x"
proof -
  from mem_existence_ivl_iv_defined[OF b] have iv_defined: "t0  T" "x0  X" by simp_all
  note eiit = existence_ivl_initial_time[OF iv_defined]
  {
    fix a b
    assume assms: "a  existence_ivl t0 x0" "b  existence_ivl t0 x0" "a  b"
    from global_existence_ivl_explicit[OF assms]
    obtain d K where *: "d > 0" "K > 0"
      "ball x0 d  X"
      "y. y  ball x0 d  a  existence_ivl t0 y"
      "y. y  ball x0 d  b  existence_ivl t0 y"
      "t y. y  ball x0 d  t  {a .. b} 
        dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * abs (t - t0))"
      by auto
    have "eventually (λy. y  ball x0 d) (at x0)"
      using d > 0[THEN eventually_at_ball]
      by eventually_elim simp
    then have "F x in at x0. a  existence_ivl t0 x  b  existence_ivl t0 x"
      by (eventually_elim) (auto intro!: *)
  } from this[OF b eiit] this[OF eiit b]
  show ?thesis
    by (cases "t0  b") (auto simp: eventually_mono)
qed

lemma uniform_limit_flow:
  assumes a: "a  existence_ivl t0 x0"
  assumes b: "b  existence_ivl t0 x0"
  assumes le: "a  b"
  shows "uniform_limit {a .. b} (flow t0) (flow t0 x0) (at x0)"
proof (rule uniform_limitI)
  fix e::real assume "0 < e"
  from eventually_exponential_separation[OF assms] obtain K where "0 < K"
    "F y in at x0. t{a..b}. dist (flow t0 x0 t) (flow t0 y t)  dist x0 y * exp (K * ¦t - t0¦)"
    by auto
  note this(2)
  moreover
  let ?m = "max (abs (b - t0)) (abs (a - t0))"
  have "eventually (λy. t{a..b}. dist x0 y * exp (K * ¦t - t0¦)  dist x0 y * exp (K * ?m)) (at x0)"
    using a  b 0 < K
    by (auto intro!: mult_left_mono always_eventually)
  moreover
  have "eventually (λy. dist x0 y * exp (K * ?m) < e) (at x0)"
    using 0 < e by (auto intro!: order_tendstoD tendsto_eq_intros)
  ultimately
  show "eventually (λy. t{a..b}. dist (flow t0 y t) (flow t0 x0 t) < e) (at x0)"
    by eventually_elim (force simp: dist_commute)
qed

lemma eventually_at_fst:
  assumes "eventually P (at (fst x))"
  assumes "P (fst x)"
  shows "eventually (λh. P (fst h)) (at x)"
  using assms
  unfolding eventually_at_topological
  by (metis open_vimage_fst rangeI range_fst vimageE vimageI)

lemma eventually_at_snd:
  assumes "eventually P (at (snd x))"
  assumes "P (snd x)"
  shows "eventually (λh. P (snd h)) (at x)"
  using assms
  unfolding eventually_at_topological
  by (metis open_vimage_snd rangeI range_snd vimageE vimageI)

lemma
  shows open_state_space: "open (Sigma X (existence_ivl t0))"
  and flow_continuous_on_state_space:
    "continuous_on (Sigma X (existence_ivl t0)) (λ(x, t). flow t0 x t)"
proof (safe intro!: topological_space_class.openI continuous_at_imp_continuous_on)
  fix t x assume "x  X" and t: "t  existence_ivl t0 x"
  have iv_defined: "t0  T" "x  X"
    using mem_existence_ivl_iv_defined[OF t] by auto
  from x  X t open_existence_ivl
  obtain e where e: "e > 0" "cball t e  existence_ivl t0 x"
    by (metis open_contains_cball)
  hence ivl: "t - e  existence_ivl t0 x" "t + e  existence_ivl t0 x" "t - e  t + e"
    by (auto simp: cball_def dist_real_def)
  obtain d K where dK:
    "0 < d" "0 < K" "ball x d  X"
    "y. y  ball x d  t - e  existence_ivl t0 y"
    "y. y  ball x d  t + e  existence_ivl t0 y"
    "y s. y  ball x d  s  {t - e..t + e} 
      dist (flow t0 x s) (flow t0 y s)  dist x y * exp (K * ¦s - t0¦)"
    by (rule global_existence_ivl_explicit[OF ivl]) blast
  let ?T = "ball x d × ball t e"
  have "open ?T" by (auto intro!: open_Times)
  moreover have "(x, t)  ?T" by (auto simp: dK 0 < e)
  moreover have "?T  Sigma X (existence_ivl t0)"
  proof safe
    fix s y assume y: "y  ball x d" and s: "s  ball t e"
    with ball x d  X show "y  X" by auto
    have "ball t e  closed_segment t0 (t - e)  closed_segment t0 (t + e)"
      by (auto simp: closed_segment_eq_real_ivl dist_real_def)
    with y  X s closed_segment_subset_existence_ivl[OF dK(4)[OF y]]
      closed_segment_subset_existence_ivl[OF dK(5)[OF y]]
    show "s  existence_ivl t0 y"
      by auto
  qed
  ultimately show "T. open T  (x, t)  T  T  Sigma X (existence_ivl t0)"
    by blast
  have **: "F s in at 0. norm (flow t0 (x + fst s) (t + snd s) - flow t0 x t) < 2 * eps"
    if "eps > 0" for eps :: real
  proof -
    have "F s in at 0. norm (flow t0 (x + fst s) (t + snd s) - flow t0 x t) =
      norm (flow t0 (x + fst s) (t + snd s) - flow t0 x (t + snd s) +
        (flow t0 x (t + snd s) - flow t0 x t))"
      by auto
    moreover
    have "F s in at 0.
        norm (flow t0 (x + fst s) (t + snd s) - flow t0 x (t + snd s) +
          (flow t0 x (t + snd s) - flow t0 x t)) 
        norm (flow t0 (x + fst s) (t + snd s) - flow t0 x (t + snd s)) +
          norm (flow t0 x (t + snd s) - flow t0 x t)"
      by eventually_elim (rule norm_triangle_ineq)
    moreover
    have "F s in at 0. t + snd s  ball t e"
      by (auto simp: dist_real_def intro!: order_tendstoD[OF _ 0 < e]
        intro!: tendsto_eq_intros)
    moreover from uniform_limit_flow[OF ivl, THEN uniform_limitD, OF eps > 0]
    have "F (h::(_ )) in at (fst (0::'a*real)).
      t{t - e..t + e}. dist (flow t0 x t) (flow t0 (x + h) t) < eps"
      by (subst (asm) at_to_0)
        (auto simp: eventually_filtermap dist_commute ac_simps)
    hence "F (h::(_ * real)) in at 0.
      t{t - e..t + e}. dist (flow t0 x t) (flow t0 (x + fst h) t) < eps"
      by (rule eventually_at_fst) (simp add: eps > 0)
    moreover
    have "F h in at (snd (0::'a * _)). norm (flow t0 x (t + h) - flow t0 x t) < eps"
      using flow_continuous[OF t, unfolded isCont_def, THEN tendstoD, OF eps > 0]
      by (subst (asm) at_to_0)
        (auto simp: eventually_filtermap dist_norm ac_simps)
    hence "F h::('a * _) in at 0. norm (flow t0 x (t + snd h) - flow t0 x t) < eps"
      by (rule eventually_at_snd) (simp add: eps > 0)
    ultimately
    show ?thesis
    proof eventually_elim
      case (elim s)
      note elim(1)
      also note elim(2)
      also note elim(5)
      also
      from elim(3) have "t + snd s  {t - e..t + e}"
        by (auto simp: dist_real_def algebra_simps)
      from elim(4)[rule_format, OF this]
      have "norm (flow t0 (x + fst s) (t + snd s) - flow t0 x (t + snd s)) < eps"
        by (auto simp: dist_commute dist_norm[symmetric])
      finally
      show ?case by simp
    qed
  qed
  have *: "F s in at 0. norm (flow t0 (x + fst s) (t + snd s) - flow t0 x t) < eps"
    if "eps > 0" for eps::real
  proof -
    from that have "eps / 2 > 0" by simp
    from **[OF this] show ?thesis by auto
  qed
  show "isCont (λ(x, y). flow t0 x y) (x, t)"
    unfolding isCont_iff
    by (rule LIM_zero_cancel)
      (auto simp: split_beta' norm_conv_dist[symmetric] intro!: tendstoI *)
qed

lemmas flow_continuous_on_compose[continuous_intros] =
  continuous_on_compose_Pair[OF flow_continuous_on_state_space]

lemma flow_isCont_state_space: "t  existence_ivl t0 x0  isCont (λ(x, t). flow t0 x t) (x0, t)"
  using flow_continuous_on_state_space[of] mem_existence_ivl_iv_defined[of t x0]
  using continuous_on_eq_continuous_at open_state_space by fastforce

lemma
  flow_absolutely_integrable_on[integrable_on_simps]:
  assumes "s  existence_ivl t0 x0"
  shows "(λx. norm (flow t0 x0 x)) integrable_on closed_segment t0 s"
  using assms
  by (auto simp: closed_segment_eq_real_ivl intro!: integrable_continuous_real continuous_intros
    flow_continuous_on_intro
    intro: in_existence_between_zeroI)

lemma existence_ivl_eq_domain:
  assumes iv_defined: "t0  T" "x0  X"
  assumes bnd: "tm tM t x. tm  T  tM  T  M. L. t  {tm .. tM}. x  X. norm (f t x)  M + L * norm x"
  assumes "is_interval T" "X = UNIV"
  shows "existence_ivl t0 x0 = T"
proof -
  from assms have XI: "x  X" for x by auto
  {
    fix tm tM assume tm: "tm  T" and tM: "tM  T" and tmtM: "tm  t0" "t0  tM"
    from bnd[OF tm tM] obtain M' L'
    where bnd': "x t. x  X  tm  t  t  tM  norm (f t x)  M' + L' * norm x"
      by force
    define M where "M  norm M' + 1"
    define L where "L  norm L' + 1"
    have bnd: "x t. x  X  tm  t  t  tM  norm (f t x)  M + L * norm x"
      by (auto simp: M_def L_def intro!: bnd'[THEN order_trans] add_mono mult_mono)
    have "M > 0" "L > 0" by (auto simp: L_def M_def)

    let ?r = "(norm x0 + ¦tm - tM¦ * M + 1) * exp (L * ¦tm - tM¦)"
    define K where "K  cball (0::'a) ?r"
    have K: "compact K" "K  X"
      by (auto simp: K_def X = UNIV)
    {
      fix t assume t: "t  existence_ivl t0 x0"  and le: "tm  t" "t  tM"
      {
        fix s assume sc: "s  closed_segment t0 t"
        then have s: "s  existence_ivl t0 x0" and le: "tm  s" "s  tM" using t le sc
          using closed_segment_subset_existence_ivl
          apply -
          subgoal by force
          subgoal by (metis (full_types) atLeastAtMost_iff closed_segment_eq_real_ivl order_trans tmtM(1))
          subgoal by (metis (full_types) atLeastAtMost_iff closed_segment_eq_real_ivl order_trans tmtM(2))
          done
        from sc have nle: "norm (t0 - s)  norm (t0 - t)" by (auto simp: closed_segment_eq_real_ivl split: if_split_asm)
        from flow_fixed_point[OF s]
        have "norm (flow t0 x0 s)  norm x0 + integral (closed_segment t0 s) (λt. M + L * norm (flow t0 x0 t))"
          using tmtM
          using closed_segment_subset_existence_ivl[OF s] le
          by (auto simp:
            intro!: norm_triangle_le norm_triangle_ineq4[THEN order.trans]
              ivl_integral_norm_bound_integral bnd
              integrable_continuous_closed_segment
              integrable_continuous_real
              continuous_intros
              continuous_on_subset[OF flow_continuous_on]
              flow_in_domain
              mem_existence_ivl_subset)
          (auto simp: closed_segment_eq_real_ivl split: if_splits)
        also have " = norm x0 + norm (t0 - s) * M + L * integral (closed_segment t0 s) (λt. norm (flow t0 x0 t))"
          by (simp add: integral_add integrable_on_simps s  existence_ivl _ _
            integral_const_closed_segment abs_minus_commute)
        also have "norm (t0 - s) * M  norm (t0 - t) * M "
          using nle M > 0 by auto
        also have "   + 1" by simp
        finally have "norm (flow t0 x0 s)  norm x0 + norm (t0 - t) * M + 1 +
            L * integral (closed_segment t0 s) (λt. norm (flow t0 x0 t))" by simp
      }
      then have "norm (flow t0 x0 t)  (norm x0 + norm (t0 - t) * M + 1) * exp (L * ¦t - t0¦)"
        using closed_segment_subset_existence_ivl[OF t]
        by (intro gronwall_more_general_segment[where a=t0 and b = t and t = t])
          (auto simp: 0 < L 0 < M less_imp_le
            intro!: add_nonneg_pos mult_nonneg_nonneg add_nonneg_nonneg continuous_intros
              flow_continuous_on_intro)
      also have "  ?r"
        using le tmtM
        by (auto simp: less_imp_le 0 < M 0 < L abs_minus_commute intro!: mult_mono)
      finally
      have "flow t0 x0 t  K" by (simp add: dist_norm K_def)
    } note flow_compact = this

    have "{tm..tM}  existence_ivl t0 x0"
      using tmtM tm x0  X compact K K  X mem_is_intervalI[OF is_interval T tm  T tM  T]
      by (intro subset_mem_compact_implies_subset_existence_interval[OF _ _ _ _flow_compact])
         (auto simp: tmtM is_interval_cc)
  } note bnds = this

  show "existence_ivl t0 x0 = T"
  proof safe
    fix x assume x: "x  T"
    from bnds[OF x iv_defined(1)] bnds[OF iv_defined(1) x]
    show "x  existence_ivl t0 x0"
      by (cases "x  t0") auto
  qed (insert existence_ivl_subset, fastforce)
qed

lemma flow_unique:
  assumes "t  existence_ivl t0 x0"
  assumes "phi t0 = x0"
  assumes "t. t  existence_ivl t0 x0  (phi has_vector_derivative f t (phi t)) (at t)"
  assumes "t. t  existence_ivl t0 x0  phi t  X"
  shows "flow t0 x0 t = phi t"
  apply (rule maximal_existence_flow[where K="existence_ivl t0 x0"])
  subgoal by (auto intro!: solves_odeI simp: has_vderiv_on_def assms at_within_open[OF _ open_existence_ivl])
  subgoal by fact
  subgoal by simp
  subgoal using mem_existence_ivl_iv_defined[OF t  existence_ivl t0 x0] by simp
  subgoal by (simp add: existence_ivl_subset)
  subgoal by fact
  done

lemma flow_unique_on:
  assumes "t  existence_ivl t0 x0"
  assumes "phi t0 = x0"
  assumes "(phi has_vderiv_on (λt. f t (phi t))) (existence_ivl t0 x0)"
  assumes "t. t  existence_ivl t0 x0  phi t  X"
  shows "flow t0 x0 t = phi t"
  using flow_unique[where phi=phi, OF assms(1,2) _ assms(4)] assms(3)
  by (auto simp: has_vderiv_on_open)

end ― ‹@{thm local_lipschitz}

locale two_ll_on_open =
  F: ll_on_open T1 F X + G: ll_on_open T2 G X
  for F T1 G T2 X J x0 +
  fixes e::real and K
  assumes t0_in_J: "0  J"
  assumes J_subset: "J  F.existence_ivl 0 x0"
  assumes J_ivl: "is_interval J"
  assumes F_lipschitz: "t. t  J  K-lipschitz_on X (F t)"
  assumes K_pos: "0 < K"
  assumes F_G_norm_ineq: "t x. t  J  x  X  norm (F t x - G t x) < e"
begin

context begin

lemma F_iv_defined: "0  T1" "x0  X"
  subgoal using F.existence_ivl_initial_time_iff J_subset t0_in_J by blast
  subgoal using F.mem_existence_ivl_iv_defined(2) J_subset t0_in_J by blast
  done

lemma e_pos: "0 < e"
  using le_less_trans[OF norm_ge_zero F_G_norm_ineq[OF t0_in_J F_iv_defined(2)]]
  by assumption

qualified definition "flow0 t = F.flow 0 x0 t"
qualified definition "Y t = G.flow 0 x0 t"

lemma norm_X_Y_bound:
shows "t  J  G.existence_ivl 0 x0. norm (flow0 t - Y t)  e / K * (exp(K * ¦t¦) - 1)"
proof(safe)
  fix t assume "t  J"
  assume tG: "t  G.existence_ivl 0 x0"
  have "0  J" by (simp add: t0_in_J)

  let ?u="λt. norm (flow0 t - Y t)"
  show "norm (flow0 t - Y t)  e / K * (exp (K * ¦t¦) - 1)"
  proof(cases "0  t")
    assume "0  t"
    hence [simp]: "¦t¦ = t" by simp

    have t0_t_in_J: "{0..t}  J"
      using t  J 0  J J_ivl
      using mem_is_interval_1_I atLeastAtMost_iff subsetI by blast

    note F_G_flow_cont[continuous_intros] =
      continuous_on_subset[OF F.flow_continuous_on]
      continuous_on_subset[OF G.flow_continuous_on]

    have "?u t + e/K  e/K * exp(K * t)"
    proof(rule gronwall[where g="λt. ?u t + e/K", OF _ _ _ _ K_pos 0  t order.refl])
      fix s assume "0  s" "s  t"
      hence "{0..s}  J" using t0_t_in_J by auto

      hence t0_s_in_existence:
        "{0..s}  F.existence_ivl 0 x0"
        "{0..s}  G.existence_ivl 0 x0"
        using J_subset tG 0  s s  t G.ivl_subset_existence_ivl[OF tG]
        by auto

      hence s_in_existence:
        "s  F.existence_ivl 0 x0"
        "s  G.existence_ivl 0 x0"
          using 0  s by auto

      note cont_statements[continuous_intros] =
        F_iv_defined (*  G.iv_defined *)
        F.flow_in_domain
        G.flow_in_domain
        F.mem_existence_ivl_subset
        G.mem_existence_ivl_subset

      have [integrable_on_simps]:
        "continuous_on {0..s} (λs. F s (F.flow 0 x0 s))"
        "continuous_on {0..s} (λs. G s (G.flow 0 x0 s))"
        "continuous_on {0..s} (λs. F s (G.flow 0 x0 s))"
        "continuous_on {0..s} (λs. G s (F.flow 0 x0 s))"
        using t0_s_in_existence
        by (auto intro!: continuous_intros integrable_continuous_real)

      have "flow0 s - Y s = integral {0..s} (λs. F s (flow0 s) - G s (Y s))"
        using 0  s
        by (simp add: flow0_def Y_def Henstock_Kurzweil_Integration.integral_diff integrable_on_simps ivl_integral_def
               F.flow_fixed_point[OF s_in_existence(1)]
               G.flow_fixed_point[OF s_in_existence(2)])
      also have "... = integral {0..s} (λs. (F s (flow0 s) - F s (Y s)) + (F s (Y s) - G s (Y s)))"
        by simp
      also have "... = integral {0..s} (λs. F s (flow0 s) - F s (Y s)) + integral {0..s} (λs. F s (Y s) - G s (Y s))"
        by (simp add: Henstock_Kurzweil_Integration.integral_diff Henstock_Kurzweil_Integration.integral_add flow0_def Y_def integrable_on_simps)
      finally have "?u s  norm (integral {0..s} (λs. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (λs. F s (Y s) - G s (Y s)))"
        by (simp add: norm_triangle_ineq)
      also have "...  integral {0..s} (λs. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (λs. norm (F s (Y s) - G s (Y s)))"
        using t0_s_in_existence
        by (auto simp add: flow0_def Y_def
          intro!: add_mono continuous_intros continuous_on_imp_absolutely_integrable_on)
      also have "...  integral {0..s} (λs. K * ?u s) + integral {0..s} (λs. e)"
      proof (rule add_mono[OF integral_le integral_le])
        show "norm (F x (flow0 x) - F x (Y x))  K * norm (flow0 x - Y x)" if "x  {0..s}" for x
          using F_lipschitz[unfolded lipschitz_on_def, THEN conjunct2] that
            cont_statements(1,2,4)
            t0_s_in_existence F_iv_defined (* G.iv_defined *)
          by (metis F_lipschitz flow0_def Y_def {0..s}  J lipschitz_on_normD F.flow_in_domain
            G.flow_in_domain subsetCE)
        show "x. x  {0..s}  norm (F x (Y x) - G x (Y x))  e"
          using F_G_norm_ineq cont_statements(2,3) t0_s_in_existence
          using Y_def {0..s}  J cont_statements(5) subset_iff G.flow_in_domain
          by (metis eucl_less_le_not_le)
      qed (simp_all add: t0_s_in_existence continuous_intros integrable_on_simps flow0_def Y_def)
      also have "... = K * integral {0..s} (λs. ?u s + e / K)"
        using K_pos t0_s_in_existence
        by (simp_all add: algebra_simps Henstock_Kurzweil_Integration.integral_add flow0_def Y_def continuous_intros
          continuous_on_imp_absolutely_integrable_on)
      finally show "?u s + e / K  e / K + K * integral {0..s} (λs. ?u s + e / K)"
        by simp
    next
      show "continuous_on {0..t} (λt. norm (flow0 t - Y t) + e / K)"
        using t0_t_in_J J_subset G.ivl_subset_existence_ivl[OF tG]
        by (auto simp add: flow0_def Y_def intro!: continuous_intros)
    next
      fix s assume "0  s" "s  t"
      show "0  norm (flow0 s - Y s) + e / K"
        using e_pos K_pos by simp
    next
      show "0 < e / K" using e_pos K_pos by simp
    qed
    thus ?thesis by (simp add: algebra_simps)
  next
    assume "¬0  t"
    hence "t  0" by simp
    hence [simp]: "¦t¦ = -t" by simp

    have t0_t_in_J: "{t..0}  J"
      using t  J 0  J J_ivl ¬ 0  t atMostAtLeast_subset_convex is_interval_convex_1
      by auto

    note F_G_flow_cont[continuous_intros] =
      continuous_on_subset[OF F.flow_continuous_on]
      continuous_on_subset[OF G.flow_continuous_on]

    have "?u t + e/K  e/K * exp(- K * t)"
    proof(rule gronwall_left[where g="λt. ?u t + e/K", OF _ _ _ _ K_pos order.refl t  0])
      fix s assume "t  s" "s  0"
      hence "{s..0}  J" using t0_t_in_J by auto

      hence t0_s_in_existence:
        "{s..0}  F.existence_ivl 0 x0"
        "{s..0}  G.existence_ivl 0 x0"
        using J_subset G.ivl_subset_existence_ivl'[OF tG] s  0 t  s
        by auto

      hence s_in_existence:
        "s  F.existence_ivl 0 x0"
        "s  G.existence_ivl 0 x0"
          using s  0 by auto

      note cont_statements[continuous_intros] =
        F_iv_defined
        F.flow_in_domain
        G.flow_in_domain
        F.mem_existence_ivl_subset
        G.mem_existence_ivl_subset
      then have [continuous_intros]:
        "{s..0}  T1"
        "{s..0}  T2"
        "F.flow 0 x0 ` {s..0}  X"
        "G.flow 0 x0 ` {s..0}  X"
        "s  x  x  0  x  F.existence_ivl 0 x0"
        "s  x  x  0  x  G.existence_ivl 0 x0" for x
        using t0_s_in_existence
        by auto
      have "flow0 s - Y s = - integral {s..0} (λs. F s (flow0 s) - G s (Y s))"
        using t0_s_in_existence s  0
        by (simp add: flow0_def Y_def ivl_integral_def
               F.flow_fixed_point[OF s_in_existence(1)]
               G.flow_fixed_point[OF s_in_existence(2)]
               continuous_intros integrable_on_simps Henstock_Kurzweil_Integration.integral_diff)
      also have "... = - integral {s..0} (λs. (F s (flow0 s) - F s (Y s)) + (F s (Y s) - G s (Y s)))"
        by simp
      also have "... = - (integral {s..0} (λs. F s (flow0 s) - F s (Y s)) + integral {s..0} (λs. F s (Y s) - G s (Y s)))"
        using t0_s_in_existence
        by (subst Henstock_Kurzweil_Integration.integral_add) (simp_all add: integral_add flow0_def Y_def continuous_intros integrable_on_simps)
      finally have "?u s  norm (integral {s..0} (λs. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (λs. F s (Y s) - G s (Y s)))"
        by (metis (no_types, lifting) norm_minus_cancel norm_triangle_ineq)
      also have "...  integral {s..0} (λs. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (λs. norm (F s (Y s) - G s (Y s)))"
        using t0_s_in_existence
        by (auto simp add: flow0_def Y_def intro!: continuous_intros continuous_on_imp_absolutely_integrable_on add_mono)
      also have "...  integral {s..0} (λs. K * ?u s) + integral {s..0} (λs. e)"
      proof (rule add_mono[OF integral_le integral_le])
        show "norm (F x (flow0 x) - F x (Y x))  K * norm (flow0 x - Y x)" if "x{s..0}" for x
          using F_lipschitz[unfolded lipschitz_on_def, THEN conjunct2]
            cont_statements(1,2,4) that
            t0_s_in_existence F_iv_defined (* G.iv_defined *)
          by (metis F_lipschitz flow0_def Y_def {s..0}  J lipschitz_on_normD F.flow_in_domain
            G.flow_in_domain subsetCE)
        show "x. x  {s..0}  norm (F x (Y x) - G x (Y x))  e"
          using F_G_norm_ineq Y_def {s..0}  J cont_statements(5) subset_iff t0_s_in_existence(2)
          using Y_def {s..0}  J cont_statements(5) subset_iff G.flow_in_domain
          by (metis eucl_less_le_not_le)
      qed (simp_all add: t0_s_in_existence continuous_intros integrable_on_simps flow0_def Y_def)
      also have "... = K * integral {s..0} (λs. ?u s + e / K)"
        using K_pos t0_s_in_existence
        by (simp_all add: algebra_simps Henstock_Kurzweil_Integration.integral_add t0_s_in_existence continuous_intros integrable_on_simps flow0_def Y_def)
      finally show "?u s + e / K  e / K + K * integral {s..0} (λs. ?u s + e / K)"
        by simp
    next
      show "continuous_on {t..0} (λt. norm (flow0 t - Y t) + e / K)"
        using t0_t_in_J J_subset G.ivl_subset_existence_ivl'[OF tG] F_iv_defined
        by (auto simp add: flow0_def Y_def intro!: continuous_intros)
    next
      fix s assume "t  s" "s  0"
      show "0  norm (flow0 s - Y s) + e / K"
        using e_pos K_pos by simp
    next
      show "0 < e / K" using e_pos K_pos by simp
    qed
    thus ?thesis by (simp add: algebra_simps)
  qed
qed

end

end

locale auto_ll_on_open =
  fixes f::"'a::{banach, heine_borel}  'a" and X
  assumes auto_local_lipschitz: "local_lipschitz UNIV X (λ_::real. f)"
  assumes auto_open_domain[intro!, simp]: "open X"
begin

text ‹autonomous flow and existence interval ›

definition "flow0 x0 t = ll_on_open.flow UNIV (λ_. f) X 0 x0 t"

definition "existence_ivl0 x0 = ll_on_open.existence_ivl UNIV (λ_. f) X 0 x0"

sublocale ll_on_open_it UNIV "λ_. f" X 0
  rewrites "flow = (λt0 x0 t. flow0 x0 (t - t0))"
       and "existence_ivl = (λt0 x0. (+) t0 ` existence_ivl0 x0)"
       and "(+) 0 = (λx::real. x)"
       and "s - 0 = s"
       and "(λx. x) ` S = S"
       and "s  (+) t ` S  s - t  (S::real set)"
       and "P (s + t - s) = P (t::real)"― ‹TODO: why does just the equation not work?›
       and "P (t + s - s) = P t"― ‹TODO: why does just the equation not work?›
proof -
  interpret ll_on_open UNIV "λ_. f" X
    by unfold_locales (auto intro!: continuous_on_const auto_local_lipschitz)
  show "ll_on_open_it UNIV (λ_. f) X" ..
  show "(+) 0 = (λx::real. x)" "(λx. x) ` S = S" "s - 0 = s" "P (t + s - s) = P t" "P (s + t - s) = P (t::real)"
    by auto
  show "flow = (λt0 x0 t. flow0 x0 (t - t0))"
    unfolding flow0_def
    by (metis flow_def flow_shift_autonomous1 flow_shift_autonomous2 mem_existence_ivl_iv_defined(2))
  show "existence_ivl = (λt0 x0. (+) t0 ` existence_ivl0 x0)"
    unfolding existence_ivl0_def
    apply (safe intro!: ext)
    subgoal using image_iff mem_existence_ivl_shift_autonomous1 by fastforce
    subgoal premises prems for t0 x0 x s
    proof -
      have f2: "x1 x2. (x2::real) - x1 = - 1 * x1 + x2"
        by auto
      have "- 1 * t0 + (t0 + s) = s"
        by auto
      then show ?thesis
        using f2 prems mem_existence_ivl_iv_defined(2) mem_existence_ivl_shift_autonomous2
        by presburger
    qed
    done
  show "(s  (+) t ` S) = (s - t  S)" by force
qed
― ‹at this point, there should be no theorems about existence_ivl›, only existence_ivl0›.
Moreover, (+) _ ` _› and _ + _ - _› etc should have been removed›

lemma existence_ivl_zero: "x0  X  0  existence_ivl0 x0" by simp

lemmas [continuous_intros del] = continuous_on_f
lemmas continuous_on_f_comp[continuous_intros] = continuous_on_f[OF continuous_on_const _ subset_UNIV]

lemma
  flow_in_compact_right_existence:
  assumes "t. 0  t  t  existence_ivl0 x  flow0 x t  K"
  assumes "compact K" "K  X"
  assumes "x  X" "t  0"
  shows "t  existence_ivl0 x"
proof (rule ccontr)
  assume "t  existence_ivl0 x"
  have "bdd_above (existence_ivl0 x)"
    by (rule bdd_above_is_intervalI[OF is_interval_existence_ivl 0  t existence_ivl_zero]) fact+
  from sup_existence_maximal[OF UNIV_I x  X assms(1-3) this]
  show False by auto
qed

lemma
  flow_in_compact_left_existence:
  assumes "t. t  0  t  existence_ivl0 x  flow0 x t  K"
  assumes "compact K" "K  X"
  assumes "x  X" "t  0"
  shows "t  existence_ivl0 x"
proof (rule ccontr)
  assume "t  existence_ivl0 x"
  have "bdd_below (existence_ivl0 x)"
    by (rule bdd_below_is_intervalI[OF is_interval_existence_ivl t  0 _ existence_ivl_zero]) fact+
  from inf_existence_minimal[OF UNIV_I x  X assms(1-3) this]
  show False by auto
qed

end

locale compact_continuously_diff =
  derivative_on_prod T X f "λ(t, x). f' x oL snd_blinfun"
    for T X and f::"real  'a::{banach,perfect_space,heine_borel}  'a"
    and f'::"'a  ('a, 'a) blinfun" +
  assumes compact_domain: "compact X"
  assumes convex: "convex X"
  assumes nonempty_domains: "T  {}" "X  {}"
  assumes continuous_derivative: "continuous_on X f'"
begin

lemma ex_onorm_bound:
  "B. x  X. norm (f' x)  B"
proof -
  from _ compact_domain have "compact (f' ` X)"
    by (intro compact_continuous_image continuous_derivative)
  hence "bounded (f' ` X)" by (rule compact_imp_bounded)
  thus ?thesis
    by (auto simp add: bounded_iff cball_def norm_blinfun.rep_eq)
qed

definition "onorm_bound = (SOME B. x  X. norm (f' x)  B)"

lemma onorm_bound: assumes "x  X" shows "norm (f' x)  onorm_bound"
  unfolding onorm_bound_def
  using someI_ex[OF ex_onorm_bound] assms
  by blast

sublocale closed_domain X
  using compact_domain by unfold_locales (rule compact_imp_closed)

sublocale global_lipschitz T X f onorm_bound
proof (unfold_locales, rule lipschitz_onI)
  fix t z y
  assume "t  T" "y  X" "z  X"
  then have "norm (f t y - f t z)  onorm_bound * norm (y - z)"
    using onorm_bound
    by (intro differentiable_bound[where f'=f', OF convex])
       (auto intro!: derivative_eq_intros simp: norm_blinfun.rep_eq)
  thus "dist (f t y) (f t z)  onorm_bound * dist y z"
    by (auto simp: dist_norm norm_Pair)
next
  from nonempty_domains obtain x where x: "x  X" by auto
  show "0  onorm_bound"
    using dual_order.trans local.onorm_bound norm_ge_zero x by blast
qed

end ― ‹@{thm compact_domain}

locale unique_on_compact_continuously_diff = self_mapping +
  compact_interval T +
  compact_continuously_diff T X f
begin

sublocale unique_on_closed t0 T x0 f X onorm_bound
  by unfold_locales (auto intro!: f' has_derivative_continuous_on)

end

locale c1_on_open =
  fixes f::"'a::{banach, perfect_space, heine_borel}  'a" and f' X
  assumes open_dom[simp]: "open X"
  assumes derivative_rhs:
    "x. x  X  (f has_derivative blinfun_apply (f' x)) (at x)"
  assumes continuous_derivative: "continuous_on X f'"
begin

lemmas continuous_derivative_comp[continuous_intros] =
  continuous_on_compose2[OF continuous_derivative]

lemma derivative_tendsto[tendsto_intros]:
  assumes [tendsto_intros]: "(g  l) F"
    and "l  X"
  shows "((λx. f' (g x))  f' l) F"
  using continuous_derivative[simplified continuous_on] assms
  by (auto simp: at_within_open[OF _ open_dom]
    intro!: tendsto_eq_intros
    intro: tendsto_compose)

lemma c1_on_open_rev[intro, simp]: "c1_on_open (-f) (-f') X"
  using derivative_rhs continuous_derivative
  by unfold_locales
    (auto intro!: continuous_intros derivative_eq_intros
    simp: fun_Compl_def blinfun.bilinear_simps)

lemma derivative_rhs_compose[derivative_intros]:
  "((g has_derivative g') (at x within s))  g x  X 
    ((λx. f (g x)) has_derivative
      (λxa. blinfun_apply (f' (g x)) (g' xa)))
    (at x within s)"
  by (metis has_derivative_compose[of g g' x s f "f' (g x)"] derivative_rhs)

sublocale auto_ll_on_open
proof (standard, rule local_lipschitzI)
  fix x and t::real
  assume "x  X"
  with open_contains_cball[of "UNIV::real set"] open_UNIV
    open_contains_cball[of X] open_dom
  obtain u v where uv: "cball t u  UNIV" "cball x v  X" "u > 0" "v > 0"
    by blast
  let ?T = "cball t u" and ?X = "cball x v"
  have "bounded ?X" by simp
  have "compact (cball x v)"
    by simp
  interpret compact_continuously_diff ?T ?X "λ_. f" f'
    using uv
    by unfold_locales
      (auto simp: convex_cball cball_eq_empty split_beta'
        intro!: derivative_eq_intros continuous_on_compose2[OF continuous_derivative]
          continuous_intros)
  have "onorm_bound-lipschitz_on ?X f"
    using lipschitz[of t] uv
    by auto
  thus "u>0. L. t  cball t u  UNIV. L-lipschitz_on (cball x u  X) f"
    by (intro exI[where x=v])
      (auto intro!: exI[where x=onorm_bound] 0 < v simp: Int_absorb2 uv)
qed (auto intro!: continuous_intros)

end ― ‹@{thm derivative_rhs}

locale c1_on_open_euclidean = c1_on_open f f' X
  for f::"'a::euclidean_space  _" and f' X
begin
lemma c1_on_open_euclidean_anchor: True ..

definition "vareq x0 t = f' (flow0 x0 t)"

interpretation var: ll_on_open "existence_ivl0 x0" "vareq x0" UNIV
  apply standard
  apply (auto intro!: c1_implies_local_lipschitz[where f' = "λ(t, x). vareq x0 t"] continuous_intros
      derivative_eq_intros
      simp: split_beta' blinfun.bilinear_simps vareq_def)
  using local.mem_existence_ivl_iv_defined(2) apply blast
  using local.existence_ivl_reverse local.mem_existence_ivl_iv_defined(2) apply blast
  using local.mem_existence_ivl_iv_defined(2) apply blast
  using local.existence_ivl_reverse local.mem_existence_ivl_iv_defined(2) apply blast
  done

context begin

lemma continuous_on_A[continuous_intros]:
  assumes "continuous_on S a"
  assumes "continuous_on S b"
  assumes "s. s  S  a s  X"
  assumes "s. s  S  b s  existence_ivl0 (a s)"
  shows "continuous_on S (λs. vareq (a s) (b s))"
proof -
  have "continuous_on S (λx. f' (flow0 (a x) (b x)))"
    by (auto intro!: continuous_intros assms flow_in_domain)
  then show ?thesis
    by (rule continuous_on_eq) (auto simp: assms vareq_def)
qed

lemmas [intro] = mem_existence_ivl_iv_defined

context
  fixes x0::'a
begin

lemma flow0_defined: "xa  existence_ivl0 x0  flow0 x0 xa  X"
  by (auto simp: flow_in_domain)

lemma continuous_on_flow0: "continuous_on (existence_ivl0 x0) (flow0 x0)"
  by (auto simp: intro!: continuous_intros)

lemmas continuous_on_flow0_comp[continuous_intros] = continuous_on_compose2[OF continuous_on_flow0]

lemma varexivl_eq_exivl:
  assumes "t  existence_ivl0 x0"
  shows "var.existence_ivl x0 t a = existence_ivl0 x0"
proof (rule var.existence_ivl_eq_domain)
  fix s t x
  assume s: "s  existence_ivl0 x0" and t: "t  existence_ivl0 x0"
  then have "{s .. t}  existence_ivl0 x0"
    by (metis atLeastatMost_empty_iff2 empty_subsetI real_Icc_closed_segment var.closed_segment_subset_domain)
  then have "continuous_on {s .. t} (vareq x0)"
    by (auto simp: closed_segment_eq_real_ivl intro!: continuous_intros flow0_defined)
  then have "compact ((vareq x0) ` {s .. t})"
    using compact_Icc
    by (rule compact_continuous_image)
  then obtain B where B: "u. u  {s .. t}  norm (vareq x0 u)  B"
    by (force dest!: compact_imp_bounded simp: bounded_iff)
  show "M L. t{s..t}. xUNIV. norm (blinfun_apply (vareq x0 t) x)  M + L * norm x"
    by (rule exI[where x=0], rule exI[where x=B])
      (auto intro!: order_trans[OF norm_blinfun] mult_right_mono B simp:)
qed (auto intro: assms)

definition "vector_Dflow u0 t  var.flow x0 0 u0 t"

qualified abbreviation "Y z t  flow0 (x0 + z) t"

text ‹Linearity of the solution to the variational equation.
  TODO: generalize this and some other things for arbitrary linear ODEs›
lemma vector_Dflow_linear:
assumes "t  existence_ivl0 x0"
shows "vector_Dflow (α *R a + β *R b) t = α *R vector_Dflow a t + β *R vector_Dflow b t"
proof -
  note mem_existence_ivl_iv_defined[OF assms, intro, simp]
  have "((λc. α *R var.flow x0 0 a c + β *R var.flow x0 0 b c) solves_ode (λx. vareq x0 x)) (existence_ivl0 x0) UNIV"
    by (auto intro!: derivative_intros var.flow_has_vector_derivative solves_odeI
      simp: blinfun.bilinear_simps varexivl_eq_exivl vareq_def[symmetric])
  moreover
  have "α *R var.flow x0 0 a 0 + β *R var.flow x0 0 b 0 = α *R a + β *R b" by simp
  moreover note is_interval_existence_ivl[of x0]
  ultimately show ?thesis
    unfolding vareq_def[symmetric] vector_Dflow_def
    by (rule var.maximal_existence_flow) (auto simp: assms)
qed

lemma linear_vector_Dflow:
assumes "t  existence_ivl0 x0"
shows "linear (λz. vector_Dflow z t)"
using vector_Dflow_linear[OF assms, of 1 _ 1] vector_Dflow_linear[OF assms, of _ _ 0]
by (auto intro!: linearI)

lemma bounded_linear_vector_Dflow:
assumes "t  existence_ivl0 x0"
shows "bounded_linear (λz. vector_Dflow z t)"
by (simp add: linear_linear linear_vector_Dflow assms)

lemma vector_Dflow_continuous_on_time: "x0  X  continuous_on (existence_ivl0 x0) (λt. vector_Dflow z t)"
  using var.flow_continuous_on[of x0 0 z] varexivl_eq_exivl
  unfolding vector_Dflow_def
  by (auto simp:  )

proposition proposition_17_6_weak:
  ― ‹from "Differential Equations, Dynamical Systems, and an Introduction to Chaos",
    Hirsch/Smale/Devaney›
assumes "t  existence_ivl0 x0"
shows "(λy. (Y (y - x0) t - flow0 x0 t - vector_Dflow (y - x0) t) /R norm (y - x0))  x0  0"
proof-
  note x0_def = mem_existence_ivl_iv_defined[OF assms]
  have "0  existence_ivl0 x0"
    by (simp add: x0_def)

  text ‹Find some J ⊆ existence_ivl0 x0› with 0 ∈ J› and t ∈ J›.›
  define t0 where "t0  min 0 t"
  define t1 where "t1  max 0 t"
  define J where "J  {t0..t1}"

  have "t0  0" "0  t1" "0  J" "J  {}" "t  J" "compact J"
  and J_in_existence: "J  existence_ivl0 x0"
    using ivl_subset_existence_ivl ivl_subset_existence_ivl' x0_def assms
    by (auto simp add: J_def t0_def t1_def min_def max_def)

  {
    fix z S
    assume assms: "x0 + z  X" "S  existence_ivl0 (x0 + z)"
    have "continuous_on S (Y z)"
      using flow_continuous_on assms(1)
      by (intro continuous_on_subset[OF _ assms(2)]) (simp add:)
  }
  note [continuous_intros] = this integrable_continuous_real blinfun.continuous_on

  have U_continuous[continuous_intros]: "z. continuous_on J (vector_Dflow z)"
    by(rule continuous_on_subset[OF vector_Dflow_continuous_on_time[OF x0  X] J_in_existence])

  from t  J
  have "t0  t"
  and "t  t1"
  and "t0  t1"
  and "t0  existence_ivl0 x0"
  and "t  existence_ivl0 x0"
  and "t1  existence_ivl0 x0"
    using J_def J_in_existence by auto
  from global_existence_ivl_explicit[OF t0  existence_ivl0 x0 t1  existence_ivl0 x0 t0  t1]
  obtain u K where uK_def:
    "0 < u"
    "0 < K"
    "ball x0 u  X"
    "y. y  ball x0 u  t0  existence_ivl0 y"
    "y. y  ball x0 u  t1  existence_ivl0 y"
    "t y. y  ball x0 u  t  J  dist (flow0 x0 t) (Y (y - x0) t)  dist x0 y * exp (K * ¦t¦)"
    by (auto simp add: J_def)

  have J_in_existence_ivl: "y. y  ball x0 u  J  existence_ivl0 y"
    unfolding J_def
    using uK_def
    by (simp add: real_Icc_closed_segment segment_subset_existence_ivl t0_def t1_def)
  have ball_in_X: "z. z  ball 0 u  x0 + z  X"
    using uK_def(3)
    by (auto simp: dist_norm)

  have flow0_J_props: "flow0 x0 ` J  {}" "compact (flow0 x0 ` J)" "flow0 x0` J  X"
    using t0  t1
    using J_def(1) J_in_existence
    by (auto simp add: J_def intro!:
      compact_continuous_image continuous_intros flow_in_domain)

  have [continuous_intros]: "continuous_on J (λs. f' (flow0 x0 s))"
    using J_in_existence
    by (auto intro!: continuous_intros flow_in_domain simp:)

  text ‹ Show the thesis via cases t = 0›, 0 < t› and t < 0›. ›
  show ?thesis
  proof(cases "t = 0")
    assume "t = 0"
    show ?thesis
    unfolding t = 0 Lim_at
    proof(simp add: dist_norm[of _ 0] del: zero_less_dist_iff, safe, rule exI, rule conjI[OF 0 < u], safe)
      fix e::real and x assume "0 < e" "dist x x0 < u"
      hence "x  X"
        using uK_def(3)
        by (auto simp: dist_commute)
      hence "inverse (norm (x - x0)) * norm (Y (x - x0) 0 - flow0 x0 0 - vector_Dflow (x - x0) 0) = 0"
        using x0_def
        by (simp add: vector_Dflow_def)
      thus "inverse (norm (x - x0)) * norm (flow0 x 0 - flow0 x0 0 - vector_Dflow (x - x0) 0) < e"
        using 0 < e by auto
    qed
  next
    assume "t  0"
    show ?thesis
    proof(unfold Lim_at, safe)
      fix e::real assume "0 < e"
      then obtain e' where "0 < e'" "e' < e"
        using dense by auto

      obtain N
        where N_ge_SupS: "Sup { norm (f' (flow0 x0 s)) |s. s  J }  N" (is "Sup ?S  N")
          and N_gr_0: "0 < N"
        ― ‹We need N to be an upper bound of @{term ?S}, but also larger than zero.›
        by (meson le_cases less_le_trans linordered_field_no_ub)
      have N_ineq: "s. s  J  norm (f' (flow0 x0 s))  N"
        proof-
          fix s assume "s  J"
          have "?S = (norm o f' o flow0 x0) ` J" by auto
          moreover have "continuous_on J (norm o f' o flow0 x0)"
            using J_in_existence
            by (auto intro!: continuous_intros)
          ultimately have  "a b. ?S = {a..b}  a  b"
            using continuous_image_closed_interval[OF t0  t1]
            by (simp add: J_def)
          then obtain a b where "?S = {a..b}" and "a  b" by auto
          hence "bdd_above ?S" by simp
          from s  J  cSup_upper[OF _ this]
          have "norm (f' (flow0 x0 s))  Sup ?S"
            by auto
          thus "norm (f' (flow0 x0 s))  N"
            using N_ge_SupS by simp
        qed

      text ‹ Define a small region around flow0 ` J›, that is a subset of the domain X›. ›
      from compact_in_open_separated[OF flow0_J_props(1,2) auto_open_domain flow0_J_props(3)]
        obtain e_domain where e_domain_def: "0 < e_domain" "{x. infdist x (flow0 x0 ` J)  e_domain}  X"
        by auto
      define G where "G  {xX. infdist x (flow0 x0 ` J) < e_domain}"
      have G_vimage: "G = ((λx. infdist x (flow0 x0 ` J)) -` {..<e_domain})  X"
        by (auto simp: G_def)
      have "open G" "G  X"
        unfolding G_vimage
        by (auto intro!: open_Int open_vimage continuous_intros continuous_at_imp_continuous_on)

      text ‹Define a compact subset H of G. Inside H, we can guarantee
         an upper bound on the Taylor remainder.›
      define e_domain2 where "e_domain2  e_domain / 2"
      have "e_domain2 > 0" "e_domain2 < e_domain" using e_domain > 0
        by (simp_all add: e_domain2_def)
      define H where "H  {x. infdist x (flow0 x0 ` J)  e_domain2}"
      have H_props: "H  {}" "compact H" "H  G"
        proof-
          have "x0  flow0 x0 ` J"
            unfolding image_iff
            using 0  J  x0_def
            by force

          hence "x0  H"
            using 0 < e_domain2
            by (simp add: H_def x0_def)
          thus "H  {}"
            by auto
        next
          show "compact H"
            unfolding H_def
            using 0 < e_domain2 flow0_J_props
            by (intro compact_infdist_le) simp_all
        next
          show "H  G"
          proof
            fix x assume "x  H"
            then have *: "infdist x (flow0 x0 ` J) < e_domain"
              using 0 < e_domain
              by (simp add: H_def e_domain2_def)
            then have "x  X"
              using e_domain_def(2)
              by auto
            with * show "x  G"
              unfolding G_def
              by auto
          qed
        qed

      have f'_cont_on_G: "(x. x  G  isCont f' x)"
        using continuous_on_interior[OF continuous_on_subset[OF continuous_derivative G  X]]
        by (simp add: interior_open[OF open G])

      define e1 where "e1  e' / (¦t¦ * exp (K * ¦t¦) * exp (N * ¦t¦))"
        ― ‹@{term e1} is the bounding term for the Taylor remainder.›
      have "0 < ¦t¦"
        using t  0
        by simp
      hence "0 < e1"
        using 0 < e'
        by (simp add: e1_def)

      text ‹ Taylor expansion of f on set G. ›
      from uniform_explicit_remainder_Taylor_1[where f=f and f'=f',
        OF derivative_rhs[OF subsetD[OF G  X]] f'_cont_on_G open G H_props 0 < e1]
      obtain d_Taylor R
      where Taylor_expansion:
        "0 < d_Taylor"
        "x z. f z = f x + (f' x) (z - x) + R x z"
        "x y. x  H  y  H  dist x y < d_Taylor  norm (R x y)  e1 * dist x y"
        "continuous_on (G × G) (λ(a, b). R a b)"
          by auto

      text ‹ Find d, such that solutions are always at least min (e_domain/2) d_Taylor› apart,
         i.e. always in H. This later gives us the bound on the remainder. ›
      have "0 < min (e_domain/2) d_Taylor"
        using 0 < d_Taylor 0 < e_domain
        by auto
      from uniform_limit_flow[OF t0  existence_ivl0 x0 t1  existence_ivl0 x0 t0  t1,
        THEN uniform_limitD, OF this, unfolded eventually_at]
      obtain d_ivl where d_ivl_def:
        "0 < d_ivl"
        "x. 0 < dist x x0  dist x x0 < d_ivl 
          (tJ. dist (flow0 x0 t) (Y (x - x0) t) < min (e_domain / 2) d_Taylor)"
        by (auto simp: dist_commute J_def)

      define d where "d  min u d_ivl"
      have "0 < d" using 0 < u 0 < d_ivl
        by (simp add: d_def)
      hence "d  u" "d  d_ivl"
        by (auto simp: d_def)

      text ‹ Therefore, any flow0 starting in ball x0 d› will be in G. ›
      have Y_in_G: "y. y  ball x0 d  (λs. Y (y - x0) s) ` J  G"
        proof
          fix x y assume assms: "y  ball x0 d" "x  (λs. Y (y - x0) s) ` J"
          show "x  G"
          proof(cases)
            assume "y = x0"
            from assms(2)
            have "x  flow0 x0 ` J"
              by (simp add: y = x0)
            thus "x  G"
              using 0 < e_domain flow0 x0 ` J  X
              by (auto simp: G_def)
          next
            assume "y  x0"
            hence "0 < dist y x0"
              by (simp add: dist_norm)
            from d_ivl_def(2)[OF this] d  d_ivl  0 < e_domain assms(1)
            have dist_flow0_Y: "t. t  J  dist (flow0 x0 t) (Y (y - x0) t) < e_domain"
              by (auto simp: dist_commute)

            from assms(2)
            obtain t where t_def: "t  J" "x = Y (y - x0) t"
              by auto
            have "x  X"
              unfolding t_def(2)
              using uK_def(3) assms(1) d  u subsetD[OF J_in_existence_ivl t_def(1)]
              by (auto simp: intro!: flow_in_domain)

            have "flow0 x0 t  flow0 x0 ` J" using t_def by auto
            from dist_flow0_Y[OF t_def(1)]
            have "dist x (flow0 x0 t) < e_domain"
              by (simp add: t_def(2) dist_commute)
            from le_less_trans[OF infdist_le[OF flow0 x0 t  flow0 x0 ` J] this] x  X
            show "x  G"
              by (auto simp: G_def)
          qed
        qed
      from this[of x0] 0 < d
      have X_in_G: "flow0 x0 ` J  G"
        by simp

      show "d>0. x. 0 < dist x x0  dist x x0 < d 
                     dist ((Y (x - x0) t - flow0 x0 t - vector_Dflow (x - x0) t) /R norm (x - x0)) 0 < e"
      proof(rule exI, rule conjI[OF 0 < d], safe, unfold norm_conv_dist[symmetric])
        fix x assume x_x0_dist: "0 < dist x x0" "dist x x0 < d"
        hence x_in_ball': "x  ball x0 d"
          by (simp add: dist_commute)
        hence x_in_ball: "x  ball x0 u"
          using d  u
          by simp

        text ‹ First, some prerequisites. ›
        from x_in_ball
        have z_in_ball: "x - x0  ball 0 u"
          using 0 < u
          by (simp add: dist_norm)
        hence [continuous_intros]: "dist x0 x < u"
          by (auto simp: dist_norm)

        from J_in_existence_ivl[OF x_in_ball]
        have J_in_existence_ivl_x: "J  existence_ivl0 x" .
        from ball_in_X[OF z_in_ball]
        have x_in_X[continuous_intros]: "x  X"
          by simp

        text ‹ On all of J›, we can find upper bounds for the distance of flow0› and Y›. ›
        have dist_flow0_Y: "s. s  J  dist (flow0 x0 s) (Y (x - x0) s)  dist x0 x * exp (K * ¦t¦)"
          using t0_def t1_def uK_def(2)
          by (intro order_trans[OF uK_def(6)[OF x_in_ball] mult_left_mono])
             (auto simp add: J_def intro!: mult_mono)
        from d_ivl_def x_x0_dist d  d_ivl
        have dist_flow0_Y2: "t. t  J  dist (flow0 x0 t) (Y (x - x0) t) < min (e_domain2) d_Taylor"
          by (auto simp: e_domain2_def)

        let ?g = "λt. norm (Y (x - x0) t - flow0 x0 t - vector_Dflow (x - x0) t)"
        let ?C = "¦t¦ * dist x0 x * exp (K * ¦t¦) * e1"
        text ‹ Find an upper bound to ?g›, i.e. show that
             ?g s ≤ ?C + N * integral {a..b} ?g›
           for {a..b} = {0..s}› or {a..b} = {s..0}› for some s ∈ J›.
           We can then apply Grönwall's inequality to obtain a true bound for ?g›. ›
        have g_bound: "?g s  ?C + N * integral {a..b} ?g"
          if s_def: "s  {a..b}"
          and J'_def: "{a..b}  J"
          and ab_cases: "(a = 0  b = s)  (a = s  b = 0)"
          for s a b
        proof -
          from that have "s  J" by auto

          have s_in_existence_ivl_x0: "s  existence_ivl0 x0"
            using J_in_existence s  J by auto
          have s_in_existence_ivl: "y. y  ball x0 u  s  existence_ivl0 y"
            using J_in_existence_ivl s  J by auto
          have s_in_existence_ivl2: "z. z  ball 0 u  s  existence_ivl0 (x0 + z)"
            using s_in_existence_ivl
            by (simp add: dist_norm)

          text ‹Prove continuities beforehand.›
          note continuous_on_0_s[continuous_intros] = continuous_on_subset[OF _ {a..b}  J]

          have[continuous_intros]: "continuous_on J (flow0 x0)"
            using J_in_existence
            by (auto intro!: continuous_intros simp:)
          {
            fix z S
            assume assms: "x0 + z  X" "S  existence_ivl0 (x0 + z)"
            have "continuous_on S (λs. f (Y z s))"
            proof(rule continuous_on_subset[OF _ assms(2)])
              show "continuous_on (existence_ivl0 (x0 + z)) (λs. f (Y z s))"
                using assms
                by (auto intro!: continuous_intros flow_in_domain flow_continuous_on simp:)
            qed
          }
          note [continuous_intros] = this

          have [continuous_intros]: "continuous_on J (λs. f (flow0 x0 s))"
            by(rule continuous_on_subset[OF _ J_in_existence])
              (auto intro!: continuous_intros flow_continuous_on flow_in_domain simp: x0_def)

          have [continuous_intros]: "z. continuous_on J (λs. f' (flow0 x0 s) (vector_Dflow z s))"
          proof-
            fix z
            have a1: "continuous_on J (flow0 x0)"
              by (auto intro!: continuous_intros)

            have a2: "(λs. (flow0 x0 s, vector_Dflow z s)) ` J  (flow0 x0 ` J) × ((λs. vector_Dflow z s) ` J)"
              by auto
            have a3: "continuous_on ((λs. (flow0 x0 s, vector_Dflow z s)) ` J) (λ(x, u). f' x u)"
              using assms flow0_J_props
              by (auto intro!: continuous_intros simp: split_beta')
            from continuous_on_compose[OF continuous_on_Pair[OF a1 U_continuous] a3]
            show "continuous_on J (λs. f' (flow0 x0 s) (vector_Dflow z s))"
              by simp
          qed

          have [continuous_intros]: "continuous_on J (λs. R (flow0 x0 s) (Y (x - x0) s))"
            using J_in_existence J_in_existence_ivl[OF x_in_ball] X_in_G {a..b}  J Y_in_G
              x_x0_dist
            by (auto intro!: continuous_intros continuous_on_compose_Pair[OF Taylor_expansion(4)]
              simp: dist_commute subset_iff)
          hence [continuous_intros]:
            "(λs. R (flow0 x0 s) (Y (x - x0) s)) integrable_on J"
            unfolding J_def
            by (rule integrable_continuous_real)

          have i1: "integral {a..b} (λs. f (flow0 x s)) - integral {a..b} (λs. f (flow0 x0 s)) =
              integral {a..b} (λs. f (flow0 x s) - f (flow0 x0 s))"
            using J_in_existence_ivl[OF x_in_ball]
            apply (intro Henstock_Kurzweil_Integration.integral_diff[symmetric])
             by (auto intro!: continuous_intros existence_ivl_reverse)
          have i2:
            "integral {a..b} (λs. f (flow0 x s) - f (flow0 x0 s) - (f' (flow0 x0 s)) (vector_Dflow (x - x0) s)) =
              integral {a..b} (λs. f (flow0 x s) - f (flow0 x0 s)) -
              integral {a..b} (λs. f' (flow0 x0 s) (vector_Dflow (x - x0) s))"
            using J_in_existence_ivl[OF x_in_ball]
            by (intro Henstock_Kurzweil_Integration.integral_diff[OF Henstock_Kurzweil_Integration.integrable_diff])
              (auto intro!: continuous_intros existence_ivl_reverse)
          from ab_cases
          have "?g s = norm (integral {a..b} (λs'. f (Y (x - x0) s')) -
            integral {a..b} (λs'. f (flow0 x0 s')) -
            integral {a..b} (λs'. (f' (flow0 x0 s')) (vector_Dflow (x - x0) s')))"
          proof(safe)
            assume "a = 0" "b = s"
            hence "0  s" using s  {a..b} by simp

            text‹ Integral equations for flow0, Y and U. ›
            have flow0_integral_eq: "flow0 x0 s = x0 + ivl_integral 0 s (λs. f (flow0 x0 s))"
              by (rule flow_fixed_point[OF s_in_existence_ivl_x0])
            have Y_integral_eq: "flow0 x s = x0 + (x - x0) + ivl_integral 0 s (λs. f (Y (x - x0) s))"
              using flow_fixed_point 0  s s_in_existence_ivl2[OF z_in_ball] ball_in_X[OF z_in_ball]
              by (simp add:)
            have U_integral_eq: "vector_Dflow (x - x0) s = (x - x0) + ivl_integral 0 s (λs. vareq x0 s (vector_Dflow (x - x0) s))"
              unfolding vector_Dflow_def
              by (rule var.flow_fixed_point)
                (auto simp: 0  s x0_def varexivl_eq_exivl s_in_existence_ivl_x0)
            show "?g s = norm (integral {0..s} (λs'. f (Y (x - x0) s')) -
                integral {0..s} (λs'. f (flow0 x0 s')) -
                integral {0..s} (λs'. blinfun_apply (f' (flow0 x0 s')) (vector_Dflow (x - x0) s')))"
              using 0  s
              unfolding vareq_def[symmetric]
              by (simp add: flow0_integral_eq Y_integral_eq U_integral_eq ivl_integral_def)
          next
            assume "a = s" "b = 0"
            hence "s  0" using s  {a..b} by simp

            have flow0_integral_eq_left: "flow0 x0 s = x0 + ivl_integral 0 s (λs. f (flow0 x0 s))"
              by (rule flow_fixed_point[OF s_in_existence_ivl_x0])
            have Y_integral_eq_left: "Y (x - x0) s = x0 + (x - x0) + ivl_integral 0 s (λs. f (Y (x - x0) s))"
              using flow_fixed_point s  0 s_in_existence_ivl2[OF z_in_ball] ball_in_X[OF z_in_ball]
              by simp
            have U_integral_eq_left: "vector_Dflow (x - x0) s = (x - x0) + ivl_integral 0 s (λs. vareq x0 s (vector_Dflow (x - x0) s))"
              unfolding vector_Dflow_def
              by (rule var.flow_fixed_point)
                (auto simp: s  0 x0_def varexivl_eq_exivl s_in_existence_ivl_x0)

            have "?g s =
              norm (- integral {s..0} (λs'. f (Y (x - x0) s')) +
                integral {s..0} (λs'. f (flow0 x0 s')) +
                integral {s..0} (λs'. vareq x0 s' (vector_Dflow (x - x0) s')))"
              unfolding flow0_integral_eq_left Y_integral_eq_left U_integral_eq_left
              using s  0
              by (simp add: ivl_integral_def)
            also have "... = norm (integral {s..0} (λs'. f (Y (x - x0) s')) -
                integral {s..0} (λs'. f (flow0 x0 s')) -
                integral {s..0} (λs'. vareq x0 s' (vector_Dflow (x - x0) s')))"
              by (subst norm_minus_cancel[symmetric], simp)
            finally show "?g s =
              norm (integral {s..0} (λs'. f (Y (x - x0) s')) -
                integral {s..0} (λs'. f (flow0 x0 s')) -
                integral {s..0} (λs'. blinfun_apply (f' (flow0 x0 s')) (vector_Dflow (x - x0) s')))"
              unfolding vareq_def .
          qed
          also have "... =
            norm (integral {a..b} (λs. f (Y (x - x0) s) - f (flow0 x0 s) - (f' (flow0 x0 s)) (vector_Dflow (x - x0) s)))"
            by (simp add: i1 i2)
          also have "... 
            integral {a..b} (λs. norm (f (Y (x - x0) s) - f (flow0 x0 s) - f' (flow0 x0 s) (vector_Dflow (x - x0) s)))"
            using x_in_X J_in_existence_ivl_x J_in_existence {a..b}  J
            by (auto intro!: continuous_intros continuous_on_imp_absolutely_integrable_on
                existence_ivl_reverse)
          also have "... = integral {a..b}
              (λs. norm (f' (flow0 x0 s) (Y (x - x0) s - flow0 x0 s - vector_Dflow (x - x0) s) + R (flow0 x0 s) (Y (x - x0) s)))"
          proof (safe intro!: integral_spike[OF negligible_empty, simplified] arg_cong[where f=norm])
            fix s' assume "s'  {a..b}"
            show "f' (flow0 x0 s') (Y (x - x0) s' - flow0 x0 s' - vector_Dflow (x - x0) s') + R (flow0 x0 s') (Y (x - x0) s') =
              f (Y (x - x0) s') - f (flow0 x0 s') - f' (flow0 x0 s') (vector_Dflow (x - x0) s')"
              by (simp add: blinfun.diff_right Taylor_expansion(2)[of "flow0 x s'" "flow0 x0 s'"])
          qed
          also have "...  integral {a..b}
            (λs. norm (f' (flow0 x0 s) (Y (x - x0) s - flow0 x0 s - vector_Dflow (x - x0) s)) +
              norm (R (flow0 x0 s) (Y (x - x0) s)))"
            using J_in_existence_ivl[OF x_in_ball] norm_triangle_ineq
            using continuous_on J (λs. R (flow0 x0 s) (Y (x - x0) s))
            by (auto intro!: continuous_intros integral_le)
          also have "... =
            integral {a..b} (λs. norm (f' (flow0 x0 s) (Y (x - x0) s - flow0 x0 s - vector_Dflow (x - x0) s))) +
            integral {a..b} (λs. norm (R (flow0 x0 s) (Y (x - x0) s)))"
            using J_in_existence_ivl[OF x_in_ball]
            using continuous_on J (λs. R (flow0 x0 s) (Y (x - x0) s))
            by (auto intro!: continuous_intros Henstock_Kurzweil_Integration.integral_add)
          also have "...  N * integral {a..b} ?g + ?C" (is "?l1 + ?r1  _")
          proof(rule add_mono)
            have "?l1  integral {a..b} (λs. norm (f' (flow0 x0 s)) * norm (Y (x - x0) s - flow0 x0 s - vector_Dflow (x - x0) s))"
              using norm_blinfun J_in_existence_ivl[OF x_in_ball]
              by (auto intro!: continuous_intros integral_le)

            also have "...  integral {a..b} (λs. N * norm (Y (x - x0) s - flow0 x0 s - vector_Dflow (x - x0) s))"
              using J_in_existence_ivl[OF x_in_ball] N_ineq[OF {a..b}  J[THEN subsetD]]
              by (intro integral_le) (auto intro!: continuous_intros mult_right_mono)
              
            also have "... = N * integral {a..b} (λs. norm ((Y (x - x0) s - flow0 x0 s - vector_Dflow (x - x0) s)))"
              unfolding real_scaleR_def[symmetric]
              by(rule integral_cmul)
            finally show "?l1  N * integral {a..b} ?g" .
          next
            have "?r1  integral {a..b} (λs. e1 * dist (flow0 x0 s) (Y (x - x0) s))"
              using J_in_existence_ivl[OF x_in_ball] 0 < e_domain dist_flow0_Y2 0 < e_domain2
              by (intro integral_le)
                (force
                  intro!: continuous_intros Taylor_expansion(3) order_trans[OF infdist_le]
                   dest!: {a..b}  J[THEN subsetD]
                   intro: less_imp_le
                   simp: dist_commute H_def)+
            also have "...  integral {a..b} (λs. e1 * (dist x0 x * exp (K * ¦t¦)))"
              apply(rule integral_le)
              subgoal using J_in_existence_ivl[OF x_in_ball] by (force intro!: continuous_intros)
              subgoal by force
              subgoal by (force dest!: {a..b}  J[THEN subsetD]
                intro!: less_imp_le[OF 0 < e1] mult_left_mono[OF dist_flow0_Y])
              done
            also have "...  ?C"
              using s  J x_x0_dist 0 < e1 {a..b}  J 0 < ¦t¦ t0_def t1_def
              by (auto simp: integral_const_real J_def(1))
            finally show "?r1  ?C" .
          qed
          finally show ?thesis
            by simp
        qed
        have g_continuous: "continuous_on J ?g"
          using J_in_existence_ivl[OF x_in_ball] J_in_existence
          using J_def(1) U_continuous
          by (auto simp: J_def intro!: continuous_intros)
        note [continuous_intros] = continuous_on_subset[OF g_continuous]
        have C_gr_zero: "0 < ?C"
          using 0 < ¦t¦ 0 < e1 x_x0_dist(1)
          by (simp add: dist_commute)
        have "0  t  t  0" by auto
        then have "?g t  ?C * exp (N * ¦t¦)"
        proof
          assume "0  t"
          moreover
          have "continuous_on {0..t} (vector_Dflow (x - x0))"
            using U_continuous
            by (rule continuous_on_subset) (auto simp: J_def t0_def t1_def)
          then have "norm (Y (x - x0) t - flow0 x0 t - vector_Dflow (x - x0) t) 
            ¦t¦ * dist x0 x * exp (K * ¦t¦) * e1 * exp (N * t)"
            using t  J J_def t0  0 J_in_existence J_in_existence_ivl_x
            by (intro gronwall[OF g_bound _ _ C_gr_zero 0 < N 0  t order.refl])
               (auto intro!: continuous_intros simp: )
          ultimately show ?thesis by simp
        next
          assume "t  0"
          moreover
          have "continuous_on {t .. 0} (vector_Dflow (x - x0))"
            using U_continuous
            by (rule continuous_on_subset) (auto simp: J_def t0_def t1_def)
          then have "norm (Y (x - x0) t - flow0 x0 t - vector_Dflow (x - x0) t) 
            ¦t¦ * dist x0 x * exp (K * ¦t¦) * e1 * exp (- N * t)"
            using t  J J_def 0  t1 J_in_existence J_in_existence_ivl_x
            by (intro gronwall_left[OF g_bound _ _ C_gr_zero 0 < N order.refl t  0])
                (auto intro!: continuous_intros)
          ultimately show ?thesis
            by simp
        qed
        also have "... = dist x x0 * (¦t¦ * exp (K * ¦t¦) * e1 * exp (N * ¦t¦))"
          by (auto simp: dist_commute)
        also have "... < norm (x - x0) * e"
          unfolding e1_def
          using e' < e 0 < ¦t¦ 0 < e1 x_x0_dist(1)
          by (simp add: dist_norm)
        finally show "norm ((Y (x - x0) t - flow0 x0 t - vector_Dflow (x - x0) t) /R norm (x - x0)) < e"
          by (simp, metis x_x0_dist(1) dist_norm divide_inverse mult.commute pos_divide_less_eq)
      qed
    qed
  qed
qed

lemma local_lipschitz_A:
  "OT  existence_ivl0 x0  local_lipschitz OT (OS::('a L 'a) set) (λt. (oL) (vareq x0 t))"
  by (rule local_lipschitz_subset[OF _ _ subset_UNIV, where T="existence_ivl0 x0"])
     (auto simp: split_beta' vareq_def
      intro!: c1_implies_local_lipschitz[where f'="λ(t, x). comp3 (f' (flow0 x0 t))"]
        derivative_eq_intros blinfun_eqI ext
        continuous_intros flow_in_domain)

lemma total_derivative_ll_on_open:
  "ll_on_open (existence_ivl0 x0) (λt. blinfun_compose (vareq x0 t)) (UNIV::('a L 'a) set)"
  by standard (auto intro!: continuous_intros local_lipschitz_A[OF order_refl])

end

end

sublocale mvar: ll_on_open "existence_ivl0 x0" "λt. blinfun_compose (vareq x0 t)" "UNIV::('a L 'a) set" for x0
  by (rule total_derivative_ll_on_open)

lemma mvar_existence_ivl_eq_existence_ivl[simp]:― ‹TODO: unify with @{thm varexivl_eq_exivl}
  assumes "t  existence_ivl0 x0"
  shows "mvar.existence_ivl x0 t = (λ_. existence_ivl0 x0)"
proof (rule ext, rule mvar.existence_ivl_eq_domain)
  fix s t x
  assume s: "s  existence_ivl0 x0" and t: "t  existence_ivl0 x0"
  then have "{s .. t}  existence_ivl0 x0"
    by (meson atLeastAtMost_iff is_interval_1 is_interval_existence_ivl subsetI)
  then have "continuous_on {s .. t} (vareq x0)"
    by (auto intro!: continuous_intros)
  then have "compact (vareq x0 ` {s .. t})"
    using compact_Icc
    by (rule compact_continuous_image)
  then obtain B where B: "u. u  {s .. t}  norm (vareq x0 u)  B"
    by (force dest!: compact_imp_bounded simp: bounded_iff)
  show "M L. t{s .. t}. xUNIV. norm (vareq x0 t oL x)  M + L * norm x"
    unfolding o_def
    by (rule exI[where x=0], rule exI[where x=B])
      (auto intro!: order_trans[OF norm_blinfun_compose] mult_right_mono B)
qed (auto intro: assms)

lemma
  assumes "t  existence_ivl0 x0"
  shows "continuous_on (UNIV × existence_ivl0 x0) (λ(x, ta). mvar.flow x0 t x ta)"
proof -
  from mvar.flow_continuous_on_state_space[of x0 t, unfolded mvar_existence_ivl_eq_existence_ivl[OF assms]]
  show "continuous_on (UNIV × existence_ivl0 x0) (λ(x, ta). mvar.flow x0 t x ta)" .
qed

definition "Dflow x0 = mvar.flow x0 0 id_blinfun"

lemma var_eq_mvar:
  assumes "t0  existence_ivl0 x0"
  assumes "t  existence_ivl0 x0"
  shows "var.flow x0 t0 i t = mvar.flow x0 t0 id_blinfun t i"
  by (rule var.flow_unique)
     (auto intro!: assms derivative_eq_intros mvar.flow_has_derivative
       simp: varexivl_eq_exivl assms has_vector_derivative_def blinfun.bilinear_simps)

lemma Dflow_zero[simp]: "x  X  Dflow x 0 = 1L"
  unfolding Dflow_def
  by (subst mvar.flow_initial_time) auto


subsection ‹Differentiability of the flow0›

text U t›, i.e. the solution of the variational equation, is the space derivative at the initial
  value x0›. ›
lemma flow_dx_derivative:
assumes "t  existence_ivl0 x0"
shows "((λx0. flow0 x0 t) has_derivative (λz. vector_Dflow x0 z t)) (at x0)"
  unfolding has_derivative_at2
  using assms
  by (intro iffD1[OF LIM_equal proposition_17_6_weak[OF assms]] conjI[OF bounded_linear_vector_Dflow[OF assms]])
    (simp add: diff_diff_add inverse_eq_divide)

lemma flow_dx_derivative_blinfun:
assumes "t  existence_ivl0 x0"
shows "((λx. flow0 x t) has_derivative Blinfun (λz. vector_Dflow x0 z t)) (at x0)"
by (rule has_derivative_Blinfun[OF flow_dx_derivative[OF assms]])

definition "flowderiv x0 t = comp12 (Dflow x0 t) (blinfun_scaleR_left (f (flow0 x0 t)))"

lemma flowderiv_eq: "flowderiv x0 t (ξ1, ξ2) = (Dflow x0 t) ξ1 + ξ2 *R f (flow0 x0 t)"
  by (auto simp: flowderiv_def)

lemma W_continuous_on: "continuous_on (Sigma X existence_ivl0) (λ(x0, t). Dflow x0 t)"
  ― ‹TODO: somewhere here is hidden continuity wrt rhs of ODE, extract it!›
  unfolding continuous_on split_beta'
proof (safe intro!: tendstoI)
  fix e'::real and t x assume x: "x  X" and tx: "t  existence_ivl0 x" and e': "e' > 0"
  let ?S = "Sigma X existence_ivl0"

  have "(x, t)  ?S" using x tx by auto
  from open_prod_elim[OF open_state_space this]
  obtain OX OT where OXOT: "open OX" "open OT" "(x, t)  OX × OT" "OX × OT  ?S"
    by blast
  then obtain dx dt
  where dx: "dx > 0" "cball x dx  OX"
    and dt: "dt > 0" "cball t dt  OT"
    by (force simp: open_contains_cball)

  from OXOT dt dx have "cball t dt  existence_ivl0 x" "cball x dx  X"
    apply (auto simp: subset_iff)
    subgoal for ta
      apply (drule spec[where x=ta])
      apply (drule spec[where x=t])+
      apply auto
      done
    done

  have one_exivl: "mvar.existence_ivl x 0 = (λ_. existence_ivl0 x)"
    by (rule mvar_existence_ivl_eq_existence_ivl[OF existence_ivl_zero[OF x  X]])

  have *: "closed ({t .. 0}  {0 .. t})" "{t .. 0}  {0 .. t}  {}"
    by auto
  let ?T = "{t .. 0}  {0 .. t}  cball t dt"
  have "compact ?T"
    by (auto intro!: compact_Un)
  have "?T  existence_ivl0 x"
    by (intro Un_least ivl_subset_existence_ivl' ivl_subset_existence_ivl x  X
      t  existence_ivl0 x cball t dt  existence_ivl0 x)

  have "compact (mvar.flow x 0 id_blinfun ` ?T)"
    using ?T  _ x  X
      mvar_existence_ivl_eq_existence_ivl[OF existence_ivl_zero[OF x  X]]
    by (auto intro!: 0 < dx compact_continuous_image compact ?T
      continuous_on_subset[OF mvar.flow_continuous_on])

  let ?line = "mvar.flow x 0 id_blinfun ` ?T"
  let ?X = "{x. infdist x ?line  dx}"
  have "compact ?X"
    using ?T  _ x  X
      mvar_existence_ivl_eq_existence_ivl[OF existence_ivl_zero[OF x  X]]
    by (auto intro!: compact_infdist_le 0 < dx compact_continuous_image compact_Un
      continuous_on_subset[OF mvar.flow_continuous_on ])

  from mvar.local_lipschitz ?T  _
  have llc: "local_lipschitz ?T ?X (λt. (oL) (vareq x t))"
    by (rule local_lipschitz_subset) auto

  have cont: "xa. xa  ?X  continuous_on ?T (λt. vareq x t oL xa)"
    using ?T  _
    by (auto intro!: continuous_intros x  X)

  from local_lipschitz_compact_implies_lipschitz[OF llc compact ?X compact ?T cont]
  obtain K' where K': "ta. ta  ?T  K'-lipschitz_on ?X ((oL) (vareq x ta))"
    by blast
  define K where "K  abs K' + 1"
  have "K > 0"
    by (simp add: K_def)
  have K: "ta. ta  ?T  K-lipschitz_on ?X ((oL) (vareq x ta))"
    by (auto intro!: lipschitz_onI mult_right_mono order_trans[OF lipschitz_onD[OF K']] simp: K_def)

  have ex_ivlI: "y. y  cball x dx  ?T  existence_ivl0 y"
    using dx dt OXOT
    by (intro Un_least ivl_subset_existence_ivl' ivl_subset_existence_ivl; force)

  have cont: "continuous_on ((?T × ?X) × cball x dx) (λ((ta, xa), y). (vareq y ta oL xa))"
    using cball x dx  X ex_ivlI
    by (force intro!: continuous_intros simp: split_beta' )

  have "mvar.flow x 0 id_blinfun t  mvar.flow x 0 id_blinfun ` ({t..0}  {0..t}  cball t dt)"
    by auto
  then have mem: "(t, mvar.flow x 0 id_blinfun t, x)  ?T × ?X × cball x dx"
    by (auto simp: 0 < dx less_imp_le)

  define e where "e  min e' (dx / 2) / 2"
  have "e > 0" using e' > 0 by (auto simp: e_def 0 < dx)
  define d where "d  e * K / (exp (K * (abs t + abs dt + 1)) - 1)"
  have "d > 0" by (auto simp: d_def intro!: mult_pos_pos divide_pos_pos 0 < e K > 0)

  have cmpct: "compact ((?T × ?X) × cball x dx)" "compact (?T × ?X)"
    using compact ?T compact ?X
    by (auto intro!: compact_cball compact_Times)

  have compact_line: "compact ?line"
    using {t..0}  {0..t}  cball t dt  existence_ivl0 x one_exivl
    by (force intro!: compact_continuous_image compact ?T continuous_on_subset[OF mvar.flow_continuous_on] simp: x  X)

  from compact_uniformly_continuous[OF cont cmpct(1), unfolded uniformly_continuous_on_def,
      rule_format, OF 0 < d]
  obtain d' where d': "d' > 0"
    "ta xa xa' y. ta  ?T  xa  ?X  xa'cball x dx  ycball x dx  dist xa' y < d' 
      dist (vareq xa' ta oL xa) (vareq y ta oL xa) < d"
    by (auto simp: dist_prod_def)
  {
    fix y
    assume dxy: "dist x y < d'"
    assume "y  cball x dx"
    then have "y  X"
      using dx dt OXOT by force+

    have two_exivl: "mvar.existence_ivl y 0 = (λ_. existence_ivl0 y)"
      by (rule mvar_existence_ivl_eq_existence_ivl[OF existence_ivl_zero[OF y  X]])

    let ?X' = "x  ?line. ball x dx"
    have "open ?X'" by auto
    have "?X'  ?X"
      by (auto intro!: infdist_le2 simp: dist_commute)

    interpret oneR: ll_on_open "existence_ivl0 x" "(λt. (oL) (vareq x t))" ?X'
      by standard (auto intro!: x  X continuous_intros local_lipschitz_A[OF order_refl])
    interpret twoR: ll_on_open "existence_ivl0 y" "(λt. (oL) (vareq y t))" ?X'
      by standard (auto intro!: y  X continuous_intros local_lipschitz_A[OF order_refl])
    interpret both:
      two_ll_on_open "(λt. (oL) (vareq x t))" "existence_ivl0 x" "(λt. (oL) (vareq y t))" "existence_ivl0 y" ?X' ?T "id_blinfun" d K
    proof unfold_locales
      show "0 < K" by (simp add: 0 < K)
      show iv_defined: "0  {t..0}  {0..t}  cball t dt"
        by auto
      show "is_interval ({t..0}  {0..t}  cball t dt)"
        by (auto simp: is_interval_def dist_real_def)
      show "{t..0}  {0..t}  cball t dt  oneR.existence_ivl 0 id_blinfun"
        apply (rule oneR.maximal_existence_flow[where x="mvar.flow x 0 id_blinfun"])
        subgoal
          apply (rule solves_odeI)
          apply (rule has_vderiv_on_subset[OF solves_odeD(1)[OF mvar.flow_solves_ode[of 0 x id_blinfun]]])
          subgoal using x  X ?T  _ 0 < dx by simp
          subgoal by simp
          subgoal by (simp add: cball t dt  existence_ivl0 x ivl_subset_existence_ivl ivl_subset_existence_ivl' one_exivl tx)
          subgoal using dx by (auto; force)
          done
        subgoal by (simp add: x  X)
        subgoal by fact
        subgoal using iv_defined by blast
        subgoal using {t..0}  {0..t}  cball t dt  existence_ivl0 x by blast
        done
      fix s assume s: "s  ?T"
      then show "K-lipschitz_on ?X' ((oL) (vareq x s))"
        by (intro lipschitz_on_subset[OF K ?X'  ?X]) auto
      fix j assume j: "j  ?X'"
      show "norm ((vareq x s oL j) - (vareq y s oL j)) < d"
        unfolding dist_norm[symmetric]
        apply (rule d')
        subgoal by (rule s)
        subgoal using ?X'  ?X j ..
        subgoal using dx > 0 by simp
        subgoal using y  cball x dx by simp
        subgoal using dxy by simp
        done
    qed
    have less_e: "norm (Dflow x s - both.Y s) < e"
      if s: "s  ?T  twoR.existence_ivl 0 id_blinfun" for s
    proof -
      from s have s_less: "¦s¦ < ¦t¦ + ¦dt¦ + 1"
        by (auto simp: dist_real_def)
      note both.norm_X_Y_bound[rule_format, OF s]
      also have "d / K * (exp (K * ¦s¦) - 1) =
          e * ((exp (K * ¦s¦) - 1) / (exp (K * (¦t¦ + ¦dt¦ + 1)) - 1))"
        by (simp add: d_def)
      also have " < e * 1"
        by (rule mult_strict_left_mono[OF _ 0 < e])
           (simp add: add_nonneg_pos 0 < K 0 < e s_less)
      also have " = e" by simp
      also
      from s have s: "s  ?T" by simp
      have "both.flow0 s = Dflow x s"
        unfolding both.flow0_def Dflow_def
        apply (rule oneR.maximal_existence_flow[where K="?T"])
        subgoal
          apply (rule solves_odeI)
          apply (rule has_vderiv_on_subset[OF solves_odeD(1)[OF mvar.flow_solves_ode[of 0 x id_blinfun]]])
          subgoal using x  X 0 < dx by simp
          subgoal by simp
          subgoal by (simp add: cball t dt  existence_ivl0 x ivl_subset_existence_ivl ivl_subset_existence_ivl' one_exivl tx)
          subgoal using dx by (auto; force)
          done
        subgoal by (simp add: x  X)
        subgoal by (rule both.J_ivl)
        subgoal using both.t0_in_J by blast
        subgoal using {t..0}  {0..t}  cball t dt  existence_ivl0 x by blast
        subgoal using s by blast
        done
      finally show ?thesis .
    qed

    have "e < dx" using dx > 0 by (auto simp: e_def)

    let ?i = "{y. infdist y (mvar.flow x 0 id_blinfun ` ?T)  e}"
    have 1: "?i  (xmvar.flow x 0 id_blinfun ` ?T. ball x dx)"
    proof -
      have cl: "closed ?line" "?line  {}" using compact_line
        by (auto simp: compact_imp_closed)
      have "?i  (ymvar.flow x 0 id_blinfun ` ?T. cball y e)"
      proof safe
        fix x
        assume H: "infdist x ?line  e"
        from infdist_attains_inf[OF cl, of x]
        obtain y where "y  ?line" "infdist x ?line = dist x y" by auto
        then show "x  (x?line. cball x e)"
          using H
          by (auto simp: dist_commute)
      qed
      also have "  (x?line. ball x dx)"
        using e < dx
        by auto
      finally show ?thesis .
    qed
    have 2: "twoR.flow 0 id_blinfun s  ?i"
      if "s  ?T" "s  twoR.existence_ivl 0 id_blinfun" for s
    proof -
      from that have sT: "s  ?T  twoR.existence_ivl 0 id_blinfun"
        by force
      from less_e[OF this]
      have "dist (twoR.flow 0 id_blinfun s) (mvar.flow x 0 id_blinfun s)  e"
        unfolding Dflow_def both.Y_def dist_commute dist_norm by simp
      then show ?thesis
        using sT by (force intro: infdist_le2)
    qed
    have T_subset: "?T  twoR.existence_ivl 0 id_blinfun"
      apply (rule twoR.subset_mem_compact_implies_subset_existence_interval[
          where K="{x. infdist x ?line  e}"])
      subgoal using 0 < dt by force
      subgoal by (rule both.J_ivl)
      subgoal using y  cball x dx ex_ivlI by blast
      subgoal using both.F_iv_defined(2) by blast
      subgoal by (rule 2)
      subgoal using dt > 0 by (intro compact_infdist_le) (auto intro!: compact_line 0 < e)
      subgoal by (rule 1)
      done
    also have "twoR.existence_ivl 0 id_blinfun  existence_ivl0 y"
      by (rule twoR.existence_ivl_subset)
    finally have "?T  existence_ivl0 y" .
    have "norm (Dflow x s - Dflow y s) < e" if s: "s  ?T" for s
    proof -
      from s have "s  ?T  twoR.existence_ivl 0 id_blinfun" using T_subset by force
      from less_e[OF this] have "norm (Dflow x s - both.Y s) < e" .
      also have "mvar.flow y 0 id_blinfun s = twoR.flow 0 id_blinfun s"
        apply (rule mvar.maximal_existence_flow[where K="?T"])
        subgoal
          apply (rule solves_odeI)
          apply (rule has_vderiv_on_subset[OF solves_odeD(1)[OF twoR.flow_solves_ode[of 0 id_blinfun]]])
          subgoal using y  X by simp
          subgoal using both.F_iv_defined(2) by blast
          subgoal using T_subset by blast
          subgoal by simp
          done
        subgoal using y  X auto_ll_on_open.existence_ivl_zero auto_ll_on_open_axioms both.F_iv_defined(2) twoR.flow_initial_time by blast
        subgoal by (rule both.J_ivl)
        subgoal using both.t0_in_J by blast
        subgoal using {t..0}  {0..t}  cball t dt  existence_ivl0 y by blast
        subgoal using s by blast
        done
      then have "both.Y s = Dflow y s"
        unfolding both.Y_def Dflow_def
        by simp
      finally show ?thesis .
    qed
  } note cont_data = this
  have "F (y, s) in at (x, t) within ?S. dist x y < d'"
    unfolding at_within_open[OF (x, t)  ?S open_state_space] UNIV_Times_UNIV[symmetric]
    using d' > 0
    by (intro eventually_at_Pair_within_TimesI1)
      (auto simp: eventually_at less_imp_le dist_commute)
  moreover
  have "F (y, s) in at (x, t) within ?S. y  cball x dx"
    unfolding at_within_open[OF (x, t)  ?S open_state_space] UNIV_Times_UNIV[symmetric]
    using dx > 0
    by (intro eventually_at_Pair_within_TimesI1)
      (auto simp: eventually_at less_imp_le dist_commute)
  moreover
  have "F (y, s) in at (x, t) within ?S. s  ?T"
    unfolding at_within_open[OF (x, t)  ?S open_state_space] UNIV_Times_UNIV[symmetric]
    using dt > 0
    by (intro eventually_at_Pair_within_TimesI2)
      (auto simp: eventually_at less_imp_le dist_commute)
  moreover
  have "0  existence_ivl0 x" by (simp add: x  X)
  have "F y in at t within existence_ivl0 x. dist (mvar.flow x 0 id_blinfun y) (mvar.flow x 0 id_blinfun t) < e"
    using mvar.flow_continuous_on[of x 0 id_blinfun]
    using 0 < e tx
    by (auto simp add: continuous_on one_exivl dest!: tendstoD)
  then have "F (y, s) in at (x, t) within ?S. dist (Dflow x s) (Dflow x t) < e"
    using 0 < e
    unfolding at_within_open[OF (x, t)  ?S open_state_space] UNIV_Times_UNIV[symmetric] Dflow_def
    by (intro eventually_at_Pair_within_TimesI2)
      (auto simp: at_within_open[OF tx open_existence_ivl])
  ultimately
  have "F (y, s) in at (x, t) within ?S. dist (Dflow y s) (Dflow x t) < e'"
    apply eventually_elim
  proof (safe del: UnE, goal_cases)
    case (1 y s)
    have "dist (Dflow y s) (Dflow x t)  dist (Dflow y s) (Dflow x s) + dist (Dflow x s) (Dflow x t)"
      by (rule dist_triangle)
    also
    have "dist (Dflow x s) (Dflow x t) < e"
      by (rule 1)
    also have "dist (Dflow y s) (Dflow x s) < e"
      unfolding dist_norm norm_minus_commute
      using 1
      by (intro cont_data)
    also have "e + e  e'" by (simp add: e_def)
    finally show "dist (Dflow y s) (Dflow x t) < e'" by arith
  qed
  then show "F ys in at (x, t) within ?S. dist (Dflow (fst ys) (snd ys)) (Dflow (fst (x, t)) (snd (x, t))) < e'"
    by (simp add: split_beta')
qed

lemma W_continuous_on_comp[continuous_intros]:
  assumes h: "continuous_on S h" and g: "continuous_on S g"
  shows "(s. s  S  h s  X)  (s. s  S  g s  existence_ivl0 (h s)) 
    continuous_on S (λs. Dflow (h s) (g s))"
  using continuous_on_compose[OF continuous_on_Pair[OF h g] continuous_on_subset[OF W_continuous_on]]
  by auto

lemma f_flow_continuous_on: "continuous_on (Sigma X existence_ivl0) (λ(x0, t). f (flow0 x0 t))"
  using flow_continuous_on_state_space
  by (auto intro!: continuous_on_f flow_in_domain simp: split_beta')

lemma
  flow_has_space_derivative:
  assumes "t  existence_ivl0 x0"
  shows "((λx0. flow0 x0 t) has_derivative Dflow x0 t) (at x0)"
  by (rule flow_dx_derivative_blinfun[THEN has_derivative_eq_rhs])
    (simp_all add: var_eq_mvar assms blinfun.blinfun_apply_inverse Dflow_def vector_Dflow_def
      mem_existence_ivl_iv_defined[OF assms])

lemma
  flow_has_flowderiv:
  assumes "t  existence_ivl0 x0"
  shows "((λ(x0, t). flow0 x0 t) has_derivative flowderiv x0 t) (at (x0, t) within S)"
proof -
  have Sigma: "(x0, t)  Sigma X existence_ivl0"
    using assms by auto
  from open_state_space assms obtain e' where e': "e' > 0" "ball (x0, t) e'  Sigma X existence_ivl0"
    by (force simp: open_contains_ball)
  define e where "e = e' / sqrt 2"
  have "0 < e" using e' by (auto simp: e_def)
  have "ball x0 e × ball t e  ball (x0, t) e'"
    by (auto simp: dist_prod_def real_sqrt_sum_squares_less e_def)
  also note e'(2)
  finally have subs: "ball x0 e × ball t e  Sigma X existence_ivl0" .


  have d1: "((λx0. flow0 x0 s) has_derivative blinfun_apply (Dflow y s)) (at y within ball x0 e)"
    if "y  ball x0 e" "s  ball t e" for y s
    using subs that
    by (subst at_within_open; force intro!: flow_has_space_derivative)
  have d2: "(flow0 y has_derivative blinfun_apply (blinfun_scaleR_left (f (flow0 y s)))) (at s within ball t e)"
    if "y  ball x0 e" "s  ball t e" for y s
    using subs that
    unfolding has_vector_derivative_eq_has_derivative_blinfun[symmetric]
    by (subst at_within_open; force intro!: flow_has_vector_derivative)
  have "((λ(x0, t). flow0 x0 t) has_derivative flowderiv x0 t) (at (x0, t) within ball x0 e × ball t e)"
    using subs
    unfolding UNIV_Times_UNIV[symmetric]
    by (intro has_derivative_partialsI[OF d1 d2, THEN has_derivative_eq_rhs])
       (auto intro!: 0 < e continuous_intros flow_in_domain
          continuous_on_imp_continuous_within[where s="Sigma X existence_ivl0"]
          assms
        simp: flowderiv_def split_beta' flow0_defined assms mem_ball)
  then have "((λ(x0, t). flow0 x0 t) has_derivative flowderiv x0 t) (at (x0, t) within Sigma X existence_ivl0)"
    by (auto simp: at_within_open[OF _ open_state_space] at_within_open[OF _ open_Times] assms 0 < e
        mem_existence_ivl_iv_defined[OF assms])
  then show ?thesis unfolding at_within_open[OF Sigma open_state_space]
    by (rule has_derivative_at_withinI)
qed

lemma flow0_comp_has_derivative:
  assumes h: "h s  existence_ivl0 (g s)"
  assumes [derivative_intros]: "(g has_derivative g') (at s within S)"
  assumes [derivative_intros]: "(h has_derivative h') (at s within S)"
  shows "((λx. flow0 (g x) (h x)) has_derivative (λx. blinfun_apply (flowderiv (g s) (h s)) (g' x, h' x)))
     (at s within S)"
  by (rule has_derivative_compose[where f="λx. (g x, h x)" and s=S,
        OF _ flow_has_flowderiv[OF h], simplified])
    (auto intro!: derivative_eq_intros)

lemma flowderiv_continuous_on: "continuous_on (Sigma X existence_ivl0) (λ(x0, t). flowderiv x0 t)"
  unfolding flowderiv_def split_beta'
  by (subst blinfun_of_matrix_works[where f="comp12 (Dflow (fst x) (snd x))
            (blinfun_scaleR_left (f (flow0 (fst x) (snd x))))" for x, symmetric])
    (auto intro!: continuous_intros flow_in_domain)

lemma flowderiv_continuous_on_comp[continuous_intros]:
  assumes "continuous_on S x"
  assumes "continuous_on S t"
  assumes "s. s  S  x s  X" "s. s  S  t s  existence_ivl0 (x s)"
  shows "continuous_on S (λxa. flowderiv (x xa) (t xa))"
  by (rule continuous_on_compose2[OF flowderiv_continuous_on, where f="λs. (x s, t s)",
        unfolded split_beta' fst_conv snd_conv])
    (auto intro!: continuous_intros assms)

lemmas [intro] = flow_in_domain

lemma vareq_trans: "t0  existence_ivl0 x0  t  existence_ivl0 (flow0 x0 t0) 
  vareq (flow0 x0 t0) t = vareq x0 (t0 + t)"
  by (auto simp: vareq_def flow_trans)

lemma diff_existence_ivl_trans:
  "t0  existence_ivl0 x0  t  existence_ivl0 x0  t - t0  existence_ivl0 (flow0 x0 t0)" for t
  by (metis (no_types, opaque_lifting) add.left_neutral diff_add_eq
      local.existence_ivl_reverse local.existence_ivl_trans local.flows_reverse)

lemma has_vderiv_on_blinfun_compose_right[derivative_intros]:
  assumes "(g has_vderiv_on g') T"
  assumes "x. x  T  gd' x = g' x oL d"
  shows "((λx. g x oL d) has_vderiv_on gd') T"
  using assms
  by (auto simp: has_vderiv_on_def has_vector_derivative_def blinfun_ext blinfun.bilinear_simps
      intro!: derivative_eq_intros ext)

lemma has_vderiv_on_blinfun_compose_left[derivative_intros]:
  assumes "(g has_vderiv_on g') T"
  assumes "x. x  T  gd' x = d oL g' x"
  shows "((λx. d oL g x) has_vderiv_on gd') T"
  using assms
  by (auto simp: has_vderiv_on_def has_vector_derivative_def blinfun_ext blinfun.bilinear_simps
      intro!: derivative_eq_intros ext)

lemma mvar_flow_shift:
  assumes "t0  existence_ivl0 x0" "t1  existence_ivl0 x0"
  shows "mvar.flow x0 t0 d t1 = Dflow (flow0 x0 t0) (t1 - t0) oL d"
proof -
  have "mvar.flow x0 t0 d t1 = mvar.flow x0 t0 d (t0 + (t1 - t0))"
    by simp
  also have " = mvar.flow x0 t0 (mvar.flow x0 t0 d t0) t1"
    by (subst mvar.flow_trans) (auto simp add: assms)
  also have " = Dflow (flow0 x0 t0) (t1 - t0) oL d"
    apply (rule mvar.flow_unique_on)
       apply (auto simp add: assms mvar.flow_initial_time_if blinfun_ext Dflow_def
        intro!: derivative_intros derivative_eq_intros)
      apply (auto simp: assms has_vderiv_on_open has_vector_derivative_def
        intro!: derivative_eq_intros blinfun_eqI)
     apply (subst mvar_existence_ivl_eq_existence_ivl)
    by (auto simp add: vareq_trans assms diff_existence_ivl_trans)
  finally show ?thesis .
qed

lemma Dflow_trans:
  assumes "h  existence_ivl0 x0"
  assumes "i  existence_ivl0 (flow0 x0 h)"
  shows "Dflow x0 (h + i) = Dflow (flow0 x0 h) i oL (Dflow x0 h)"
proof -
  have [intro, simp]: "h + i  existence_ivl0 x0" "i + h  existence_ivl0 x0" "x0  X"
    using assms
    by (auto simp add: add.commute existence_ivl_trans)
  show ?thesis
    unfolding Dflow_def
    apply (subst mvar.flow_trans[where s=h and t=i])
    subgoal by (auto simp: assms)
    subgoal by (auto simp: assms)
    by (subst mvar_flow_shift) (auto simp: assms Dflow_def )
qed

lemma Dflow_trans_apply:
  assumes "h  existence_ivl0 x0"
  assumes "i  existence_ivl0 (flow0 x0 h)"
  shows "Dflow x0 (h + i) d0 = Dflow (flow0 x0 h) i (Dflow x0 h d0)"
proof -
  have [intro, simp]: "h + i  existence_ivl0 x0" "i + h  existence_ivl0 x0" "x0  X"
    using assms
    by (auto simp add: add.commute existence_ivl_trans)
  show ?thesis
    unfolding Dflow_def
    apply (subst mvar.flow_trans[where s=h and t=i])
    subgoal by (auto simp: assms)
    subgoal by (auto simp: assms)
    by (subst mvar_flow_shift) (auto simp: assms Dflow_def )
qed


end ― ‹@{thm c1_on_open_euclidean_anchor}

end