Theory 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 ("1⇩L")
lemma blinfun_inverse_left:
fixes f::"'a::euclidean_space ⇒⇩L 'a" and f'
shows "f o⇩L f' = 1⇩L ⟷ f' o⇩L f = 1⇩L"
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 o⇩L 1⇩L = x"
and blinfun_compose_1_right[simp]: "1⇩L o⇩L 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
integrable_on_refl integrable_on_refl_ivl integrable_on_refl_closed_segment
integrable_const integrable_const_ivl integrable_const_ivl_closed_segment
ident_integrable_on integrable_ident_ivl integrable_ident_cbox
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 ⟷ (∃x∈existence_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
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
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
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
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)"
and "P (t + s - s) = P t"
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
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 o⇩L 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
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
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}. ∀x∈UNIV. 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:
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"
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 ≡ {x∈X. 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¦))"
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 ⟹
(∀t∈J. 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. (o⇩L) (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]:
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}. ∀x∈UNIV. norm (vareq x0 t o⇩L 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 = 1⇩L"
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)"
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. (o⇩L) (vareq x t))"
by (rule local_lipschitz_subset) auto
have cont: "⋀xa. xa ∈ ?X ⟹ continuous_on ?T (λt. vareq x t o⇩L 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 ((o⇩L) (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 ((o⇩L) (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 o⇩L 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 ⟹ y∈cball x dx ⟹ dist xa' y < d' ⟹
dist (vareq xa' ta o⇩L xa) (vareq y ta o⇩L 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. (o⇩L) (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. (o⇩L) (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. (o⇩L) (vareq x t))" "existence_ivl0 x" "(λt. (o⇩L) (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' ((o⇩L) (vareq x s))"
by (intro lipschitz_on_subset[OF K ‹?X' ⊆ ?X›]) auto
fix j assume j: "j ∈ ?X'"
show "norm ((vareq x s o⇩L j) - (vareq y s o⇩L 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 ⊆ (⋃x∈mvar.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 ⊆ (⋃y∈mvar.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 o⇩L d"
shows "((λx. g x o⇩L 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 o⇩L g' x"
shows "((λx. d o⇩L 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) o⇩L 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) o⇩L 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 o⇩L (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
end