Theory Initial_Value_Problem
section‹Initial Value Problems›
theory Initial_Value_Problem
imports
"../ODE_Auxiliarities"
"../Library/Interval_Integral_HK"
"../Library/Gronwall"
begin
lemma clamp_le[simp]: "x ≤ a ⟹ clamp a b x = a" for x::"'a::ordered_euclidean_space"
by (auto simp: clamp_def eucl_le[where 'a='a] intro!: euclidean_eqI[where 'a='a])
lemma clamp_ge[simp]: "a ≤ b ⟹ b ≤ x ⟹ clamp a b x = b" for x::"'a::ordered_euclidean_space"
by (force simp: clamp_def eucl_le[where 'a='a] not_le not_less intro!: euclidean_eqI[where 'a='a])
abbreviation cfuncset :: "'a::topological_space set ⇒ 'b::metric_space set ⇒ ('a ⇒⇩C 'b) set"
(infixr "→⇩C" 60)
where "A →⇩C B ≡ PiC A (λ_. B)"
lemma closed_segment_translation_zero: "z ∈ {z + a--z + b} ⟷ 0 ∈ {a -- b}"
by (metis add.right_neutral closed_segment_translation_eq)
lemma closed_segment_subset_interval: "is_interval T ⟹ a ∈ T ⟹ b ∈ T ⟹ closed_segment a b ⊆ T"
by (rule closed_segment_subset) (auto intro!: closed_segment_subset is_interval_convex)
definition half_open_segment::"'a::real_vector ⇒ 'a ⇒ 'a set" ("(1{_--<_})")
where "half_open_segment a b = {a -- b} - {b}"
lemma half_open_segment_real:
fixes a b::real
shows "{a --< b} = (if a ≤ b then {a ..< b} else {b <.. a})"
by (auto simp: half_open_segment_def closed_segment_eq_real_ivl)
lemma closure_half_open_segment:
fixes a b::real
shows "closure {a --< b} = (if a = b then {} else {a -- b})"
unfolding closed_segment_eq_real_ivl if_distrib half_open_segment_real
unfolding if_distribR
by simp
lemma half_open_segment_subset[intro, simp]:
"{t0--<t1} ⊆ {t0 -- t1}"
"x ∈ {t0--<t1} ⟹ x ∈ {t0 -- t1}"
by (auto simp: half_open_segment_def)
lemma half_open_segment_closed_segmentI:
"t ∈ {t0 -- t1} ⟹ t ≠ t1 ⟹ t ∈ {t0 --< t1}"
by (auto simp: half_open_segment_def)
lemma islimpt_half_open_segment:
fixes t0 t1 s::real
assumes "t0 ≠ t1" "s ∈ {t0--t1}"
shows "s islimpt {t0--<t1}"
proof -
have "s islimpt {t0..<t1}" if "t0 ≤ s" "s ≤ t1" for s
proof -
have *: "{t0..<t1} - {s} = {t0..<s} ∪ {s<..<t1}"
using that by auto
show ?thesis
using that ‹t0 ≠ t1› *
by (cases "t0 = s") (auto simp: islimpt_in_closure)
qed
moreover have "s islimpt {t1<..t0}" if "t1 ≤ s" "s ≤ t0" for s
proof -
have *: "{t1<..t0} - {s} = {t1<..<s} ∪ {s<..t0}"
using that by auto
show ?thesis
using that ‹t0 ≠ t1› *
by (cases "t0 = s") (auto simp: islimpt_in_closure)
qed
ultimately show ?thesis using assms
by (auto simp: half_open_segment_real closed_segment_eq_real_ivl)
qed
lemma
mem_half_open_segment_eventually_in_closed_segment:
fixes t::real
assumes "t ∈ {t0--<t1'}"
shows "∀⇩F t1' in at t1' within {t0--<t1'}. t ∈ {t0--t1'}"
unfolding half_open_segment_real
proof (split if_split, safe)
assume le: "t0 ≤ t1'"
with assms have t: "t0 ≤ t" "t < t1'"
by (auto simp: half_open_segment_real)
then have "∀⇩F t1' in at t1' within {t0..<t1'}. t0 ≤ t"
by simp
moreover
from tendsto_ident_at ‹t < t1'›
have "∀⇩F t1' in at t1' within {t0..<t1'}. t < t1'"
by (rule order_tendstoD)
ultimately show "∀⇩F t1' in at t1' within {t0..<t1'}. t ∈ {t0--t1'}"
by eventually_elim (auto simp add: closed_segment_eq_real_ivl)
next
assume le: "¬ t0 ≤ t1'"
with assms have t: "t ≤ t0" "t1' < t"
by (auto simp: half_open_segment_real)
then have "∀⇩F t1' in at t1' within {t1'<..t0}. t ≤ t0"
by simp
moreover
from tendsto_ident_at ‹t1' < t›
have "∀⇩F t1' in at t1' within {t1'<..t0}. t1' < t"
by (rule order_tendstoD)
ultimately show "∀⇩F t1' in at t1' within {t1'<..t0}. t ∈ {t0--t1'}"
by eventually_elim (auto simp add: closed_segment_eq_real_ivl)
qed
lemma closed_segment_half_open_segment_subsetI:
fixes x::real shows "x ∈ {t0--<t1} ⟹ {t0--x} ⊆ {t0--<t1}"
by (auto simp: half_open_segment_real closed_segment_eq_real_ivl split: if_split_asm)
lemma dist_component_le:
fixes x y::"'a::euclidean_space"
assumes "i ∈ Basis"
shows "dist (x ∙ i) (y ∙ i) ≤ dist x y"
using assms
by (auto simp: euclidean_dist_l2[of x y] intro: member_le_L2_set)
lemma sum_inner_Basis_one: "i ∈ Basis ⟹ (∑x∈Basis. x ∙ i) = 1"
by (subst sum.mono_neutral_right[where S="{i}"])
(auto simp: inner_not_same_Basis)
lemma cball_in_cbox:
fixes y::"'a::euclidean_space"
shows "cball y r ⊆ cbox (y - r *⇩R One) (y + r *⇩R One)"
unfolding scaleR_sum_right interval_cbox cbox_def
proof safe
fix x i::'a assume "i ∈ Basis" "x ∈ cball y r"
with dist_component_le[OF ‹i ∈ Basis›, of y x]
have "dist (y ∙ i) (x ∙ i) ≤ r" by (simp add: mem_cball)
thus "(y - sum ((*⇩R) r) Basis) ∙ i ≤ x ∙ i"
"x ∙ i ≤ (y + sum ((*⇩R) r) Basis) ∙ i"
by (auto simp add: inner_diff_left inner_add_left inner_sum_left
sum_distrib_left[symmetric] sum_inner_Basis_one ‹i∈Basis› dist_real_def)
qed
lemma centered_cbox_in_cball:
shows "cbox (- r *⇩R One) (r *⇩R One::'a::euclidean_space) ⊆
cball 0 (sqrt(DIM('a)) * r)"
proof
fix x::'a
have "norm x ≤ sqrt(DIM('a)) * infnorm x"
by (rule norm_le_infnorm)
also
assume "x ∈ cbox (- r *⇩R One) (r *⇩R One)"
hence "infnorm x ≤ r"
by (auto simp: infnorm_def mem_box intro!: cSup_least)
finally show "x ∈ cball 0 (sqrt(DIM('a)) * r)"
by (auto simp: dist_norm mult_left_mono mem_cball)
qed
subsection ‹Solutions of IVPs \label{sec:solutions}›
definition
solves_ode :: "(real ⇒ 'a::real_normed_vector) ⇒ (real ⇒ 'a ⇒ 'a) ⇒ real set ⇒ 'a set ⇒ bool"
(infix "(solves'_ode)" 50)
where
"(y solves_ode f) T X ⟷ (y has_vderiv_on (λt. f t (y t))) T ∧ y ∈ T → X"
lemma solves_odeI:
assumes solves_ode_vderivD: "(y has_vderiv_on (λt. f t (y t))) T"
and solves_ode_domainD: "⋀t. t ∈ T ⟹ y t ∈ X"
shows "(y solves_ode f) T X"
using assms
by (auto simp: solves_ode_def)
lemma solves_odeD:
assumes "(y solves_ode f) T X"
shows solves_ode_vderivD: "(y has_vderiv_on (λt. f t (y t))) T"
and solves_ode_domainD: "⋀t. t ∈ T ⟹ y t ∈ X"
using assms
by (auto simp: solves_ode_def)
lemma solves_ode_continuous_on: "(y solves_ode f) T X ⟹ continuous_on T y"
by (auto intro!: vderiv_on_continuous_on simp: solves_ode_def)
lemma solves_ode_congI:
assumes "(x solves_ode f) T X"
assumes "⋀t. t ∈ T ⟹ x t = y t"
assumes "⋀t. t ∈ T ⟹ f t (x t) = g t (x t)"
assumes "T = S" "X = Y"
shows "(y solves_ode g) S Y"
using assms
by (auto simp: solves_ode_def Pi_iff)
lemma solves_ode_cong[cong]:
assumes "⋀t. t ∈ T ⟹ x t = y t"
assumes "⋀t. t ∈ T ⟹ f t (x t) = g t (x t)"
assumes "T = S" "X = Y"
shows "(x solves_ode f) T X ⟷ (y solves_ode g) S Y"
using assms
by (auto simp: solves_ode_def Pi_iff)
lemma solves_ode_on_subset:
assumes "(x solves_ode f) S Y"
assumes "T ⊆ S" "Y ⊆ X"
shows "(x solves_ode f) T X"
using assms
by (auto simp: solves_ode_def has_vderiv_on_subset)
lemma preflect_solution:
assumes "t0 ∈ T"
assumes sol: "((λt. x (preflect t0 t)) solves_ode (λt x. - f (preflect t0 t) x)) (preflect t0 ` T) X"
shows "(x solves_ode f) T X"
proof (rule solves_odeI)
from solves_odeD[OF sol]
have xm_deriv: "(x o preflect t0 has_vderiv_on (λt. - f (preflect t0 t) (x (preflect t0 t)))) (preflect t0 ` T)"
and xm_mem: "t ∈ preflect t0 ` T ⟹ x (preflect t0 t) ∈ X" for t
by simp_all
have "(x o preflect t0 o preflect t0 has_vderiv_on (λt. f t (x t))) T"
apply (rule has_vderiv_on_eq_rhs)
apply (rule has_vderiv_on_compose)
apply (rule xm_deriv)
apply (auto simp: preflect_def intro!: derivative_intros)
done
then show "(x has_vderiv_on (λt. f t (x t))) T"
by (simp add: preflect_def)
show "x t ∈ X" if "t ∈ T" for t
using that xm_mem[of "preflect t0 t"]
by (auto simp: preflect_def)
qed
lemma solution_preflect:
assumes "t0 ∈ T"
assumes sol: "(x solves_ode f) T X"
shows "((λt. x (preflect t0 t)) solves_ode (λt x. - f (preflect t0 t) x)) (preflect t0 ` T) X"
using sol ‹t0 ∈ T›
by (simp_all add: preflect_def image_image preflect_solution[of t0])
lemma solution_eq_preflect_solution:
assumes "t0 ∈ T"
shows "(x solves_ode f) T X ⟷ ((λt. x (preflect t0 t)) solves_ode (λt x. - f (preflect t0 t) x)) (preflect t0 ` T) X"
using solution_preflect[OF ‹t0 ∈ T›] preflect_solution[OF ‹t0 ∈ T›]
by blast
lemma shift_autonomous_solution:
assumes sol: "(x solves_ode f) T X"
assumes auto: "⋀s t. s ∈ T ⟹ f s (x s) = f t (x s)"
shows "((λt. x (t + t0)) solves_ode f) ((λt. t - t0) ` T) X"
using solves_odeD[OF sol]
apply (intro solves_odeI)
apply (rule has_vderiv_on_compose'[of x, THEN has_vderiv_on_eq_rhs])
apply (auto simp: image_image intro!: auto derivative_intros)
done
lemma solves_ode_singleton: "y t0 ∈ X ⟹ (y solves_ode f) {t0} X"
by (auto intro!: solves_odeI has_vderiv_on_singleton)
subsubsection‹Connecting solutions›
text‹\label{sec:combining-solutions}›
lemma connection_solves_ode:
assumes x: "(x solves_ode f) T X"
assumes y: "(y solves_ode g) S Y"
assumes conn_T: "closure S ∩ closure T ⊆ T"
assumes conn_S: "closure S ∩ closure T ⊆ S"
assumes conn_x: "⋀t. t ∈ closure S ⟹ t ∈ closure T ⟹ x t = y t"
assumes conn_f: "⋀t. t ∈ closure S ⟹ t ∈ closure T ⟹ f t (y t) = g t (y t)"
shows "((λt. if t ∈ T then x t else y t) solves_ode (λt. if t ∈ T then f t else g t)) (T ∪ S) (X ∪ Y)"
proof (rule solves_odeI)
from solves_odeD(2)[OF x] solves_odeD(2)[OF y]
show "t ∈ T ∪ S ⟹ (if t ∈ T then x t else y t) ∈ X ∪ Y" for t
by auto
show "((λt. if t ∈ T then x t else y t) has_vderiv_on (λt. (if t ∈ T then f t else g t) (if t ∈ T then x t else y t))) (T ∪ S)"
apply (rule has_vderiv_on_If[OF refl, THEN has_vderiv_on_eq_rhs])
unfolding Un_absorb2[OF conn_T] Un_absorb2[OF conn_S]
apply (rule solves_odeD(1)[OF x])
apply (rule solves_odeD(1)[OF y])
apply (simp_all add: conn_T conn_S Un_absorb2 conn_x conn_f)
done
qed
lemma
solves_ode_subset_range:
assumes x: "(x solves_ode f) T X"
assumes s: "x ` T ⊆ Y"
shows "(x solves_ode f) T Y"
using assms
by (auto intro!: solves_odeI dest!: solves_odeD)
subsection ‹unique solution with initial value›
definition
usolves_ode_from :: "(real ⇒ 'a::real_normed_vector) ⇒ (real ⇒ 'a ⇒ 'a) ⇒ real ⇒ real set ⇒ 'a set ⇒ bool"
("((_) usolves'_ode (_) from (_))" [10, 10, 10] 10)
where
"(y usolves_ode f from t0) T X ⟷ (y solves_ode f) T X ∧ t0 ∈ T ∧ is_interval T ∧
(∀z T'. t0 ∈ T' ∧ is_interval T' ∧ T' ⊆ T ∧ (z solves_ode f) T' X ⟶ z t0 = y t0 ⟶ (∀t ∈ T'. z t = y t))"
text ‹uniqueness of solution can depend on domain ‹X›:›
lemma
"((λ_. 0::real) usolves_ode (λ_. sqrt) from 0) {0..} {0}"
"((λt. t⇧2 / 4) solves_ode (λ_. sqrt)) {0..} {0..}"
"(λt. t⇧2 / 4) 0 = (λ_. 0::real) 0"
by (auto intro!: derivative_eq_intros
simp: has_vderiv_on_def has_vector_derivative_def usolves_ode_from_def solves_ode_def
is_interval_ci real_sqrt_divide)
text ‹TODO: show that if solution stays in interior, then domain can be enlarged! (?)›
lemma usolves_odeD:
assumes "(y usolves_ode f from t0) T X"
shows "(y solves_ode f) T X"
and "t0 ∈ T"
and "is_interval T"
and "⋀z T' t. t0 ∈ T' ⟹ is_interval T' ⟹ T' ⊆ T ⟹(z solves_ode f) T' X ⟹ z t0 = y t0 ⟹ t ∈ T' ⟹ z t = y t"
using assms
unfolding usolves_ode_from_def
by blast+
lemma usolves_ode_rawI:
assumes "(y solves_ode f) T X" "t0 ∈ T" "is_interval T"
assumes "⋀z T' t. t0 ∈ T' ⟹ is_interval T' ⟹ T' ⊆ T ⟹ (z solves_ode f) T' X ⟹ z t0 = y t0 ⟹ t ∈ T' ⟹ z t = y t"
shows "(y usolves_ode f from t0) T X"
using assms
unfolding usolves_ode_from_def
by blast
lemma usolves_odeI:
assumes "(y solves_ode f) T X" "t0 ∈ T" "is_interval T"
assumes usol: "⋀z t. {t0 -- t} ⊆ T ⟹ (z solves_ode f) {t0 -- t} X ⟹ z t0 = y t0 ⟹ z t = y t"
shows "(y usolves_ode f from t0) T X"
proof (rule usolves_ode_rawI; fact?)
fix z T' t
assume T': "t0 ∈ T'" "is_interval T'" "T' ⊆ T"
and z: "(z solves_ode f) T' X" and iv: "z t0 = y t0" and t: "t ∈ T'"
have subset_T': "{t0 -- t} ⊆ T'"
by (rule closed_segment_subset_interval; fact)
with z have sol_cs: "(z solves_ode f) {t0 -- t} X"
by (rule solves_ode_on_subset[OF _ _ order_refl])
from subset_T' have subset_T: "{t0 -- t} ⊆ T"
using ‹T' ⊆ T› by simp
from usol[OF subset_T sol_cs iv]
show "z t = y t" by simp
qed
lemma is_interval_singleton[intro,simp]: "is_interval {t0}"
by (auto simp: is_interval_def intro!: euclidean_eqI[where 'a='a])
lemma usolves_ode_singleton: "x t0 ∈ X ⟹ (x usolves_ode f from t0) {t0} X"
by (auto intro!: usolves_odeI solves_ode_singleton)
lemma usolves_ode_congI:
assumes x: "(x usolves_ode f from t0) T X"
assumes "⋀t. t ∈ T ⟹ x t = y t"
assumes "⋀t y. t ∈ T ⟹ y ∈ X ⟹ f t y = g t y"
assumes "t0 = s0"
assumes "T = S"
assumes "X = Y"
shows "(y usolves_ode g from s0) S Y"
proof (rule usolves_ode_rawI)
from assms x have "(y solves_ode f) S Y"
by (auto simp add: usolves_ode_from_def)
then show "(y solves_ode g) S Y"
by (rule solves_ode_congI) (use assms in ‹auto simp: usolves_ode_from_def dest!: solves_ode_domainD›)
from assms show "s0 ∈ S" "is_interval S"
by (auto simp add: usolves_ode_from_def)
next
fix z T' t
assume hyps: "s0 ∈ T'" "is_interval T'" "T' ⊆ S" "(z solves_ode g) T' Y" "z s0 = y s0" "t ∈ T'"
from ‹(z solves_ode g) T' Y›
have zsol: "(z solves_ode f) T' Y"
by (rule solves_ode_congI) (use assms hyps in ‹auto dest!: solves_ode_domainD›)
have "z t = x t"
by (rule x[THEN usolves_odeD(4),where T' = T'])
(use zsol ‹s0 ∈ T'› ‹is_interval T'› ‹T' ⊆ S› ‹T = S› ‹z s0 = y s0› ‹t ∈ T'› assms in auto)
also have "y t = x t" using assms ‹t ∈ T'› ‹T' ⊆ S› ‹T = S› by auto
finally show "z t = y t" by simp
qed
lemma usolves_ode_cong[cong]:
assumes "⋀t. t ∈ T ⟹ x t = y t"
assumes "⋀t y. t ∈ T ⟹ y ∈ X ⟹ f t y = g t y"
assumes "t0 = s0"
assumes "T = S"
assumes "X = Y"
shows "(x usolves_ode f from t0) T X ⟷ (y usolves_ode g from s0) S Y"
apply (rule iffI)
subgoal by (rule usolves_ode_congI[OF _ assms]; assumption)
subgoal by (metis assms(1) assms(2) assms(3) assms(4) assms(5) usolves_ode_congI)
done
lemma shift_autonomous_unique_solution:
assumes usol: "(x usolves_ode f from t0) T X"
assumes auto: "⋀s t x. x ∈ X ⟹ f s x = f t x"
shows "((λt. x (t + t0 - t1)) usolves_ode f from t1) ((+) (t1 - t0) ` T) X"
proof (rule usolves_ode_rawI)
from usolves_odeD[OF usol]
have sol: "(x solves_ode f) T X"
and "t0 ∈ T"
and "is_interval T"
and unique: "t0 ∈ T' ⟹ is_interval T' ⟹ T' ⊆ T ⟹ (z solves_ode f) T' X ⟹ z t0 = x t0 ⟹ t ∈ T' ⟹ z t = x t"
for z T' t
by blast+
have "(λt. t + t1 - t0) = (+) (t1 - t0)"
by (auto simp add: algebra_simps)
with shift_autonomous_solution[OF sol auto, of "t0 - t1"] solves_odeD[OF sol]
show "((λt. x (t + t0 - t1)) solves_ode f) ((+) (t1 - t0) ` T) X"
by (simp add: algebra_simps)
from ‹t0 ∈ T› show "t1 ∈ (+) (t1 - t0) ` T" by auto
from ‹is_interval T›
show "is_interval ((+) (t1 - t0) ` T)"
by simp
fix z T' t
assume z: "(z solves_ode f) T' X"
and t0': "t1 ∈ T'" "T' ⊆ (+) (t1 - t0) ` T"
and shift: "z t1 = x (t1 + t0 - t1)"
and t: "t ∈ T'"
and ivl: "is_interval T'"
let ?z = "(λt. z (t + (t1 - t0)))"
have "(?z solves_ode f) ((λt. t - (t1 - t0)) ` T') X"
apply (rule shift_autonomous_solution[OF z, of "t1 - t0"])
using solves_odeD[OF z]
by (auto intro!: auto)
with _ _ _ have "?z ((t + (t0 - t1))) = x (t + (t0 - t1))"
apply (rule unique[where z = ?z ])
using shift t t0' ivl
by auto
then show "z t = x (t + t0 - t1)"
by (simp add: algebra_simps)
qed
lemma three_intervals_lemma:
fixes a b c::real
assumes a: "a ∈ A - B"
and b: "b ∈ B - A"
and c: "c ∈ A ∩ B"
and iA: "is_interval A" and iB: "is_interval B"
and aI: "a ∈ I"
and bI: "b ∈ I"
and iI: "is_interval I"
shows "c ∈ I"
apply (rule mem_is_intervalI[OF iI aI bI])
using iA iB
apply (auto simp: is_interval_def)
apply (metis Diff_iff Int_iff a b c le_cases)
apply (metis Diff_iff Int_iff a b c le_cases)
done
lemma connection_usolves_ode:
assumes x: "(x usolves_ode f from tx) T X"
assumes y: "⋀t. t ∈ closure S ∩ closure T ⟹ (y usolves_ode g from t) S X"
assumes conn_T: "closure S ∩ closure T ⊆ T"
assumes conn_S: "closure S ∩ closure T ⊆ S"
assumes conn_t: "t ∈ closure S ∩ closure T"
assumes conn_x: "⋀t. t ∈ closure S ⟹ t ∈ closure T ⟹ x t = y t"
assumes conn_f: "⋀t x. t ∈ closure S ⟹ t ∈ closure T ⟹ x ∈ X ⟹ f t x = g t x"
shows "((λt. if t ∈ T then x t else y t) usolves_ode (λt. if t ∈ T then f t else g t) from tx) (T ∪ S) X"
apply (rule usolves_ode_rawI)
apply (subst Un_absorb[of X, symmetric])
apply (rule connection_solves_ode[OF usolves_odeD(1)[OF x] usolves_odeD(1)[OF y[OF conn_t]] conn_T conn_S conn_x conn_f])
subgoal by assumption
subgoal by assumption
subgoal by assumption
subgoal by assumption
subgoal using solves_odeD(2)[OF usolves_odeD(1)[OF x]] conn_T by (auto simp add: conn_x[symmetric])
subgoal using usolves_odeD(2)[OF x] by auto
subgoal using usolves_odeD(3)[OF x] usolves_odeD(3)[OF y]
apply (rule is_real_interval_union)
using conn_T conn_S conn_t by auto
subgoal premises prems for z TS' s
proof -
from ‹(z solves_ode _) _ _›
have "(z solves_ode (λt. if t ∈ T then f t else g t)) (T ∩ TS') X"
by (rule solves_ode_on_subset) auto
then have z_f: "(z solves_ode f) (T ∩ TS') X"
by (subst solves_ode_cong) auto
from prems(4)
have "(z solves_ode (λt. if t ∈ T then f t else g t)) (S ∩ TS') X"
by (rule solves_ode_on_subset) auto
then have z_g: "(z solves_ode g) (S ∩ TS') X"
apply (rule solves_ode_congI)
subgoal by simp
subgoal by clarsimp (meson closure_subset conn_f contra_subsetD prems(4) solves_ode_domainD)
subgoal by simp
subgoal by simp
done
have "tx ∈ T" using assms using usolves_odeD(2)[OF x] by auto
have "z tx = x tx" using assms prems
by (simp add: ‹tx ∈ T›)
from usolves_odeD(4)[OF x _ _ _ ‹(z solves_ode f) _ _›, of s] prems
have "z s = x s" if "s ∈ T" using that ‹tx ∈ T› ‹z tx = x tx›
by (auto simp: is_interval_Int usolves_odeD(3)[OF x] ‹is_interval TS'›)
moreover
{
assume "s ∉ T"
then have "s ∈ S" using prems assms by auto
{
assume "tx ∉ S"
then have "tx ∈ T - S" using ‹tx ∈ T› by simp
moreover have "s ∈ S - T" using ‹s ∉ T› ‹s ∈ S› by blast
ultimately have "t ∈ TS'"
apply (rule three_intervals_lemma)
subgoal using assms by auto
subgoal using usolves_odeD(3)[OF x] .
subgoal using usolves_odeD(3)[OF y[OF conn_t]] .
subgoal using ‹tx ∈ TS'› .
subgoal using ‹s ∈ TS'› .
subgoal using ‹is_interval TS'› .
done
with assms have t: "t ∈ closure S ∩ closure T ∩ TS'" by simp
then have "t ∈ S" "t ∈ T" "t ∈ TS'" using assms by auto
have "z t = x t"
apply (rule usolves_odeD(4)[OF x _ _ _ z_f, of t])
using ‹t ∈ TS'› ‹t ∈ T› prems assms ‹tx ∈ T› usolves_odeD(3)[OF x]
by (auto intro!: is_interval_Int)
with assms have "z t = y t" using t by auto
from usolves_odeD(4)[OF y[OF conn_t] _ _ _ z_g, of s] prems
have "z s = y s" using ‹s ∉ T› assms ‹z t = y t› t ‹t ∈ S›
‹is_interval TS'› usolves_odeD(3)[OF y[OF conn_t]]
by (auto simp: is_interval_Int)
} moreover {
assume "tx ∈ S"
with prems closure_subset ‹tx ∈ T›
have tx: "tx ∈ closure S ∩ closure T ∩ TS'" by force
then have "tx ∈ S" "tx ∈ T" "tx ∈ TS'" using assms by auto
have "z tx = x tx"
apply (rule usolves_odeD(4)[OF x _ _ _ z_f, of tx])
using ‹tx ∈ TS'› ‹tx ∈ T› prems assms ‹tx ∈ T› usolves_odeD(3)[OF x]
by (auto intro!: is_interval_Int)
with assms have "z tx = y tx" using tx by auto
from usolves_odeD(4)[OF y[where t=tx] _ _ _ z_g, of s] prems
have "z s = y s" using ‹s ∉ T› assms ‹z tx = y tx› tx ‹tx ∈ S›
‹is_interval TS'› usolves_odeD(3)[OF y]
by (auto simp: is_interval_Int)
} ultimately have "z s = y s" by blast
}
ultimately
show "z s = (if s ∈ T then x s else y s)" by simp
qed
done
lemma usolves_ode_union_closed:
assumes x: "(x usolves_ode f from tx) T X"
assumes y: "⋀t. t ∈ closure S ∩ closure T ⟹ (x usolves_ode f from t) S X"
assumes conn_T: "closure S ∩ closure T ⊆ T"
assumes conn_S: "closure S ∩ closure T ⊆ S"
assumes conn_t: "t ∈ closure S ∩ closure T"
shows "(x usolves_ode f from tx) (T ∪ S) X"
using connection_usolves_ode[OF assms] by simp
lemma usolves_ode_solves_odeI:
assumes "(x usolves_ode f from tx) T X"
assumes "(y solves_ode f) T X" "y tx = x tx"
shows "(y usolves_ode f from tx) T X"
using assms(1)
apply (rule usolves_ode_congI)
subgoal using assms by (metis set_eq_subset usolves_odeD(2) usolves_odeD(3) usolves_odeD(4))
by auto
lemma usolves_ode_subset_range:
assumes x: "(x usolves_ode f from t0) T X"
assumes r: "x ` T ⊆ Y" and "Y ⊆ X"
shows "(x usolves_ode f from t0) T Y"
proof (rule usolves_odeI)
note usolves_odeD[OF x]
show "(x solves_ode f) T Y" by (rule solves_ode_subset_range; fact)
show "t0 ∈ T" "is_interval T" by fact+
fix z t
assume s: "{t0 -- t} ⊆ T" and z: "(z solves_ode f) {t0 -- t} Y" and z0: "z t0 = x t0"
then have "t0 ∈ {t0 -- t}" "is_interval {t0 -- t}"
by auto
moreover note s
moreover have "(z solves_ode f) {t0--t} X"
using solves_odeD[OF z] ‹Y ⊆ X›
by (intro solves_ode_subset_range[OF z]) force
moreover note z0
moreover have "t ∈ {t0 -- t}" by simp
ultimately show "z t = x t"
by (rule usolves_odeD[OF x])
qed
subsection ‹ivp on interval›
context
fixes t0 t1::real and T
defines "T ≡ closed_segment t0 t1"
begin
lemma is_solution_ext_cont:
"continuous_on T x ⟹ (ext_cont x (min t0 t1) (max t0 t1) solves_ode f) T X = (x solves_ode f) T X"
by (rule solves_ode_cong) (auto simp add: T_def min_def max_def closed_segment_eq_real_ivl)
lemma solution_fixed_point:
fixes x:: "real ⇒ 'a::banach"
assumes x: "(x solves_ode f) T X" and t: "t ∈ T"
shows "x t0 + ivl_integral t0 t (λt. f t (x t)) = x t"
proof -
from solves_odeD(1)[OF x, unfolded T_def]
have "(x has_vderiv_on (λt. f t (x t))) (closed_segment t0 t)"
by (rule has_vderiv_on_subset) (insert ‹t ∈ T›, auto simp: closed_segment_eq_real_ivl T_def)
from fundamental_theorem_of_calculus_ivl_integral[OF this]
have "((λt. f t (x t)) has_ivl_integral x t - x t0) t0 t" .
from this[THEN ivl_integral_unique]
show ?thesis by simp
qed
lemma solution_fixed_point_left:
fixes x:: "real ⇒ 'a::banach"
assumes x: "(x solves_ode f) T X" and t: "t ∈ T"
shows "x t1 - ivl_integral t t1 (λt. f t (x t)) = x t"
proof -
from solves_odeD(1)[OF x, unfolded T_def]
have "(x has_vderiv_on (λt. f t (x t))) (closed_segment t t1)"
by (rule has_vderiv_on_subset) (insert ‹t ∈ T›, auto simp: closed_segment_eq_real_ivl T_def)
from fundamental_theorem_of_calculus_ivl_integral[OF this]
have "((λt. f t (x t)) has_ivl_integral x t1 - x t) t t1" .
from this[THEN ivl_integral_unique]
show ?thesis by simp
qed
lemma solution_fixed_pointI:
fixes x:: "real ⇒ 'a::banach"
assumes cont_f: "continuous_on (T × X) (λ(t, x). f t x)"
assumes cont_x: "continuous_on T x"
assumes defined: "⋀t. t ∈ T ⟹ x t ∈ X"
assumes fp: "⋀t. t ∈ T ⟹ x t = x t0 + ivl_integral t0 t (λt. f t (x t))"
shows "(x solves_ode f) T X"
proof (rule solves_odeI)
note [continuous_intros] = continuous_on_compose_Pair[OF cont_f]
have "((λt. x t0 + ivl_integral t0 t (λt. f t (x t))) has_vderiv_on (λt. f t (x t))) T"
using cont_x defined
by (auto intro!: derivative_eq_intros ivl_integral_has_vector_derivative
continuous_intros
simp: has_vderiv_on_def T_def)
with fp show "(x has_vderiv_on (λt. f t (x t))) T" by simp
qed (simp add: defined)
end
lemma solves_ode_half_open_segment_continuation:
fixes f::"real ⇒ 'a ⇒ 'a::banach"
assumes ode: "(x solves_ode f) {t0 --< t1} X"
assumes continuous: "continuous_on ({t0 -- t1} × X) (λ(t, x). f t x)"
assumes "compact X"
assumes "t0 ≠ t1"
obtains l where
"(x ⤏ l) (at t1 within {t0 --< t1})"
"((λt. if t = t1 then l else x t) solves_ode f) {t0 -- t1} X"
proof -
note [continuous_intros] = continuous_on_compose_Pair[OF continuous]
have "compact ((λ(t, x). f t x) ` ({t0 -- t1} × X))"
by (auto intro!: compact_continuous_image continuous_intros compact_Times ‹compact X›
simp: split_beta)
then obtain B where "B > 0" and B: "⋀t x. t ∈ {t0 -- t1} ⟹ x ∈ X ⟹ norm (f t x) ≤ B"
by (auto dest!: compact_imp_bounded simp: bounded_pos)
have uc: "uniformly_continuous_on {t0 --< t1} x"
apply (rule lipschitz_on_uniformly_continuous[where L=B])
apply (rule bounded_vderiv_on_imp_lipschitz)
apply (rule solves_odeD[OF ode])
using solves_odeD(2)[OF ode] ‹0 < B›
by (auto simp: closed_segment_eq_real_ivl half_open_segment_real subset_iff
intro!: B split: if_split_asm)
have "t1 ∈ closure ({t0 --< t1})"
using closure_half_open_segment[of t0 t1] ‹t0 ≠ t1›
by simp
from uniformly_continuous_on_extension_on_closure[OF uc]
obtain g where uc_g: "uniformly_continuous_on {t0--t1} g"
and xg: "(⋀t. t ∈ {t0 --< t1} ⟹ x t = g t)"
using closure_half_open_segment[of t0 t1] ‹t0 ≠ t1›
by metis
from uc_g[THEN uniformly_continuous_imp_continuous, unfolded continuous_on_def]
have "(g ⤏ g t) (at t within {t0--t1})" if "t∈{t0--t1}" for t
using that by auto
then have g_tendsto: "(g ⤏ g t) (at t within {t0--<t1})" if "t∈{t0--t1}" for t
using that by (auto intro: tendsto_within_subset half_open_segment_subset)
then have x_tendsto: "(x ⤏ g t) (at t within {t0--<t1})" if "t∈{t0--t1}" for t
using that
by (subst Lim_cong_within[OF refl refl refl xg]) auto
then have "(x ⤏ g t1) (at t1 within {t0 --< t1})"
by auto
moreover
have nbot: "at s within {t0--<t1} ≠ bot" if "s ∈ {t0--t1}" for s
using that ‹t0 ≠ t1›
by (auto simp: trivial_limit_within islimpt_half_open_segment)
have g_mem: "s ∈ {t0--t1} ⟹ g s ∈ X" for s
apply (rule Lim_in_closed_set[OF compact_imp_closed[OF ‹compact X›] _ _ x_tendsto])
using solves_odeD(2)[OF ode] ‹t0 ≠ t1›
by (auto intro!: simp: eventually_at_filter nbot)
have "(g solves_ode f) {t0 -- t1} X"
apply (rule solution_fixed_pointI[OF continuous])
subgoal by (auto intro!: uc_g uniformly_continuous_imp_continuous)
subgoal by (rule g_mem)
subgoal premises prems for s
proof -
{
fix s
assume s: "s ∈ {t0--<t1}"
with prems have subs: "{t0--s} ⊆ {t0--<t1}"
by (auto simp: half_open_segment_real closed_segment_eq_real_ivl)
with ode have sol: "(x solves_ode f) ({t0--s}) X"
by (rule solves_ode_on_subset) (rule order_refl)
from subs have inner_eq: "t ∈ {t0 -- s} ⟹ x t = g t" for t
by (intro xg) auto
from solution_fixed_point[OF sol, of s]
have "g t0 + ivl_integral t0 s (λt. f t (g t)) - g s = 0"
using s prems ‹t0 ≠ t1›
by (auto simp: inner_eq cong: ivl_integral_cong)
} note fp = this
from prems have subs: "{t0--s} ⊆ {t0--t1}"
by (auto simp: closed_segment_eq_real_ivl)
have int: "(λt. f t (g t)) integrable_on {t0--t1}"
using prems subs
by (auto intro!: integrable_continuous_closed_segment continuous_intros g_mem
uc_g[THEN uniformly_continuous_imp_continuous, THEN continuous_on_subset])
note ivl_tendsto[tendsto_intros] =
indefinite_ivl_integral_continuous(1)[OF int, unfolded continuous_on_def, rule_format]
from subs half_open_segment_subset
have "((λs. g t0 + ivl_integral t0 s (λt. f t (g t)) - g s) ⤏
g t0 + ivl_integral t0 s (λt. f t (g t)) - g s) (at s within {t0 --< t1})"
using subs
by (auto intro!: tendsto_intros ivl_tendsto[THEN tendsto_within_subset]
g_tendsto[THEN tendsto_within_subset])
moreover
have "((λs. g t0 + ivl_integral t0 s (λt. f t (g t)) - g s) ⤏ 0) (at s within {t0 --< t1})"
apply (subst Lim_cong_within[OF refl refl refl, where g="λ_. 0"])
subgoal by (subst fp) auto
subgoal by simp
done
ultimately have "g t0 + ivl_integral t0 s (λt. f t (g t)) - g s = 0"
using nbot prems tendsto_unique by blast
then show "g s = g t0 + ivl_integral t0 s (λt. f t (g t))" by simp
qed
done
then have "((λt. if t = t1 then g t1 else x t) solves_ode f) {t0--t1} X"
apply (rule solves_ode_congI)
using xg ‹t0 ≠ t1›
by (auto simp: half_open_segment_closed_segmentI)
ultimately show ?thesis ..
qed
subsection ‹Picard-Lindeloef on set of functions into closed set›
text‹\label{sec:plclosed}›
locale continuous_rhs = fixes T X f
assumes continuous: "continuous_on (T × X) (λ(t, x). f t x)"
begin
lemma continuous_rhs_comp[continuous_intros]:
assumes [continuous_intros]: "continuous_on S g"
assumes [continuous_intros]: "continuous_on S h"
assumes "g ` S ⊆ T"
assumes "h ` S ⊆ X"
shows "continuous_on S (λx. f (g x) (h x))"
using continuous_on_compose_Pair[OF continuous assms(1,2)] assms(3,4)
by auto
end
locale global_lipschitz =
fixes T X f and L::real
assumes lipschitz: "⋀t. t ∈ T ⟹ L-lipschitz_on X (λx. f t x)"
locale closed_domain =
fixes X assumes closed: "closed X"
locale interval = fixes T::"real set"
assumes interval: "is_interval T"
begin
lemma closed_segment_subset_domain: "t0 ∈ T ⟹ t ∈ T ⟹ closed_segment t0 t ⊆ T"
by (simp add: closed_segment_subset_interval interval)
lemma closed_segment_subset_domainI: "t0 ∈ T ⟹ t ∈ T ⟹ s ∈ closed_segment t0 t ⟹ s ∈ T"
using closed_segment_subset_domain by force
lemma convex[intro, simp]: "convex T"
and connected[intro, simp]: "connected T"
by (simp_all add: interval is_interval_connected is_interval_convex )
end
locale nonempty_set = fixes T assumes nonempty_set: "T ≠ {}"
locale compact_interval = interval + nonempty_set T +
assumes compact_time: "compact T"
begin
definition "tmin = Inf T"
definition "tmax = Sup T"
lemma
shows tmin: "t ∈ T ⟹ tmin ≤ t" "tmin ∈ T"
and tmax: "t ∈ T ⟹ t ≤ tmax" "tmax ∈ T"
using nonempty_set
by (auto intro!: cInf_lower cSup_upper bounded_imp_bdd_below bounded_imp_bdd_above
compact_imp_bounded compact_time closed_contains_Inf closed_contains_Sup compact_imp_closed
simp: tmin_def tmax_def)
lemma tmin_le_tmax[intro, simp]: "tmin ≤ tmax"
using nonempty_set tmin tmax by auto
lemma T_def: "T = {tmin .. tmax}"
using closed_segment_subset_interval[OF interval tmin(2) tmax(2)]
by (auto simp: closed_segment_eq_real_ivl subset_iff intro!: tmin tmax)
lemma mem_T_I[intro, simp]: "tmin ≤ t ⟹ t ≤ tmax ⟹ t ∈ T"
using interval mem_is_interval_1_I tmax(2) tmin(2) by blast
end
locale self_mapping = interval T for T +
fixes t0::real and x0 f X
assumes iv_defined: "t0 ∈ T" "x0 ∈ X"
assumes self_mapping:
"⋀x t. t ∈ T ⟹ x t0 = x0 ⟹ x ∈ closed_segment t0 t → X ⟹
continuous_on (closed_segment t0 t) x ⟹ x t0 + ivl_integral t0 t (λt. f t (x t)) ∈ X"
begin
sublocale nonempty_set T using iv_defined by unfold_locales auto
lemma closed_segment_iv_subset_domain: "t ∈ T ⟹ closed_segment t0 t ⊆ T"
by (simp add: closed_segment_subset_domain iv_defined)
end
locale unique_on_closed =
compact_interval T +
self_mapping T t0 x0 f X +
continuous_rhs T X f +
closed_domain X +
global_lipschitz T X f L for t0::real and T and x0::"'a::banach" and f X L
begin
lemma T_split: "T = {tmin .. t0} ∪ {t0 .. tmax}"
by (metis T_def atLeastAtMost_iff iv_defined(1) ivl_disj_un_two_touch(4))
lemma L_nonneg: "0 ≤ L"
by (auto intro!: lipschitz_on_nonneg[OF lipschitz] iv_defined)
text ‹Picard Iteration›
definition P_inner where "P_inner x t = x0 + ivl_integral t0 t (λt. f t (x t))"
definition P::"(real ⇒⇩C 'a) ⇒ (real ⇒⇩C 'a)"
where "P x = (SOME g::real⇒⇩C 'a.
(∀t ∈ T. g t = P_inner x t) ∧
(∀t≤tmin. g t = P_inner x tmin) ∧
(∀t≥tmax. g t = P_inner x tmax))"
lemma cont_P_inner_ivl:
"x ∈ T →⇩C X ⟹ continuous_on {tmin..tmax} (P_inner (apply_bcontfun x))"
apply (auto simp: real_Icc_closed_segment P_inner_def Pi_iff mem_PiC_iff
intro!: continuous_intros indefinite_ivl_integral_continuous_subset
integrable_continuous_closed_segment tmin(1) tmax(1))
using closed_segment_subset_domainI tmax(2) tmin(2) apply blast
using closed_segment_subset_domainI tmax(2) tmin(2) apply blast
using T_def closed_segment_eq_real_ivl iv_defined(1) by auto
lemma P_inner_t0[simp]: "P_inner g t0 = x0"
by (simp add: P_inner_def)
lemma t0_cs_tmin_tmax: "t0 ∈ {tmin--tmax}" and cs_tmin_tmax_subset: "{tmin--tmax} ⊆ T"
using iv_defined T_def closed_segment_eq_real_ivl
by auto
lemma
P_eqs:
assumes "x ∈ T →⇩C X"
shows P_eq_P_inner: "t ∈ T ⟹ P x t = P_inner x t"
and P_le_tmin: "t ≤ tmin ⟹ P x t = P_inner x tmin"
and P_ge_tmax: "t ≥ tmax ⟹ P x t = P_inner x tmax"
unfolding atomize_conj atomize_imp
proof goal_cases
case 1
obtain g where
"t ∈ {tmin .. tmax} ⟹ apply_bcontfun g t = P_inner (apply_bcontfun x) t"
"apply_bcontfun g t = P_inner (apply_bcontfun x) (clamp tmin tmax t)"
for t
by (metis continuous_on_cbox_bcontfunE cont_P_inner_ivl[OF assms(1)] cbox_interval)
with T_def have "∃g::real⇒⇩C 'a.
(∀t ∈ T. g t = P_inner x t) ∧
(∀t≤tmin. g t = P_inner x tmin) ∧
(∀t≥tmax. g t = P_inner x tmax)"
by (auto intro!: exI[where x=g])
then have "(∀t ∈ T. P x t = P_inner x t) ∧
(∀t≤tmin. P x t = P_inner x tmin) ∧
(∀t≥tmax. P x t = P_inner x tmax)"
unfolding P_def
by (rule someI_ex)
then show ?case using T_def by auto
qed
lemma P_if_eq:
"x ∈ T →⇩C X ⟹
P x t = (if tmin ≤ t ∧ t ≤ tmax then P_inner x t else if t ≥ tmax then P_inner x tmax else P_inner x tmin)"
by (auto simp: P_eqs)
lemma dist_P_le:
assumes y: "y ∈ T →⇩C X" and z: "z ∈ T →⇩C X"
assumes le: "⋀t. tmin ≤ t ⟹ t ≤ tmax ⟹ dist (P_inner y t) (P_inner z t) ≤ R"
assumes "0 ≤ R"
shows "dist (P y t) (P z t) ≤ R"
by (cases "t ≤ tmin"; cases "t ≥ tmax") (auto simp: P_eqs y z not_le intro!: le)
lemma P_def':
assumes "t ∈ T"
assumes "fixed_point ∈ T →⇩C X"
shows "(P fixed_point) t = x0 + ivl_integral t0 t (λx. f x (fixed_point x))"
by (simp add: P_eq_P_inner assms P_inner_def)
definition "iter_space = PiC T ((λ_. X)(t0:={x0}))"
lemma iter_spaceI:
assumes "g ∈ T →⇩C X" "g t0 = x0"
shows "g ∈ iter_space"
using assms
by (simp add: iter_space_def mem_PiC_iff Pi_iff)
lemma iter_spaceD:
assumes "g ∈ iter_space"
shows "g ∈ T →⇩C X" "apply_bcontfun g t0 = x0"
using assms iv_defined
by (auto simp add: iter_space_def mem_PiC_iff split: if_splits)
lemma const_in_iter_space: "const_bcontfun x0 ∈ iter_space"
by (auto simp: iter_space_def iv_defined mem_PiC_iff)
lemma closed_iter_space: "closed iter_space"
by (auto simp: iter_space_def intro!: closed_PiC closed)
lemma iter_space_notempty: "iter_space ≠ {}"
using const_in_iter_space by blast
lemma clamp_in_eq[simp]: fixes a x b::real shows "a ≤ x ⟹ x ≤ b ⟹ clamp a b x = x"
by (auto simp: clamp_def)
lemma P_self_mapping:
assumes in_space: "g ∈ iter_space"
shows "P g ∈ iter_space"
proof (rule iter_spaceI)
show x0: "P g t0 = x0"
by (auto simp: P_def' iv_defined iter_spaceD[OF in_space])
from iter_spaceD(1)[OF in_space] show "P g ∈ T →⇩C X"
unfolding mem_PiC_iff Pi_iff
apply (auto simp: mem_PiC_iff Pi_iff P_def')
apply (auto simp: iter_spaceD(2)[OF in_space, symmetric] intro!: self_mapping)
using closed_segment_subset_domainI iv_defined(1) by blast
qed
lemma continuous_on_T: "continuous_on {tmin .. tmax} g ⟹ continuous_on T g"
using T_def by auto
lemma T_closed_segment_subsetI[intro, simp]: "t ∈ {tmin--tmax} ⟹ t ∈ T"
and T_subsetI[intro, simp]: "tmin ≤ t ⟹ t ≤ tmax ⟹ t ∈ T"
by (subst T_def, simp add: closed_segment_eq_real_ivl)+
lemma t0_mem_closed_segment[intro, simp]: "t0 ∈ {tmin--tmax}"
using T_def iv_defined
by (simp add: closed_segment_eq_real_ivl)
lemma tmin_le_t0[intro, simp]: "tmin ≤ t0"
and tmax_ge_t0[intro, simp]: "tmax ≥ t0"
using t0_mem_closed_segment
unfolding closed_segment_eq_real_ivl
by simp_all
lemma apply_bcontfun_solution_fixed_point:
assumes ode: "(apply_bcontfun x solves_ode f) T X"
assumes iv: "x t0 = x0"
assumes t: "t ∈ T"
shows "P x t = x t"
proof -
have "t ∈ {t0 -- t}" by simp
have ode': "(apply_bcontfun x solves_ode f) {t0--t} X" "t ∈ {t0 -- t}"
using ode T_def closed_segment_eq_real_ivl t apply auto
using closed_segment_iv_subset_domain solves_ode_on_subset apply fastforce
using closed_segment_iv_subset_domain solves_ode_on_subset apply fastforce
done
from solves_odeD[OF ode]
have x: "x ∈ T →⇩C X" by (auto simp: mem_PiC_iff)
from solution_fixed_point[OF ode'] iv
show ?thesis
unfolding P_def'[OF t x]
by simp
qed
lemma
solution_in_iter_space:
assumes ode: "(apply_bcontfun z solves_ode f) T X"
assumes iv: "z t0 = x0"
shows "z ∈ iter_space" (is "?z ∈ _")
proof -
from T_def ode have ode: "(z solves_ode f) {tmin -- tmax} X"
by (simp add: closed_segment_eq_real_ivl)
have "(?z solves_ode f) T X"
using is_solution_ext_cont[OF solves_ode_continuous_on[OF ode], of f X] ode T_def
by (auto simp: min_def max_def closed_segment_eq_real_ivl)
then have "z ∈ T →⇩C X"
by (auto simp add: solves_ode_def mem_PiC_iff)
thus "?z ∈ iter_space"
by (auto simp: iv intro!: iter_spaceI)
qed
end
locale unique_on_bounded_closed = unique_on_closed +
assumes lipschitz_bound: "⋀s t. s ∈ T ⟹ t ∈ T ⟹ abs (s - t) * L < 1"
begin
lemma lipschitz_bound_maxmin: "(tmax - tmin) * L < 1"
using lipschitz_bound[of tmax tmin]
by auto
lemma lipschitz_P:
shows "((tmax - tmin) * L)-lipschitz_on iter_space P"
proof (rule lipschitz_onI)
have "t0 ∈ T" by (simp add: iv_defined)
then show "0 ≤ (tmax - tmin) * L"
using T_def
by (auto intro!: mult_nonneg_nonneg lipschitz lipschitz_on_nonneg[OF lipschitz]
iv_defined)
fix y z
assume "y ∈ iter_space" and "z ∈ iter_space"
hence y_defined: "y ∈ (T →⇩C X)" and "y t0 = x0"
and z_defined: "z ∈ (T →⇩C X)" and "y t0 = x0"
by (auto dest: iter_spaceD)
have defined: "s ∈ T" "y s ∈ X" "z s ∈ X" if "s ∈ closed_segment tmin tmax" for s
using y_defined z_defined that T_def
by (auto simp: mem_PiC_iff)
{
note [intro, simp] = integrable_continuous_closed_segment
fix t
assume t_bounds: "tmin ≤ t" "t ≤ tmax"
then have cs_subs: "closed_segment t0 t ⊆ closed_segment tmin tmax"
by (auto simp: closed_segment_eq_real_ivl)
then have cs_subs_ext: "⋀ta. ta ∈ {t0--t} ⟹ ta ∈ {tmin--tmax}" by auto
have "norm (P_inner y t - P_inner z t) =
norm (ivl_integral t0 t (λt. f t (y t) - f t (z t)))"
by (subst ivl_integral_diff)
(auto intro!: integrable_continuous_closed_segment continuous_intros defined cs_subs_ext simp: P_inner_def)
also have "... ≤ abs (ivl_integral t0 t (λt. norm (f t (y t) - f t (z t))))"
by (rule ivl_integral_norm_bound_ivl_integral)
(auto intro!: ivl_integral_norm_bound_ivl_integral continuous_intros integrable_continuous_closed_segment
simp: defined cs_subs_ext)
also have "... ≤ abs (ivl_integral t0 t (λt. L * norm (y t - z t)))"
using lipschitz t_bounds T_def y_defined z_defined cs_subs
by (intro norm_ivl_integral_le) (auto intro!: continuous_intros integrable_continuous_closed_segment
simp add: dist_norm lipschitz_on_def mem_PiC_iff Pi_iff)
also have "... ≤ abs (ivl_integral t0 t (λt. L * norm (y - z)))"
using norm_bounded[of "y - z"]
L_nonneg
by (intro norm_ivl_integral_le) (auto intro!: continuous_intros mult_left_mono)
also have "... = L * abs (t - t0) * norm (y - z)"
using t_bounds L_nonneg by (simp add: abs_mult)
also have "... ≤ L * (tmax - tmin) * norm (y - z)"
using t_bounds zero_le_dist L_nonneg cs_subs tmin_le_t0 tmax_ge_t0
by (auto intro!: mult_right_mono mult_left_mono simp: closed_segment_eq_real_ivl abs_real_def
simp del: tmin_le_t0 tmax_ge_t0 split: if_split_asm)
finally
have "dist (P_inner y t) (P_inner z t) ≤ (tmax - tmin) * L * dist y z"
by (simp add: dist_norm ac_simps)
} note * = this
show "dist (P y) (P z) ≤ (tmax - tmin) * L * dist y z"
by (auto intro!: dist_bound dist_P_le * y_defined z_defined mult_nonneg_nonneg L_nonneg)
qed
lemma fixed_point_unique: "∃!x∈iter_space. P x = x"
using lipschitz lipschitz_bound_maxmin lipschitz_P T_def
complete_UNIV iv_defined
by (intro banach_fix)
(auto
intro: P_self_mapping split_mult_pos_le
intro!: closed_iter_space iter_space_notempty mult_nonneg_nonneg
simp: lipschitz_on_def complete_eq_closed)
definition fixed_point where
"fixed_point = (THE x. x ∈ iter_space ∧ P x = x)"
lemma fixed_point':
"fixed_point ∈ iter_space ∧ P fixed_point = fixed_point"
unfolding fixed_point_def using fixed_point_unique
by (rule theI')
lemma fixed_point:
"fixed_point ∈ iter_space" "P fixed_point = fixed_point"
using fixed_point' by simp_all
lemma fixed_point_equality': "x ∈ iter_space ∧ P x = x ⟹ fixed_point = x"
unfolding fixed_point_def using fixed_point_unique
by (rule the1_equality)
lemma fixed_point_equality: "x ∈ iter_space ⟹ P x = x ⟹ fixed_point = x"
using fixed_point_equality'[of x] by auto
lemma fixed_point_iv: "fixed_point t0 = x0"
and fixed_point_domain: "x ∈ T ⟹ fixed_point x ∈ X"
using fixed_point
by (force dest: iter_spaceD simp: mem_PiC_iff)+
lemma fixed_point_has_vderiv_on: "(fixed_point has_vderiv_on (λt. f t (fixed_point t))) T"
proof -
have "continuous_on T (λx. f x (fixed_point x))"
using fixed_point_domain
by (auto intro!: continuous_intros)
then have "((λu. x0 + ivl_integral t0 u (λx. f x (fixed_point x))) has_vderiv_on (λt. f t (fixed_point t))) T"
by (auto intro!: derivative_intros ivl_integral_has_vderiv_on_compact_interval interval compact_time)
then show ?thesis
proof (rule has_vderiv_eq)
fix t
assume t: "t ∈ T"
have "fixed_point t = P fixed_point t"
using fixed_point by simp
also have "… = x0 + ivl_integral t0 t (λx. f x (fixed_point x))"
using t fixed_point_domain
by (auto simp: P_def' mem_PiC_iff)
finally show "x0 + ivl_integral t0 t (λx. f x (fixed_point x)) = fixed_point t" by simp
qed (insert T_def, auto simp: closed_segment_eq_real_ivl)
qed
lemma fixed_point_solution:
shows "(fixed_point solves_ode f) T X"
using fixed_point_has_vderiv_on fixed_point_domain
by (rule solves_odeI)
subsubsection ‹Unique solution›
text‹\label{sec:ivp-ubs}›
lemma solves_ode_equals_fixed_point:
assumes ode: "(x solves_ode f) T X"
assumes iv: "x t0 = x0"
assumes t: "t ∈ T"
shows "x t = fixed_point t"
proof -
from solves_ode_continuous_on[OF ode] T_def
have "continuous_on (cbox tmin tmax) x" by simp
from continuous_on_cbox_bcontfunE[OF this]
obtain g where g:
"t ∈ {tmin .. tmax} ⟹ apply_bcontfun g t = x t"
"apply_bcontfun g t = x (clamp tmin tmax t)"
for t
by (metis interval_cbox)
with ode T_def have ode_g: "(g solves_ode f) T X"
by (metis (no_types, lifting) solves_ode_cong)
have "x t = g t"
using t T_def
by (intro g[symmetric]) auto
also
have "g t0 = x0" "g ∈ T →⇩C X"
using iv g solves_odeD(2)[OF ode_g]
unfolding mem_PiC_iff atLeastAtMost_iff
by blast+
then have "g ∈ iter_space"
by (intro iter_spaceI)
then have "g = fixed_point"
apply (rule fixed_point_equality[symmetric])
apply (rule bcontfun_eqI)
subgoal for t
using apply_bcontfun_solution_fixed_point[OF ode_g ‹g t0 = x0›, of tmin]
apply_bcontfun_solution_fixed_point[OF ode_g ‹g t0 = x0›, of tmax]
apply_bcontfun_solution_fixed_point[OF ode_g ‹g t0 = x0›, of t]
using T_def
by (fastforce simp: P_eqs not_le ‹g ∈ T →⇩C X› g)
done
finally show ?thesis .
qed
lemma solves_ode_on_closed_segment_equals_fixed_point:
assumes ode: "(x solves_ode f) {t0 -- t1'} X"
assumes iv: "x t0 = x0"
assumes subset: "{t0--t1'} ⊆ T"
assumes t_mem: "t ∈ {t0--t1'}"
shows "x t = fixed_point t"
proof -
have subsetI: "t ∈ {t0--t1'} ⟹ t ∈ T" for t
using subset by auto
interpret s: unique_on_bounded_closed t0 "{t0--t1'}" x0 f X L
apply - apply unfold_locales
subgoal by (simp add: closed_segment_eq_real_ivl)
subgoal by simp
subgoal by simp
subgoal by simp
subgoal using iv_defined by simp
subgoal by (intro self_mapping subsetI)
subgoal by (rule continuous_on_subset[OF continuous]) (auto simp: subsetI )
subgoal by (rule lipschitz) (auto simp: subsetI)
subgoal by (auto intro!: subsetI lipschitz_bound)
done
have "x t = s.fixed_point t"
by (rule s.solves_ode_equals_fixed_point; fact)
moreover
have "fixed_point t = s.fixed_point t"
by (intro s.solves_ode_equals_fixed_point solves_ode_on_subset[OF fixed_point_solution] assms
fixed_point_iv order_refl subset t_mem)
ultimately show ?thesis by simp
qed
lemma unique_solution:
assumes ivp1: "(x solves_ode f) T X" "x t0 = x0"
assumes ivp2: "(y solves_ode f) T X" "y t0 = x0"
assumes "t ∈ T"
shows "x t = y t"
using solves_ode_equals_fixed_point[OF ivp1 ‹t ∈ T›]
solves_ode_equals_fixed_point[OF ivp2 ‹t ∈ T›]
by simp
lemma fixed_point_usolves_ode: "(fixed_point usolves_ode f from t0) T X"
apply (rule usolves_odeI[OF fixed_point_solution])
subgoal by (simp add: iv_defined(1))
subgoal by (rule interval)
subgoal
using fixed_point_iv solves_ode_on_closed_segment_equals_fixed_point
by auto
done
end
lemma closed_segment_Un:
fixes a b c::real
assumes "b ∈ closed_segment a c"
shows "closed_segment a b ∪ closed_segment b c = closed_segment a c"
using assms
by (auto simp: closed_segment_eq_real_ivl)
lemma closed_segment_closed_segment_subset:
fixes s::real and i::nat
assumes "s ∈ closed_segment a b"
assumes "a ∈ closed_segment c d" "b ∈ closed_segment c d"
shows "s ∈ closed_segment c d"
using assms
by (auto simp: closed_segment_eq_real_ivl split: if_split_asm)
context unique_on_closed begin
context
fixes t1::real
assumes mem_t1: "t1 ∈ T"
begin
lemma subdivide_count_ex: "∃n. L * abs (t1 - t0) / (Suc n) < 1"
by auto (meson add_strict_increasing less_numeral_extra(1) real_arch_simple)
definition "subdivide_count = (SOME n. L * abs (t1 - t0) / Suc n < 1)"
lemma subdivide_count: "L * abs (t1 - t0) / Suc subdivide_count < 1"
unfolding subdivide_count_def
using subdivide_count_ex
by (rule someI_ex)
lemma subdivide_lipschitz:
assumes "¦s - t¦ ≤ abs (t1 - t0) / Suc subdivide_count"
shows "¦s - t¦ * L < 1"
proof -
from assms L_nonneg
have "¦s - t¦ * L ≤ abs (t1 - t0) / Suc subdivide_count * L"
by (rule mult_right_mono)
also have "… < 1"
using subdivide_count
by (simp add: ac_simps)
finally show ?thesis .
qed
lemma subdivide_lipschitz_lemma:
assumes st: "s ∈ {a -- b}" "t ∈ {a -- b}"
assumes "abs (b - a) ≤ abs (t1 - t0) / Suc subdivide_count"
shows "¦s - t¦ * L < 1"
apply (rule subdivide_lipschitz)
apply (rule order_trans[where y="abs (b - a)"])
using assms
by (auto simp: closed_segment_eq_real_ivl split: if_splits)
definition "step = (t1 - t0) / Suc subdivide_count"
lemma last_step: "t0 + real (Suc subdivide_count) * step = t1"
by (auto simp: step_def)
lemma step_in_segment:
assumes "0 ≤ i" "i ≤ real (Suc subdivide_count)"
shows "t0 + i * step ∈ closed_segment t0 t1"
unfolding closed_segment_eq_real_ivl step_def
proof (clarsimp, safe)
assume "t0 ≤ t1"
then have "(t1 - t0) * i ≤ (t1 - t0) * (1 + subdivide_count)"
using assms
by (auto intro!: mult_left_mono)
then show "t0 + i * (t1 - t0) / (1 + real subdivide_count) ≤ t1"
by (simp add: field_simps)
next
assume "¬t0 ≤ t1"
then have "(1 + subdivide_count) * (t0 - t1) ≥ i * (t0 - t1)"
using assms
by (auto intro!: mult_right_mono)
then show "t1 ≤ t0 + i * (t1 - t0) / (1 + real subdivide_count)"
by (simp add: field_simps)
show "i * (t1 - t0) / (1 + real subdivide_count) ≤ 0"
using ‹¬t0 ≤ t1›
by (auto simp: divide_simps mult_le_0_iff assms)
qed (auto intro!: divide_nonneg_nonneg mult_nonneg_nonneg assms)
lemma subset_T1:
fixes s::real and i::nat
assumes "s ∈ closed_segment t0 (t0 + i * step)"
assumes "i ≤ Suc subdivide_count"
shows "s ∈ {t0 -- t1}"
using closed_segment_closed_segment_subset assms of_nat_le_iff of_nat_0_le_iff step_in_segment
by blast
lemma subset_T: "{t0 -- t1} ⊆ T" and subset_TI: "s ∈ {t0 -- t1} ⟹ s ∈ T"
using closed_segment_iv_subset_domain mem_t1 by blast+
primrec psolution::"nat ⇒ real ⇒ 'a" where
"psolution 0 t = x0"
| "psolution (Suc i) t = unique_on_bounded_closed.fixed_point
(t0 + real i * step) {t0 + real i * step -- t0 + real (Suc i) * step}
(psolution i (t0 + real i * step)) f X t"
definition "psolutions t = psolution (LEAST i. t ∈ closed_segment (t0 + real (i - 1) * step) (t0 + real i * step)) t"
lemma psolutions_usolves_until_step:
assumes i_le: "i ≤ Suc subdivide_count"
shows "(psolutions usolves_ode f from t0) (closed_segment t0 (t0 + real i * step)) X"
proof cases
assume "t0 = t1"
then have "step = 0"
unfolding step_def by simp
then show ?thesis by (simp add: psolutions_def iv_defined usolves_ode_singleton)
next
assume "t0 ≠ t1"
then have "step ≠ 0"
by (simp add: step_def)
define S where "S ≡ λi. closed_segment (t0 + real (i - 1) * step) (t0 + real i * step)"
have solution_eq: "psolutions ≡ λt. psolution (LEAST i. t ∈ S i) t"
by (simp add: psolutions_def[abs_def] S_def)
show ?thesis
unfolding solution_eq
using i_le
proof (induction i)
case 0 then show ?case by (simp add: iv_defined usolves_ode_singleton S_def)
next
case (Suc i)
let ?sol = "λt. psolution (LEAST i. t ∈ S i) t"
let ?pi = "t0 + real (i - Suc 0) * step" and ?i = "t0 + real i * step" and ?si = "t0 + (1 + real i) * step"
from Suc have ui: "(?sol usolves_ode f from t0) (closed_segment t0 (t0 + real i * step)) X"
by simp
from usolves_odeD(1)[OF Suc.IH] Suc
have IH_sol: "(?sol solves_ode f) (closed_segment t0 ?i) X"
by simp
have Least_eq_t0[simp]: "(LEAST n. t0 ∈ S n) = 0"
by (rule Least_equality) (auto simp add: S_def)
have Least_eq[simp]: "(LEAST n. t0 + real i * step ∈ S n) = i" for i
apply (rule Least_equality)
subgoal by (simp add: S_def)
subgoal
using ‹step ≠ 0›
by (cases "step ≥ 0")
(auto simp add: S_def closed_segment_eq_real_ivl zero_le_mult_iff split: if_split_asm)
done
have "y = t0 + real i * s"
if "t0 + (1 + real i) * s ≤ t" "t ≤ y" "y ≤ t0 + real i * s" "t0 ≤ y"
for y i s t
proof -
from that have "(1 + real i) * s ≤ real i * s" "0 ≤ real i * s"
by arith+
have "s + (t0 + s * real i) ≤ t ⟹ t ≤ y ⟹ y ≤ t0 + s * real i ⟹ t0 ≤ y ⟹ y = t0 + s * real i"
by (metis add_decreasing2 eq_iff le_add_same_cancel2 linear mult_le_0_iff of_nat_0_le_iff order.trans)
then show ?thesis using that
by (simp add: algebra_simps)
qed
then have segment_inter:
"xa = t0 + real i * step"
if
"t ∈ {t0 + real (Suc i - 1) * step--t0 + real (Suc i) * step}"
"xa ∈ closed_segment (t0 + real i * step) t" "xa ∈ closed_segment t0 (t0 + real i * step)"
for xa t
apply (cases "step > 0"; cases "step = 0")
using that
by (auto simp: S_def closed_segment_eq_real_ivl split: if_split_asm)
have right_cond: "t0 ≤ t" "t ≤ t1" if "t0 + real i * step ≤ t" "t ≤ t0 + (step + real i * step)" for t
proof -
from that have "0 ≤ step" by simp
with last_step have "t0 ≤ t1"
by (metis le_add_same_cancel1 of_nat_0_le_iff zero_le_mult_iff)
from that have "t0 ≤ t - real i * step" by simp
also have "… ≤ t" using that by (auto intro!: mult_nonneg_nonneg)
finally show "t0 ≤ t" .
have "t ≤ t0 + (real (Suc i) * step)" using that by (simp add: algebra_simps)
also have "… ≤ t1"
proof -
have "real (Suc i) * (t1 - t0) ≤ real (Suc subdivide_count) * (t1 - t0)"
using Suc.prems ‹t0 ≤ t1›
by (auto intro!: mult_mono)
then show ?thesis by (simp add: divide_simps algebra_simps step_def)
qed
finally show "t ≤ t1" .
qed
have left_cond: "t1 ≤ t" "t ≤ t0" if "t0 + (step + real i * step) ≤ t" "t ≤ t0 + real i * step" for t
proof -
from that have "step ≤ 0" by simp
with last_step have "t1 ≤ t0"
by (metis add_le_same_cancel1 mult_nonneg_nonpos of_nat_0_le_iff)
from that have "t0 ≥ t - real i * step" by simp
also have "t - real i * step ≥ t" using that by (auto intro!: mult_nonneg_nonpos)
finally (xtrans) show "t ≤ t0" .
have "t ≥ t0 + (real (Suc i) * step)" using that by (simp add: algebra_simps)
also have " t0 + (real (Suc i) * step) ≥ t1"
proof -
have "real (Suc i) * (t0 - t1) ≤ real (Suc subdivide_count) * (t0 - t1)"
using Suc.prems ‹t0 ≥ t1›
by (auto intro!: mult_mono)
then show ?thesis by (simp add: divide_simps algebra_simps step_def)
qed
finally (xtrans) show "t1 ≤ t" .
qed
interpret l: self_mapping "S (Suc i)" ?i "?sol ?i" f X
proof unfold_locales
show "?sol ?i ∈ X"
using solves_odeD(2)[OF usolves_odeD(1)[OF ui], of "?i"]
by (simp add: S_def)
fix x t assume t[unfolded S_def]: "t ∈ S (Suc i)"
and x: "x ?i = ?sol ?i" "x ∈ closed_segment ?i t → X"
and cont: "continuous_on (closed_segment ?i t) x"
let ?if = "λt. if t ∈ closed_segment t0 ?i then ?sol t else x t"
let ?f = "λt. f t (?if t)"
have sol_mem: "?sol s ∈ X" if "s ∈ closed_segment t0 ?i" for s
by (auto simp: subset_T1 intro!: solves_odeD[OF IH_sol] that)
from x(1) have "x ?i + ivl_integral ?i t (λt. f t (x t)) = ?sol ?i + ivl_integral ?i t (λt. f t (x t))"
by simp
also have "?sol ?i = ?sol t0 + ivl_integral t0 ?i (λt. f t (?sol t))"
apply (subst solution_fixed_point)
apply (rule usolves_odeD[OF ui])
by simp_all
also have "ivl_integral t0 ?i (λt. f t (?sol t)) = ivl_integral t0 ?i ?f"
by (simp cong: ivl_integral_cong)
also
have psolution_eq: "x (t0 + real i * step) = psolution i (t0 + real i * step) ⟹
ta ∈ {t0 + real i * step--t} ⟹
ta ∈ {t0--t0 + real i * step} ⟹ psolution (LEAST i. ta ∈ S i) ta = x ta" for ta
by (subst segment_inter[OF t], assumption, assumption)+ simp
have "ivl_integral ?i t (λt. f t (x t)) = ivl_integral ?i t ?f"
by (rule ivl_integral_cong) (simp_all add: x psolution_eq)
also
from t right_cond(1) have cs: "closed_segment t0 t = closed_segment t0 ?i ∪ closed_segment ?i t"
by (intro closed_segment_Un[symmetric])
(auto simp: closed_segment_eq_real_ivl algebra_simps mult_le_0_iff split: if_split_asm
intro!: segment_inter segment_inter[symmetric])
have cont_if: "continuous_on (closed_segment t0 t) ?if"
unfolding cs
using x Suc.prems cont t psolution_eq
by (auto simp: subset_T1 T_def intro!: continuous_on_cases solves_ode_continuous_on[OF IH_sol])
have t_mem: "t ∈ closed_segment t0 t1"
using x Suc.prems t
apply -
apply (rule closed_segment_closed_segment_subset, assumption)
apply (rule step_in_segment, force, force)
apply (rule step_in_segment, force, force)
done
have segment_subset: "ta ∈ {t0 + real i * step--t} ⟹ ta ∈ {t0--t1}" for ta
using x Suc.prems
apply -
apply (rule closed_segment_closed_segment_subset, assumption)
subgoal by (rule step_in_segment; force)
subgoal by (rule t_mem)
done
have cont_f: "continuous_on (closed_segment t0 t) ?f"
apply (rule continuous_intros)
apply (rule continuous_intros)
apply (rule cont_if)
unfolding cs
using x Suc.prems
apply (auto simp: subset_T1 segment_subset intro!: sol_mem subset_TI)
done
have "?sol t0 + ivl_integral t0 ?i ?f + ivl_integral ?i t ?f = ?if t0 + ivl_integral t0 t ?f"
by (auto simp: cs intro!: ivl_integral_combine integrable_continuous_closed_segment
continuous_on_subset[OF cont_f])
also have "… ∈ X"
apply (rule self_mapping)
apply (rule subset_TI)
apply (rule t_mem)
using x cont_if
by (auto simp: subset_T1 Pi_iff cs intro!: sol_mem)
finally
have "x ?i + ivl_integral ?i t (λt. ?f t) ∈ X" .
also have "ivl_integral ?i t (λt. ?f t) = ivl_integral ?i t (λt. f t (x t))"
apply (rule ivl_integral_cong[OF _ refl refl])
using x
by (auto simp: segment_inter psolution_eq)
finally
show "x ?i + ivl_integral ?i t (λt. f t (x t)) ∈ X" .
qed (auto simp add: S_def closed_segment_eq_real_ivl)
have "S (Suc i) ⊆ T"
unfolding S_def
apply (rule subsetI)
apply (rule subset_TI)
proof (cases "step = 0")
case False
fix x assume x: "x ∈ {t0 + real (Suc i - 1) * step--t0 + real (Suc i) * step}"
from x have nn: "((x - t0) / step) ≥ 0"
using False right_cond(1)[of x] left_cond(2)[of x]
by (auto simp: closed_segment_eq_real_ivl divide_simps algebra_simps split: if_splits)
have "t1 < t0 ⟹ t1 ≤ x" "t1 > t0 ⟹ x ≤ t1"
using x False right_cond(1,2)[of x] left_cond(1,2)[of x]
by (auto simp: closed_segment_eq_real_ivl algebra_simps split: if_splits)
then have le: "(x - t0) / step ≤ 1 + real subdivide_count"
unfolding step_def
by (auto simp: divide_simps)
have "x = t0 + ((x - t0) / step) * step"
using False
by auto
also have "… ∈ {t0 -- t1}"
by (rule step_in_segment) (auto simp: nn le)
finally show "x ∈ {t0 -- t1}" by simp
qed simp
have algebra: "(1 + real i) * (t1 - t0) - real i * (t1 - t0) = t1 - t0"
by (simp only: algebra_simps)
interpret l: unique_on_bounded_closed ?i "S (Suc i)" "?sol ?i" f X L
apply unfold_locales
subgoal by (auto simp: S_def)
subgoal using ‹S (Suc i) ⊆ T› by (auto intro!: continuous_intros simp: split_beta')
subgoal using ‹S (Suc i) ⊆ T› by (auto intro!: lipschitz)
subgoal by (rule subdivide_lipschitz_lemma) (auto simp add: step_def divide_simps algebra S_def)
done
note ui
moreover
have mem_SI: "t ∈ closed_segment ?i ?si ⟹ t ∈ S (if t = ?i then i else Suc i)" for t
by (auto simp: S_def)
have min_S: "(if t = t0 + real i * step then i else Suc i) ≤ y"
if "t ∈ closed_segment (t0 + real i * step) (t0 + (1 + real i) * step)"
"t ∈ S y"
for y t
apply (cases "t = t0 + real i * step")
subgoal using that ‹step ≠ 0›
by (auto simp add: S_def closed_segment_eq_real_ivl algebra_simps zero_le_mult_iff split: if_splits )
subgoal premises ne
proof (cases)
assume "step > 0"
with that have "t0 + real i * step ≤ t" "t ≤ t0 + (1 + real i) * step"
"t0 + real (y - Suc 0) * step ≤ t" "t ≤ t0 + real y * step"
by (auto simp: closed_segment_eq_real_ivl S_def)
then have "real i * step < real y * step" using ‹step > 0› ne
by arith
then show ?thesis using ‹step > 0› that by (auto simp add: closed_segment_eq_real_ivl S_def)
next
assume "¬ step > 0" with ‹step ≠ 0› have "step < 0" by simp
with that have "t0 + (1 + real i) * step ≤ t" "t ≤ t0 + real i * step"
"t0 + real y * step ≤ t" "t ≤ t0 + real (y - Suc 0) * step" using ne
by (auto simp: closed_segment_eq_real_ivl S_def diff_Suc zero_le_mult_iff split: if_splits nat.splits)
then have "real y * step < real i * step"
using ‹step < 0› ne
by arith
then show ?thesis using ‹step < 0› by (auto simp add: closed_segment_eq_real_ivl S_def)
qed
done
have "(?sol usolves_ode f from ?i) (closed_segment ?i ?si) X"
apply (subst usolves_ode_cong)
apply (subst Least_equality)
apply (rule mem_SI) apply assumption
apply (rule min_S) apply assumption apply assumption
apply (rule refl)
apply (rule refl)
apply (rule refl)
apply (rule refl)
apply (rule refl)
apply (subst usolves_ode_cong[where y="psolution (Suc i)"])
using l.fixed_point_iv[unfolded Least_eq]
apply (simp add: S_def; fail)
apply (rule refl)
apply (rule refl)
apply (rule refl)
apply (rule refl)
using l.fixed_point_usolves_ode
apply -
apply (simp)
apply (simp add: S_def)
done
moreover have "t ∈ {t0 + real i * step--t0 + (step + real i * step)} ⟹
t ∈ {t0--t0 + real i * step} ⟹ t = t0 + real i * step" for t
by (subst segment_inter[rotated], assumption, assumption) (auto simp: algebra_simps)
ultimately
have "((λt. if t ∈ closed_segment t0 ?i then ?sol t else ?sol t)
usolves_ode
(λt. if t ∈ closed_segment t0 ?i then f t else f t) from t0)
(closed_segment t0 ?i ∪ closed_segment ?i ?si) X"
by (intro connection_usolves_ode[where t="?i"]) (auto simp: algebra_simps split: if_split_asm)
also have "closed_segment t0 ?i ∪ closed_segment ?i ?si = closed_segment t0 ?si"
apply (rule closed_segment_Un)
by (cases "step < 0")
(auto simp: closed_segment_eq_real_ivl zero_le_mult_iff mult_le_0_iff
intro!: mult_right_mono
split: if_split_asm)
finally show ?case by simp
qed
qed
lemma psolutions_usolves_ode: "(psolutions usolves_ode f from t0) {t0 -- t1} X"
proof -
let ?T = "closed_segment t0 (t0 + real (Suc subdivide_count) * step)"
have "(psolutions usolves_ode f from t0) ?T X"
by (rule psolutions_usolves_until_step) simp
also have "?T = {t0 -- t1}" unfolding last_step ..
finally show ?thesis .
qed
end
definition "solution t = (if t ≤ t0 then psolutions tmin t else psolutions tmax t)"
lemma solution_eq_left: "tmin ≤ t ⟹ t ≤ t0 ⟹ solution t = psolutions tmin t"
by (simp add: solution_def)
lemma solution_eq_right: "t0 ≤ t ⟹ t ≤ tmax ⟹ solution t = psolutions tmax t"
by (simp add: solution_def psolutions_def)
lemma solution_usolves_ode: "(solution usolves_ode f from t0) T X"
proof -
from psolutions_usolves_ode[OF tmin(2)] tmin_le_t0
have u1: "(psolutions tmin usolves_ode f from t0) {tmin .. t0} X"
by (auto simp: closed_segment_eq_real_ivl split: if_splits)
from psolutions_usolves_ode[OF tmax(2)] tmin_le_t0
have u2: "(psolutions tmax usolves_ode f from t0) {t0 .. tmax} X"
by (auto simp: closed_segment_eq_real_ivl split: if_splits)
have "(solution usolves_ode f from t0) ({tmin .. t0} ∪ {t0 .. tmax}) (X ∪ X)"
apply (rule usolves_ode_union_closed[where t=t0])
subgoal by (subst usolves_ode_cong[where y="psolutions tmin"]) (auto simp: solution_eq_left u1)
subgoal
using u2
by (rule usolves_ode_congI) (auto simp: solution_eq_right)
subgoal by simp
subgoal by simp
subgoal by simp
done
also have "{tmin .. t0} ∪ {t0 .. tmax} = T"
by (simp add: T_split[symmetric])
finally show ?thesis by simp
qed
lemma solution_solves_ode: "(solution solves_ode f) T X"
by (rule usolves_odeD[OF solution_usolves_ode])
lemma solution_iv[simp]: "solution t0 = x0"
by (auto simp: solution_def psolutions_def)
end
subsection ‹Picard-Lindeloef for @{term "X = UNIV"}›
text‹\label{sec:pl-us}›
locale unique_on_strip =
compact_interval T +
continuous_rhs T UNIV f +
global_lipschitz T UNIV f L
for t0 and T and f::"real ⇒ 'a ⇒ 'a::banach" and L +
assumes iv_time: "t0 ∈ T"
begin
sublocale unique_on_closed t0 T x0 f UNIV L for x0
by (-, unfold_locales) (auto simp: iv_time)
end
subsection ‹Picard-Lindeloef on cylindric domain›
text‹\label{sec:pl-rect}›
locale solution_in_cylinder =
continuous_rhs T "cball x0 b" f +
compact_interval T
for t0 T x0 b and f::"real ⇒ 'a ⇒ 'a::banach" +
fixes X B
defines "X ≡ cball x0 b"
assumes initial_time_in: "t0 ∈ T"
assumes norm_f: "⋀x t. t ∈ T ⟹ x ∈ X ⟹ norm (f t x) ≤ B"
assumes b_pos: "b ≥ 0"
assumes e_bounded: "⋀t. t ∈ T ⟹ dist t t0 ≤ b / B"
begin
lemmas cylinder = X_def
lemma B_nonneg: "B ≥ 0"
proof -
have "0 ≤ norm (f t0 x0)" by simp
also from b_pos norm_f have "... ≤ B" by (simp add: initial_time_in X_def)
finally show ?thesis by simp
qed
lemma in_bounds_derivativeI:
assumes "t ∈ T"
assumes init: "x t0 = x0"
assumes cont: "continuous_on (closed_segment t0 t) x"
assumes solves: "(x has_vderiv_on (λs. f s (y s))) (open_segment t0 t)"
assumes y_bounded: "⋀ξ. ξ ∈ closed_segment t0 t ⟹ x ξ ∈ X ⟹ y ξ ∈ X"
shows "x t ∈ cball x0 (B * abs (t - t0))"
proof cases
assume "b = 0 ∨ B = 0" with assms e_bounded T_def have "t = t0"
by auto
thus ?thesis using b_pos init by simp
next
assume "¬(b = 0 ∨ B = 0)"
hence "b > 0" "B > 0" using B_nonneg b_pos by auto
show ?thesis
proof cases
assume "t0 ≠ t"
then have b_less: "B * abs (t - t0) ≤ b"
using b_pos e_bounded using ‹b > 0› ‹B > 0› ‹t ∈ T›
by (auto simp: field_simps initial_time_in dist_real_def abs_real_def closed_segment_eq_real_ivl split: if_split_asm)
define b where "b ≡ B * abs (t - t0)"
have "b > 0" using ‹t0 ≠ t› by (auto intro!: mult_pos_pos simp: algebra_simps b_def ‹B > 0›)
from cont
have closed: "closed (closed_segment t0 t ∩ ((λs. norm (x s - x t0)) -` {b..}))"
by (intro continuous_closed_preimage continuous_intros closed_segment)
have exceeding: "{s ∈ closed_segment t0 t. norm (x s - x t0) ∈ {b..}} ⊆ {t}"
proof (rule ccontr)
assume "¬{s ∈ closed_segment t0 t. norm (x s - x t0) ∈ {b..}} ⊆ {t}"
hence notempty: "(closed_segment t0 t ∩ ((λs. norm (x s - x t0)) -` {b..})) ≠ {}"
and not_max: "{s ∈ closed_segment t0 t. norm (x s - x t0) ∈ {b..}} ≠ {t}"
by auto
obtain s where s_bound: "s ∈ closed_segment t0 t"
and exceeds: "norm (x s - x t0) ∈ {b..}"
and min: "∀t2∈closed_segment t0 t.
norm (x t2 - x t0) ∈ {b..} ⟶ dist t0 s ≤ dist t0 t2"
by (rule distance_attains_inf[OF closed notempty, of t0]) blast
have "s ≠ t0" using exceeds ‹b > 0› by auto
have st: "closed_segment t0 t ⊇ open_segment t0 s" using s_bound
by (auto simp: closed_segment_eq_real_ivl open_segment_eq_real_ivl)
from cont have cont: "continuous_on (closed_segment t0 s) x"
by (rule continuous_on_subset)
(insert b_pos closed_segment_subset_domain s_bound, auto simp: closed_segment_eq_real_ivl)
have bnd_cont: "continuous_on (closed_segment t0 s) ((*) B)"
and bnd_deriv: "((*) B has_vderiv_on (λ_. B)) (open_segment t0 s)"
by (auto intro!: continuous_intros derivative_eq_intros
simp: has_vector_derivative_def has_vderiv_on_def)
{
fix ss assume ss: "ss ∈ open_segment t0 s"
with st have "ss ∈ closed_segment t0 t" by auto
have less_b: "norm (x ss - x t0) < b"
proof (rule ccontr)
assume "¬ norm (x ss - x t0) < b"
hence "norm (x ss - x t0) ∈ {b..}" by auto
from min[rule_format, OF ‹ss ∈ closed_segment t0 t› this]
show False using ss ‹s ≠ t0›
by (auto simp: dist_real_def open_segment_eq_real_ivl split_ifs)
qed
have "norm (f ss (y ss)) ≤ B"
apply (rule norm_f)
subgoal using ss st closed_segment_subset_domain[OF initial_time_in ‹t ∈ T›] by auto
subgoal using ss st b_less less_b
by (intro y_bounded)
(auto simp: X_def dist_norm b_def init norm_minus_commute mem_cball)
done
} note bnd = this
have subs: "open_segment t0 s ⊆ open_segment t0 t" using s_bound ‹s ≠ t0›
by (auto simp: closed_segment_eq_real_ivl open_segment_eq_real_ivl)
with differentiable_bound_general_open_segment[OF cont bnd_cont has_vderiv_on_subset[OF solves subs]
bnd_deriv bnd]
have "norm (x s - x t0) ≤ B * ¦s - t0¦"
by (auto simp: algebra_simps[symmetric] abs_mult B_nonneg)
also
have "s ≠ t"
using s_bound exceeds min not_max
by (auto simp: dist_norm closed_segment_eq_real_ivl split_ifs)
hence "B * ¦s - t0¦ < ¦t - t0¦ * B"
using s_bound ‹B > 0›
by (intro le_neq_trans)
(auto simp: algebra_simps closed_segment_eq_real_ivl split_ifs
intro!: mult_left_mono)
finally have "norm (x s - x t0) < ¦t - t0¦ * B" .
moreover
{
have "b ≥ ¦t - t0¦ * B" by (simp add: b_def algebra_simps)
also from exceeds have "norm (x s - x t0) ≥ b" by simp
finally have "¦t - t0¦ * B ≤ norm (x s - x t0)" .
}
ultimately show False by simp
qed note mvt_result = this
from cont assms
have cont_diff: "continuous_on (closed_segment t0 t) (λxa. x xa - x t0)"
by (auto intro!: continuous_intros)
have "norm (x t - x t0) ≤ b"
proof (rule ccontr)
assume H: "¬ norm (x t - x t0) ≤ b"
hence "b ∈ closed_segment (norm (x t0 - x t0)) (norm (x t - x t0))"
using assms T_def ‹0 < b›
by (auto simp: closed_segment_eq_real_ivl )
from IVT'_closed_segment_real[OF this continuous_on_norm[OF cont_diff]]
obtain s where s: "s ∈ closed_segment t0 t" "norm (x s - x t0) = b"
using ‹b > 0› by auto
have "s ∈ {s ∈ closed_segment t0 t. norm (x s - x t0) ∈ {b..}}"
using s ‹t ∈ T› by (auto simp: initial_time_in)
with mvt_result have "s = t" by blast
hence "s = t" using s ‹t ∈ T› by (auto simp: initial_time_in)
with s H show False by simp
qed
hence "x t ∈ cball x0 b" using init
by (auto simp: dist_commute dist_norm[symmetric] mem_cball)
thus "x t ∈ cball x0 (B * abs (t - t0))" unfolding cylinder b_def .
qed (simp add: init[symmetric])
qed
lemma in_bounds_derivative_globalI:
assumes "t ∈ T"
assumes init: "x t0 = x0"
assumes cont: "continuous_on (closed_segment t0 t) x"
assumes solves: "(x has_vderiv_on (λs. f s (y s))) (open_segment t0 t)"
assumes y_bounded: "⋀ξ. ξ ∈ closed_segment t0 t ⟹ x ξ ∈ X ⟹ y ξ ∈ X"
shows "x t ∈ X"
proof -
from in_bounds_derivativeI[OF assms]
have "x t ∈ cball x0 (B * abs (t - t0))" .
moreover have "B * abs (t - t0) ≤ b" using e_bounded b_pos B_nonneg ‹t ∈ T›
by (cases "B = 0")
(auto simp: field_simps initial_time_in dist_real_def abs_real_def closed_segment_eq_real_ivl split: if_splits)
ultimately show ?thesis by (auto simp: cylinder mem_cball)
qed
lemma integral_in_bounds:
assumes "t ∈ T" "x t0 = x0" "x ∈ {t0 -- t} → X"
assumes cont[continuous_intros]: "continuous_on ({t0 -- t}) x"
shows "x t0 + ivl_integral t0 t (λt. f t (x t)) ∈ X" (is "_ + ?ix t ∈ X")
proof cases
assume "t = t0"
thus ?thesis by (auto simp: cylinder b_pos assms)
next
assume "t ≠ t0"
from closed_segment_subset_domain[OF initial_time_in]
have cont_f:"continuous_on {t0 -- t} (λt. f t (x t))"
using assms
by (intro continuous_intros)
(auto intro: cont continuous_on_subset[OF continuous] simp: cylinder split: if_splits)
from closed_segment_subset_domain[OF initial_time_in ‹t ∈ T›]
have subsets: "s ∈ {t0--t} ⟹ s ∈ T" "s ∈ open_segment t0 t ⟹ s ∈ {t0--t}" for s
by (auto simp: closed_segment_eq_real_ivl open_segment_eq_real_ivl initial_time_in split: if_split_asm)
show ?thesis
unfolding ‹x t0 = _›
using assms ‹t ≠ t0›
by (intro in_bounds_derivative_globalI[where y=x and x="λt. x0 + ?ix t"])
(auto simp: initial_time_in subsets cylinder has_vderiv_on_def
split: if_split_asm
intro!: cont_f has_vector_derivative_const integrable_continuous_closed_segment
has_vector_derivative_within_subset[OF ivl_integral_has_vector_derivative]
has_vector_derivative_add[THEN has_vector_derivative_eq_rhs]
continuous_intros indefinite_ivl_integral_continuous)
qed
lemma solves_in_cone:
assumes "t ∈ T"
assumes init: "x t0 = x0"
assumes cont: "continuous_on (closed_segment t0 t) x"
assumes solves: "(x has_vderiv_on (λs. f s (x s))) (open_segment t0 t)"
shows "x t ∈ cball x0 (B * abs (t - t0))"
using assms
by (rule in_bounds_derivativeI)
lemma is_solution_in_cone:
assumes "t ∈ T"
assumes sol: "(x solves_ode f) (closed_segment t0 t) Y" and iv: "x t0 = x0"
shows "x t ∈ cball x0 (B * abs (t - t0))"
using solves_odeD[OF sol] ‹t ∈ T›
by (intro solves_in_cone)
(auto intro!: assms vderiv_on_continuous_on segment_open_subset_closed
intro: has_vderiv_on_subset simp: initial_time_in)
lemma cone_subset_domain:
assumes "t ∈ T"
shows "cball x0 (B * ¦t - t0¦) ⊆ X"
using e_bounded[OF assms] B_nonneg b_pos
unfolding cylinder
by (intro subset_cball) (auto simp: dist_real_def divide_simps algebra_simps split: if_splits)
lemma is_solution_in_domain:
assumes "t ∈ T"
assumes sol: "(x solves_ode f) (closed_segment t0 t) Y" and iv: "x t0 = x0"
shows "x t ∈ X"
using is_solution_in_cone[OF assms] cone_subset_domain[OF ‹t ∈ T›]
by (rule rev_subsetD)
lemma solves_ode_on_subset_domain:
assumes sol: "(x solves_ode f) S Y" and iv: "x t0 = x0"
and ivl: "t0 ∈ S" "is_interval S" "S ⊆ T"
shows "(x solves_ode f) S X"
proof (rule solves_odeI)
show "(x has_vderiv_on (λt. f t (x t))) S" using solves_odeD(1)[OF sol] .
show "x s ∈ X" if s: "s ∈ S" for s
proof -
from s assms have "s ∈ T"
by auto
moreover
have "{t0--s} ⊆ S"
by (rule closed_segment_subset) (auto simp: s assms is_interval_convex)
with sol have "(x solves_ode f) {t0--s} Y"
using order_refl
by (rule solves_ode_on_subset)
ultimately
show ?thesis using iv
by (rule is_solution_in_domain)
qed
qed
lemma usolves_ode_on_subset:
assumes x: "(x usolves_ode f from t0) T X" and iv: "x t0 = x0"
assumes "t0 ∈ S" "is_interval S" "S ⊆ T" "X ⊆ Y"
shows "(x usolves_ode f from t0) S Y"
proof (rule usolves_odeI)
show "(x solves_ode f) S Y" by (rule solves_ode_on_subset[OF usolves_odeD(1)[OF x]]; fact)
show "t0 ∈ S" "is_interval S" by fact+
fix z t assume "{t0 -- t} ⊆ S" and z: "(z solves_ode f) {t0--t} Y" "z t0 = x t0"
then have "z t0 = x0" "t0 ∈ {t0--t}" "is_interval {t0--t}" "{t0--t} ⊆ T"
using iv ‹S ⊆ T› by (auto simp: is_interval_convex_1)
with z(1) have zX: "(z solves_ode f) {t0 -- t} X"
by (rule solves_ode_on_subset_domain)
show "z t = x t"
apply (rule usolves_odeD(4)[OF x _ _ _ zX])
using ‹{t0 -- t} ⊆ S› ‹S ⊆ T›
by (auto simp: is_interval_convex_1 ‹z t0 = x t0›)
qed
lemma usolves_ode_on_superset_domain:
assumes "(x usolves_ode f from t0) T X" and iv: "x t0 = x0"
assumes "X ⊆ Y"
shows "(x usolves_ode f from t0) T Y"
using assms(1,2) usolves_odeD(2,3)[OF assms(1)] order_refl assms(3)
by (rule usolves_ode_on_subset)
end
locale unique_on_cylinder =
solution_in_cylinder t0 T x0 b f X B +
global_lipschitz T X f L
for t0 T x0 b X f B L
begin
sublocale unique_on_closed t0 T x0 f X L
apply unfold_locales
subgoal by (simp add: initial_time_in)
subgoal by (simp add: X_def b_pos)
subgoal by (auto intro!: integral_in_bounds simp: initial_time_in)
subgoal by (auto intro!: continuous_intros simp: split_beta' X_def)
subgoal by (simp add: X_def)
done
end
locale derivative_on_prod =
fixes T X and f::"real ⇒ 'a::banach ⇒ 'a" and f':: "real × 'a ⇒ (real × 'a) ⇒ 'a"
assumes f': "⋀tx. tx ∈ T × X ⟹ ((λ(t, x). f t x) has_derivative (f' tx)) (at tx within (T × X))"
begin
lemma f'_comp[derivative_intros]:
"(g has_derivative g') (at s within S) ⟹ (h has_derivative h') (at s within S) ⟹
s ∈ S ⟹ (⋀x. x ∈ S ⟹ g x ∈ T) ⟹ (⋀x. x ∈ S ⟹ h x ∈ X) ⟹
((λx. f (g x) (h x)) has_derivative (λy. f' (g s, h s) (g' y, h' y))) (at s within S)"
apply (rule has_derivative_in_compose2[OF f' _ _ has_derivative_Pair, unfolded split_beta' fst_conv snd_conv, of g h S s g' h'])
apply auto
done
lemma derivative_on_prod_subset:
assumes "X' ⊆ X"
shows "derivative_on_prod T X' f f'"
using assms
by (unfold_locales) (auto intro!: derivative_eq_intros)
end
end