# Theory ODE_Auxiliarities

section ‹Auxiliary Lemmas›
theory ODE_Auxiliarities
imports
"HOL-Analysis.Analysis"
"HOL-Library.Float"
"List-Index.List_Index"
Affine_Arithmetic.Affine_Arithmetic_Auxiliarities
Affine_Arithmetic.Executable_Euclidean_Space
begin

instantiation prod :: (zero_neq_one, zero_neq_one) zero_neq_one
begin

definition "1 = (1, 1)"

instance by standard (simp add: zero_prod_def one_prod_def)
end

subsection ‹there is no inner product for type @{typ "'a ⇒⇩L 'b"}›

lemma (in real_inner) parallelogram_law: "(norm (x + y))⇧2 + (norm (x - y))⇧2 = 2 * (norm x)⇧2 + 2 * (norm y)⇧2"
proof -
have "(norm (x + y))⇧2 + (norm (x - y))⇧2 = inner (x + y) (x + y) + inner (x - y) (x - y)"
also have "… = 2 * (norm x)⇧2 + 2 * (norm y)⇧2"
finally show ?thesis .
qed

locale no_real_inner
begin

lift_definition fstzero::"(real*real) ⇒⇩L (real*real)" is "λ(x, y). (x, 0)"
by (auto intro!: bounded_linearI')

lemma [simp]: "fstzero (a, b) = (a, 0)"
by transfer simp

lift_definition zerosnd::"(real*real) ⇒⇩L (real*real)" is "λ(x, y). (0, y)"
by (auto intro!: bounded_linearI')

lemma [simp]: "zerosnd (a, b) = (0, b)"
by transfer simp

lemma fstzero_add_zerosnd: "fstzero + zerosnd = id_blinfun"
by transfer auto

lemma norm_fstzero_zerosnd: "norm fstzero = 1" "norm zerosnd = 1" "norm (fstzero - zerosnd) = 1"
by (rule norm_blinfun_eqI[where x="(1, 0)"]) (auto simp: norm_Pair blinfun.bilinear_simps
intro: norm_blinfun_eqI[where x="(0, 1)"] norm_blinfun_eqI[where x="(1, 0)"])

text ‹compare with @{thm parallelogram_law}›

lemma "(norm (fstzero + zerosnd))⇧2 + (norm (fstzero - zerosnd))⇧2 ≠
2 * (norm fstzero)⇧2 + 2 * (norm zerosnd)⇧2"

end

subsection ‹Topology›

subsection ‹Vector Spaces›

lemma ex_norm_eq_1: "∃x. norm (x::'a::{real_normed_vector, perfect_space}) = 1"
by (metis vector_choose_size zero_le_one)

subsection ‹Reals›

subsection ‹Balls›

text ‹sometimes @{thm mem_ball} etc. are not good ‹[simp]› rules (although they are often useful):
not sure that inequalities are simpler'' than set membership (distorts automatic reasoning
when only sets are involved)›
lemmas [simp del] = mem_ball mem_cball mem_sphere mem_ball_0 mem_cball_0

subsection ‹Boundedness›

lemma bounded_subset_cboxE:
assumes "⋀i. i ∈ Basis ⟹ bounded ((λx. x ∙ i)  X)"
obtains a b where "X ⊆ cbox a b"
proof -
have "⋀i. i ∈ Basis ⟹ ∃a b. ((λx. x ∙ i)  X) ⊆ {a..b}"
by (metis box_real(2) box_subset_cbox subset_trans bounded_subset_box_symmetric[OF assms] )
then obtain a b where bnds: "⋀i. i ∈ Basis ⟹ ((λx. x ∙ i)  X) ⊆ {a i .. b i}"
by metis
then have "X ⊆ {x. ∀i∈Basis. x ∙ i ∈ {a i .. b i}}"
by force
also have "… = cbox (∑i∈Basis. a i *⇩R i) (∑i∈Basis. b i *⇩R i)"
by (auto simp: cbox_def)
finally show ?thesis ..
qed

lemma
bounded_euclideanI:
assumes "⋀i. i ∈ Basis ⟹ bounded ((λx. x ∙ i)  X)"
shows "bounded X"
proof -
from bounded_subset_cboxE[OF assms] obtain a b where "X ⊆ cbox a b" .
with bounded_cbox show ?thesis by (rule bounded_subset)
qed

subsection ‹Intervals›

notation closed_segment ("(1{_--_})")
notation open_segment ("(1{_<--<_})")

lemma min_zero_mult_nonneg_le: "0 ≤ h' ⟹ h' ≤ h ⟹ min 0 (h * k::real) ≤ h' * k"
by (metis dual_order.antisym le_cases min_le_iff_disj mult_eq_0_iff mult_le_0_iff
mult_right_mono_neg)

lemma max_zero_mult_nonneg_le: "0 ≤ h' ⟹ h' ≤ h ⟹ h' * k ≤ max 0 (h * k::real)"
by (metis dual_order.antisym le_cases le_max_iff_disj mult_eq_0_iff mult_right_mono
zero_le_mult_iff)

lemmas closed_segment_eq_real_ivl = closed_segment_eq_real_ivl

lemma bdd_above_is_intervalI: "bdd_above I" if "is_interval I" "a ≤ b" "a ∈ I" "b ∉ I" for I::"real set"
by (meson bdd_above_def is_interval_1 le_cases that)

lemma bdd_below_is_intervalI: "bdd_below I" if "is_interval I" "a ≤ b" "a ∉ I" "b ∈ I" for I::"real set"
by (meson bdd_below_def is_interval_1 le_cases that)

subsection ‹Extended Real Intervals›

subsection ‹Euclidean Components›

subsection ‹Operator Norm›

subsection ‹Limits›

lemma eventually_open_cball:
assumes "open X"
assumes "x ∈ X"
shows "eventually (λe. cball x e ⊆ X) (at_right 0)"
proof -
from open_contains_cball_eq[OF assms(1)] assms(2)
obtain e where "e > 0" "cball x e ⊆ X" by auto
thus ?thesis
by (auto simp: eventually_at dist_real_def mem_cball intro!: exI[where x=e])
qed

subsection ‹Continuity›

subsection ‹Derivatives›

lemma
if_eventually_has_derivative:
assumes "(f has_derivative F') (at x within S)"
assumes "∀⇩F x in at x within S. P x" "P x" "x ∈ S"
shows "((λx. if P x then f x else g x) has_derivative F') (at x within S)"
using assms(1)
apply (rule has_derivative_transform_eventually)
subgoal using assms(2) by eventually_elim auto
by (auto simp: assms)

lemma norm_le_in_cubeI: "norm x ≤ norm y"
if "⋀i. i ∈ Basis ⟹ abs (x ∙ i) ≤ abs (y ∙ i)" for x y
unfolding norm_eq_sqrt_inner
apply (subst euclidean_inner)
apply (subst (3) euclidean_inner)
using that
by (auto intro!: sum_mono simp: abs_le_square_iff power2_eq_square[symmetric])

lemma has_derivative_partials_euclidean_convexI:
fixes f::"'a::euclidean_space ⇒ 'b::real_normed_vector"
assumes f': "⋀i x xi. i ∈ Basis ⟹ (∀j∈Basis. x ∙ j ∈ X j) ⟹ xi = x ∙ i ⟹
((λp. f (x + (p - x ∙ i) *⇩R i)) has_vector_derivative f' i x) (at xi within X i)"
assumes df_cont: "⋀i. i ∈ Basis ⟹ (f' i ⤏ (f' i x)) (at x within {x. ∀j∈Basis. x ∙ j ∈ X j})"
assumes "⋀i. i ∈ Basis ⟹ x ∙ i ∈ X i"
assumes "⋀i. i ∈ Basis ⟹ convex (X i)"
shows "(f has_derivative (λh. ∑j∈Basis. (h ∙ j) *⇩R f' j x)) (at x within {x. ∀j∈Basis. x ∙ j ∈ X j})"
(is "_ (at x within ?S)")
proof (rule has_derivativeI)
show "bounded_linear (λh. ∑j∈Basis. (h ∙ j) *⇩R f' j x)"
by (auto intro!: bounded_linear_intros)

obtain E where [simp]: "set E = (Basis::'a set)" "distinct E"
using finite_distinct_list[OF finite_Basis] by blast

have [simp]: "length E = DIM('a)"
using ‹distinct E› distinct_card by fastforce
have [simp]: "E ! j ∈ Basis" if "j < DIM('a)" for j
by (metis ‹length E = DIM('a)› ‹set E = Basis› nth_mem that)
have "convex ?S"
by (rule convex_prod) (use assms in auto)

have sum_Basis_E: "sum g Basis = (∑j<DIM('a). g (E ! j))" for g
apply (rule sum.reindex_cong[OF _ _ refl])
apply (auto simp: inj_on_nth)
by (metis ‹distinct E› ‹length E = DIM('a)› ‹set E = Basis› bij_betw_def bij_betw_nth)

have segment: "∀⇩F x' in at x within ?S. x' ∈ ?S" "∀⇩F x' in at x within ?S. x' ≠ x"
unfolding eventually_at_filter by auto

show "((λy. (f y - f x - (∑j∈Basis. ((y - x) ∙ j) *⇩R f' j x)) /⇩R norm (y - x)) ⤏ 0) (at x within {x. ∀j∈Basis. x ∙ j ∈ X j})"
apply (rule tendstoI)
unfolding norm_conv_dist[symmetric]
proof -
fix e::real
assume "e > 0"
define B where "B = e / norm (2*DIM('a) + 1)"
with ‹e > 0› have B_thms: "B > 0" "2 * DIM('a) * B < e" "B ≥ 0"
by (auto simp: divide_simps algebra_simps B_def)
define B' where "B' = B / 2"
have "B' > 0" by (simp add: B'_def ‹0 < B›)
have "∀i ∈ Basis. ∀⇩F xa in at x within {x. ∀j∈Basis. x ∙ j ∈ X j}. dist (f' i xa) (f' i x) < B'"
apply (rule ballI)
subgoal premises prems using df_cont[OF prems, THEN tendstoD, OF ‹0 < B'›] .
done
from eventually_ball_finite[OF finite_Basis this]
have "∀⇩F x' in at x within {x. ∀j∈Basis. x ∙ j ∈ X j}. ∀j∈Basis. dist (f' j x') (f' j x) < B'" .
then obtain d where "d > 0"
and "⋀x' j. x' ∈ {x. ∀j∈Basis. x ∙ j ∈ X j} ⟹ x' ≠ x ⟹ dist x' x < d ⟹ j ∈ Basis ⟹ dist (f' j x') (f' j x) < B'"
using ‹0 < B'›
by (auto simp: eventually_at)
then have B': "x' ∈ {x. ∀j∈Basis. x ∙ j ∈ X j} ⟹ dist x' x < d ⟹ j ∈ Basis ⟹ dist (f' j x') (f' j x) < B'" for x' j
by (cases "x' = x", auto simp add: ‹0 < B'›)
then have B: "norm (f' j x' - f' j y) < B" if
"(⋀j. j ∈ Basis ⟹ x' ∙ j ∈ X j)"
"(⋀j. j ∈ Basis ⟹ y ∙ j ∈ X j)"
"dist x' x < d"
"dist y x < d"
"j ∈ Basis"
for x' y j
proof -
have "dist (f' j x') (f' j x) < B'" "dist (f' j y) (f' j x) < B'"
using that
by (auto intro!: B')
then have "dist (f' j x') (f' j y) < B' + B'" by norm
also have "… = B" by (simp add: B'_def)
finally show ?thesis by (simp add: dist_norm)
qed
have "∀⇩F x' in at x within {x. ∀j∈Basis. x ∙ j ∈ X j}. dist x' x < d"
by (rule tendstoD[OF tendsto_ident_at ‹d > 0›])
with segment
show "∀⇩F x' in at x within {x. ∀j∈Basis. x ∙ j ∈ X j}.
norm ((f x' - f x - (∑j∈Basis. ((x' - x) ∙ j) *⇩R f' j x)) /⇩R norm (x' - x)) < e"
proof eventually_elim
case (elim x')
then have os_subset: "open_segment x x' ⊆ ?S"
using ‹convex ?S› assms(3)
unfolding convex_contains_open_segment
by auto
then have cs_subset: "closed_segment x x' ⊆ ?S"
using elim assms(3) by (auto simp add: open_segment_def)
have csc_subset: "closed_segment (x' ∙ i) (x ∙ i) ⊆ X i" if i: "i ∈ Basis" for i
apply (rule closed_segment_subset)
using cs_subset elim assms(3,4) that
by (auto )
have osc_subset: "open_segment (x' ∙ i) (x ∙ i) ⊆ X i" if i: "i ∈ Basis" for i
using segment_open_subset_closed csc_subset[OF i]
by (rule order_trans)

define h where "h = x' - x"
define z where "z j = (∑k<j. (h ∙ E ! k) *⇩R (E ! k))" for j
define g where "g j t = (f (x + z j + (t - x ∙ E ! j) *⇩R E ! j))" for j t
have z: "z j ∙ E ! j = 0" if "j < DIM('a)" for j
using that
by (auto simp: z_def h_def algebra_simps inner_sum_left inner_Basis if_distrib
nth_eq_iff_index_eq
sum.delta
intro!: euclidean_eqI[where 'a='a]
cong: if_cong)
from distinct_Ex1[OF ‹distinct E›, unfolded ‹set E = Basis› Ex1_def ‹length E = _›]
obtain index where
index: "⋀i. i ∈ Basis ⟹ i = E ! index i" "⋀i. i ∈ Basis ⟹ index i < DIM('a)"
and unique: "⋀i j. i ∈ Basis ⟹ j < DIM('a) ⟹ E ! j = i ⟹ j = index i"
by metis
have nth_eq_iff_index: "E ! k = i ⟷ index i = k" if "i ∈ Basis" "k < DIM('a)" for k i
using unique[OF that] index[OF ‹i ∈ Basis›]
by auto
have z_inner: "z j ∙ i = (if j ≤ index i then 0 else h ∙ i)" if "j < DIM('a)" "i ∈ Basis" for j i
using that index[of i]
by (auto simp: z_def h_def algebra_simps inner_sum_left inner_Basis if_distrib
sum.delta nth_eq_iff_index
intro!: euclidean_eqI[where 'a='a]
cong: if_cong)
have z_mem: "j < DIM('a) ⟹ ja ∈ Basis ⟹ x ∙ ja + z j ∙ ja ∈ X ja" for j ja
using csc_subset
by (auto simp: z_inner h_def algebra_simps)
have "norm (x' - x) < d"
using elim by (simp add: dist_norm)
have norm_z': "y ∈ closed_segment (x ∙ E ! j) (x' ∙ E ! j) ⟹ norm (z j + y *⇩R E ! j - (x ∙ E ! j) *⇩R E ! j) < d"
if "j < DIM('a)"
for j y
apply (rule le_less_trans[OF _ ‹norm (x' - x) < d›])
apply (rule norm_le_in_cubeI)
apply (auto simp: inner_diff_left inner_add_left inner_Basis that z)
subgoal by (auto simp: closed_segment_eq_real_ivl split: if_splits)
subgoal for i
using that
by (auto simp: z_inner h_def algebra_simps)
done
have norm_z: "norm (z j) < d" if "j < DIM('a)" for j
using norm_z'[OF that ends_in_segment(1)]
by (auto simp: z_def)
{
fix j
assume j: "j < DIM('a)"
have eq: "(x + z j + ((y - (x + z j)) ∙ E ! j) *⇩R E ! j +
(p - (x + z j + ((y - (x + z j)) ∙ E ! j) *⇩R E ! j) ∙ E ! j) *⇩R
E ! j) = (x + z j + (p - (x ∙ E ! j)) *⇩R E ! j)" for y p
by (auto simp: algebra_simps j z)
have f_has_derivative: "((λp. f (x + z j + (p - x ∙ E ! j) *⇩R E ! j)) has_derivative (λxa. xa *⇩R f' (E ! j) (x + z j + ((y *⇩R E ! j - (x + z j)) ∙ E ! j) *⇩R E ! j)))
(at y within closed_segment (x ∙ E ! j) (x' ∙ E ! j))"
if "y ∈ closed_segment (x ∙ E ! j) (x' ∙ E ! j)"
for y
apply (rule has_derivative_subset)
apply (rule f'[unfolded has_vector_derivative_def,
where x= "x + z j + ((y *⇩R E!j - (x + z j))∙ E!j) *⇩R E ! j" and i="E ! j", unfolded eq])
subgoal
using that
apply (auto simp: algebra_simps z j inner_Basis)
using closed_segment_commute ‹E ! j ∈ Basis› csc_subset apply blast
subgoal by (auto simp: algebra_simps z j inner_Basis)
subgoal
apply (auto simp: algebra_simps z j inner_Basis)
using closed_segment_commute ‹⋀j. j < DIM('a) ⟹ E ! j ∈ Basis› csc_subset j apply blast
done
done
have *: "((xa *⇩R E ! j - (x + z j)) ∙ E ! j) = xa - x ∙ E ! j" for xa
by (auto simp: algebra_simps z j)
have g': "(g j has_vector_derivative (f' (E ! j) (x + z j + (xa - x ∙ E ! j) *⇩R E ! j)))
(at xa within (closed_segment (x∙E!j) (x'∙E!j)))"
(is "(_ has_vector_derivative ?g' j xa) _")
if "xa ∈ closed_segment (x∙E!j) (x'∙E!j)" for xa
using that
by (auto simp: has_vector_derivative_def g_def[abs_def] *
intro!: derivative_eq_intros f_has_derivative[THEN has_derivative_eq_rhs])
define g' where "g' j = ?g' j" for j
with g' have g': "(g j has_vector_derivative g' j t) (at t within closed_segment (x∙E!j) (x'∙E!j))"
if "t ∈ closed_segment (x∙E!j) (x'∙E!j)"
for t
have cont_bound: "⋀y. y∈closed_segment (x ∙ E ! j) (x' ∙ E ! j) ⟹ norm (g' j y - g' j (x ∙ E ! j)) ≤ B"
apply (auto simp add: g'_def j algebra_simps inner_Basis z dist_norm
intro!: less_imp_le B z_mem norm_z norm_z')
using closed_segment_commute ‹⋀j. j < DIM('a) ⟹ E ! j ∈ Basis› csc_subset j apply blast
done
from vector_differentiable_bound_linearization[OF g' order_refl cont_bound ends_in_segment(1)]
have n: "norm (g j (x' ∙ E ! j) - g j (x ∙ E ! j) - (x' ∙ E ! j - x ∙ E ! j) *⇩R g' j (x ∙ E ! j)) ≤ norm (x' ∙ E ! j - x ∙ E ! j) * B"
.
have "z (Suc j) = z j + (x' ∙ E ! j - x ∙ E ! j) *⇩R E ! j"
by (auto simp: z_def h_def algebra_simps)
then have "f (x + z (Suc j)) = f (x + z j + (x' ∙ E ! j - x ∙ E ! j) *⇩R E ! j) "
with n have "norm (f (x + z (Suc j)) - f (x + z j) - (x' ∙ E ! j - x ∙ E ! j) *⇩R f' (E ! j) (x + z j)) ≤ ¦x' ∙ E ! j - x ∙ E ! j¦ * B"
} note B_le = this
have B': "norm (f' (E ! j) (x + z j) - f' (E ! j) x) ≤ B" if "j < DIM('a)" for j
using that assms(3)
by (auto simp add: algebra_simps inner_Basis z dist_norm ‹0 < d›
intro!: less_imp_le B z_mem norm_z)
have "(∑j≤DIM('a) - 1. f (x + z j) - f (x + z (Suc j))) = f (x + z 0) - f (x + z (Suc (DIM('a) - 1)))"
by (rule sum_telescope)
moreover have "z DIM('a) = h"
using index
by (auto simp: z_def h_def algebra_simps inner_sum_left inner_Basis if_distrib
nth_eq_iff_index
sum.delta
intro!: euclidean_eqI[where 'a='a]
cong: if_cong)
moreover have "z 0 = 0"
by (auto simp: z_def)
moreover have "{..DIM('a) - 1} = {..<DIM('a)}"
using le_imp_less_Suc by fastforce
ultimately have "f x - f (x + h) = (∑j<DIM('a). f (x + z j) - f (x + z (Suc j)))"
by (auto simp: )
then have "norm (f (x + h) - f x - (∑j∈Basis. ((x' - x) ∙ j) *⇩R f' j x)) =
norm(
(∑j<DIM('a). f (x + z (Suc j)) - f (x + z j) - (x' ∙ E ! j - x ∙ E ! j) *⇩R f' (E ! j) (x + z j)) +
(∑j<DIM('a). (x' ∙ E ! j - x ∙ E ! j) *⇩R (f' (E ! j) (x + z j) - f' (E ! j) x)))"
(is "_ = norm (sum ?a ?E + sum ?b ?E)")
by (intro arg_cong[where f=norm]) (simp add: sum_negf sum_subtractf sum.distrib algebra_simps sum_Basis_E)
also have "… ≤ norm (sum ?a ?E) + norm (sum ?b ?E)" by (norm)
also have "norm (sum ?a ?E) ≤ sum (λx. norm (?a x)) ?E"
by (rule norm_sum)
also have "… ≤ sum (λj. norm ¦x' ∙ E ! j - x ∙ E ! j¦ * B) ?E"
by (auto intro!: sum_mono B_le)
also have "… ≤ sum (λj. norm (x' - x) * B) ?E"
apply (rule sum_mono)
apply (auto intro!: mult_right_mono ‹0 ≤ B›)
by (metis (full_types) ‹⋀j. j < DIM('a) ⟹ E ! j ∈ Basis› inner_diff_left norm_bound_Basis_le order_refl)
also have "… = norm (x' - x) * DIM('a) * B"
by simp
also have "norm (sum ?b ?E) ≤ sum (λx. norm (?b x)) ?E"
by (rule norm_sum)
also have "… ≤ sum (λj. norm (x' - x) * B) ?E"
apply (intro sum_mono)
apply (auto intro!: mult_mono B')
apply (metis (full_types) ‹⋀j. j < DIM('a) ⟹ E ! j ∈ Basis› inner_diff_left norm_bound_Basis_le order_refl)
done
also have "… = norm (x' - x) * DIM('a) * B"
by simp
finally have "norm (f (x + h) - f x - (∑j∈Basis. ((x' - x) ∙ j) *⇩R f' j x)) ≤
norm (x' - x) * real DIM('a) * B + norm (x' - x) * real DIM('a) * B"
by arith
also have "… /⇩R norm (x' - x) ≤ norm (2 * DIM('a) * B)"
using ‹B ≥ 0›
also have "… < e" using B_thms by simp
finally show ?case by (auto simp: divide_simps abs_mult h_def)
qed
qed
qed

lemma
frechet_derivative_equals_partial_derivative:
fixes f::"'a::euclidean_space ⇒ 'a"
assumes Df: "⋀x. (f has_derivative Df x) (at x)"
assumes f': "((λp. f (x + (p - x ∙ i) *⇩R i) ∙ b) has_real_derivative f' x i b) (at (x ∙ i))"
shows "Df x i ∙ b = f' x i b"
proof -
define Dfb where "Dfb x = Blinfun (Df x)" for x
have Dfb_apply: "blinfun_apply (Dfb x) = Df x" for x
unfolding Dfb_def
apply (rule bounded_linear_Blinfun_apply)
apply (rule has_derivative_bounded_linear)
apply (rule assms)
done
have "Dfb x = blinfun_of_matrix (λi b. Dfb x b ∙ i)" for x
using blinfun_of_matrix_works[of "Dfb x"] by auto
have Dfb: "⋀x. (f has_derivative Dfb x) (at x)"
by (auto simp: Dfb_apply Df)
note [derivative_intros] = diff_chain_at[OF _ Dfb, unfolded o_def]
have "((λp. f (x + (p - x ∙ i) *⇩R i) ∙ b) has_real_derivative Dfb x i ∙ b) (at (x ∙ i))"
by (auto intro!: derivative_eq_intros ext simp: has_field_derivative_def blinfun.bilinear_simps)
from DERIV_unique[OF f' this]
show ?thesis by (simp add: Dfb_apply)
qed

subsection ‹Integration›

lemmas content_real[simp]
lemmas integrable_continuous[intro, simp]
and integrable_continuous_real[intro, simp]

lemma integral_eucl_le:
fixes f g::"'a::euclidean_space ⇒ 'b::ordered_euclidean_space"
assumes "f integrable_on s"
and "g integrable_on s"
and "⋀x. x ∈ s ⟹ f x ≤ g x"
shows "integral s f ≤ integral s g"
using assms
by (auto intro!: integral_component_le simp: eucl_le[where 'a='b])

lemma
integral_ivl_bound:
fixes l u::"'a::ordered_euclidean_space"
assumes "⋀x h'. h' ∈ {t0 .. h} ⟹ x ∈ {t0 .. h} ⟹ (h' - t0) *⇩R f x ∈ {l .. u}"
assumes "t0 ≤ h"
assumes f_int: "f integrable_on {t0 .. h}"
shows "integral {t0 .. h} f ∈ {l .. u}"
proof -
from assms(1)[of t0 t0] assms(2) have "0 ∈ {l .. u}" by auto
have "integral {t0 .. h} f = integral {t0 .. h} (λt. if t ∈ {t0, h} then 0 else f t)"
by (rule integral_spike[where S="{t0, h}"]) auto
also
{
fix x
assume 1: "x ∈ {t0 <..< h}"
with assms have "(h - t0) *⇩R f x ∈ {l .. u}" by auto
then have "(if x ∈ {t0, h} then 0 else f x) ∈ {l /⇩R (h - t0) .. u /⇩R (h - t0)}"
using ‹x ∈ _›
by (auto simp: inverse_eq_divide
simp: eucl_le[where 'a='a] field_simps algebra_simps)
}
then have "… ∈ {integral {t0..h} (λ_. l /⇩R (h - t0)) .. integral {t0..h} (λ_. u /⇩R (h - t0))}"
unfolding atLeastAtMost_iff
apply (safe intro!: integral_eucl_le)
using ‹0 ∈ {l .. u}›
apply (auto intro!: assms
intro: integrable_continuous_real  integrable_spike[where S="{t0, h}", OF f_int]
simp: eucl_le[where 'a='a] divide_simps
split: if_split_asm)
done
also have "… ⊆ {l .. u}"
using assms ‹0 ∈ {l .. u}›
by (auto simp: inverse_eq_divide)
finally show ?thesis .
qed

lemma
fixes l u::"'a::ordered_euclidean_space"
assumes "⋀x h'. h' ∈ {t0 .. h} ⟹ x ∈ {t0 .. h} ⟹ (h' - t0) *⇩R f x ∈ {l - x0 .. u - x0}"
assumes "t0 ≤ h"
assumes f_int: "f integrable_on {t0 .. h}"
shows "x0 + integral {t0 .. h} f ∈ {l .. u}"
using integral_ivl_bound[OF assms]
by (auto simp: algebra_simps)

subsection ‹conditionally complete lattice›

subsection ‹Lists›

lemma
Ball_set_Cons[simp]: "(∀a∈set_Cons x y. P a) ⟷ (∀a∈x. ∀b∈y. P (a#b))"
by (auto simp: set_Cons_def)

lemma set_cons_eq_empty[iff]: "set_Cons a b = {} ⟷ a = {} ∨ b = {}"
by (auto simp: set_Cons_def)

lemma listset_eq_empty_iff[iff]: "listset XS = {} ⟷ {} ∈ set XS"
by (induction XS) auto

lemma sing_in_sings[simp]: "[x] ∈ (λx. [x])  xd ⟷ x ∈ xd"
by auto

lemma those_eq_None_set_iff: "those xs = None ⟷ None ∈ set xs"
by (induction xs) (auto split: option.split)

lemma those_eq_Some_lengthD: "those xs = Some ys ⟹ length xs = length ys"
by (induction xs arbitrary: ys) (auto split: option.splits)

lemma those_eq_Some_map_Some_iff: "those xs = Some ys ⟷ (xs = map Some ys)" (is "?l ⟷ ?r")
proof safe
assume ?l
then have "length xs = length ys"
by (rule those_eq_Some_lengthD)
then show ?r using ‹?l›
by (induction xs ys rule: list_induct2) (auto split: option.splits)
next
assume ?r
then have "length xs = length ys"
by simp
then show "those (map Some ys) = Some ys" using ‹?r›
by (induction xs ys rule: list_induct2) (auto split: option.splits)
qed

subsection ‹Set(sum)›

subsection ‹Max›

subsection ‹Uniform Limit›

subsection ‹Bounded Linear Functions›

lift_definition comp3::― ‹TODO: name?›
"('c::real_normed_vector ⇒⇩L 'd::real_normed_vector) ⇒ ('b::real_normed_vector ⇒⇩L 'c) ⇒⇩L 'b ⇒⇩L 'd" is
"λ(cd::('c ⇒⇩L 'd)) (bc::'b ⇒⇩L 'c). (cd o⇩L bc)"
by (rule bounded_bilinear.bounded_linear_right[OF bounded_bilinear_blinfun_compose])

lemma blinfun_apply_comp3[simp]: "blinfun_apply (comp3 a) b = (a o⇩L b)"

lemma bounded_linear_comp3[bounded_linear]: "bounded_linear comp3"
by transfer (rule bounded_bilinear_blinfun_compose)

lift_definition comp12::― ‹TODO: name?›
"('a::real_normed_vector ⇒⇩L 'c::real_normed_vector) ⇒ ('b::real_normed_vector ⇒⇩L 'c) ⇒ ('a × 'b) ⇒⇩L 'c"
is "λf g (a, b). f a + g b"
by (auto intro!: bounded_linear_intros
intro: bounded_linear_compose
simp: split_beta')

lemma blinfun_apply_comp12[simp]: "blinfun_apply (comp12 f g) b = f (fst b) + g (snd b)"

subsection ‹Order Transitivity Attributes›

attribute_setup le = ‹Scan.succeed (Thm.rule_attribute [] (fn context => fn thm => thm RS @{thm order_trans}))›
"transitive version of inequality (useful for intro)"
attribute_setup ge = ‹Scan.succeed (Thm.rule_attribute [] (fn context => fn thm => thm RS @{thm order_trans[rotated]}))›
"transitive version of inequality (useful for intro)"

subsection ‹point reflection›

definition preflect::"'a::real_vector ⇒ 'a ⇒ 'a" where "preflect ≡ λt0 t. 2 *⇩R t0 - t"

lemma preflect_preflect[simp]: "preflect t0 (preflect t0 t) = t"

lemma preflect_preflect_image[simp]: "preflect t0  preflect t0  S = S"

lemma is_interval_preflect[simp]: "is_interval (preflect t0  S) ⟷ is_interval S"
by (auto simp: preflect_def[abs_def])

lemma iv_in_preflect_image[intro, simp]: "t0 ∈ T ⟹ t0 ∈ preflect t0  T"
by (auto intro!: image_eqI simp: preflect_def algebra_simps scaleR_2)

lemma preflect_tendsto[tendsto_intros]:
fixes l::"'a::real_normed_vector"
shows "(g ⤏ l) F ⟹ (h ⤏ m) F ⟹ ((λx. preflect (g x) (h x)) ⤏ preflect l m) F"
by (auto intro!: tendsto_eq_intros simp: preflect_def)

lemma continuous_preflect[continuous_intros]:
fixes a::"'a::real_normed_vector"
shows "continuous (at a within A) (preflect t0)"
by (auto simp: continuous_within intro!: tendsto_intros)

lemma
fixes t0::"'a::ordered_real_vector"
shows preflect_le[simp]: "t0 ≤ preflect t0 b ⟷ b ≤ t0"
and le_preflect[simp]: "preflect t0 b ≤ t0 ⟷ t0 ≤ b"
and antimono_preflect: "antimono (preflect t0)"
and preflect_le_preflect[simp]: "preflect t0 a ≤ preflect t0 b ⟷ b ≤ a"
and preflect_eq_cancel[simp]: "preflect t0 a = preflect t0 b ⟷ a = b"
by (auto intro!: antimonoI simp: preflect_def scaleR_2)

lemma preflect_eq_point_iff[simp]: "t0 = preflect t0 s ⟷ t0 = s" "preflect t0 s = t0 ⟷ t0 = s"
by (auto simp: preflect_def algebra_simps scaleR_2)

lemma preflect_minus_self[simp]: "preflect t0 s - t0 = t0 - s"

end


# Theory MVT_Ex

theory MVT_Ex
imports
"HOL-Analysis.Analysis"
"HOL-Decision_Procs.Approximation"
"../ODE_Auxiliarities"
begin

subsection ‹(Counter)Example of Mean Value Theorem in Euclidean Space \label{sec:countermvt}›

text ‹There is no exact analogon of the mean value theorem in the multivariate case!›

lemma MVT_wrong: assumes
"⋀J a u (f::real*real⇒real*real).
(⋀x. FDERIV f x :> J x) ⟹
(∃t∈{0<..<1}. f (a + u) - f a = J (a + t *⇩R u) u)"
shows "False"
proof -
have "⋀t::real*real. FDERIV (λt. (cos (fst t), sin (fst t))) t :> (λh. (- ((fst h) * sin (fst t)), (fst h) * cos (fst t)))"
by (auto intro!: derivative_eq_intros)
from assms[OF this, of "(pi, pi)" "(pi, pi)"] obtain t::real where t: "0 < t" "t < 1" and
"pi * sin (t * pi) = 2" "cos (t * pi) = 0"
by auto
then obtain n where tpi: "t * pi = real_of_int n * (pi / 2)" and "odd n"
by (auto simp: cos_zero_iff_int)
then have teq: "t = real_of_int n / 2" by auto
then have "n = 1" using t ‹odd n› by arith
then have "t = 1/2" using teq by simp
have "sin (t * pi) = 1"
by (simp add: ‹t = 1/2› sin_eq_1)
with ‹pi * sin (t * pi) = 2›
have "pi = 2" by simp
moreover have "pi > 2" using pi_approx by simp
ultimately show False by simp
qed

lemma MVT_corrected:
fixes f::"'a::ordered_euclidean_space⇒'b::euclidean_space"
assumes fderiv: "⋀x. x ∈ D ⟹ (f has_derivative J x) (at x within D)"
assumes line_in: "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ a + x *⇩R u ∈ D"
shows "(∃t∈Basis→{0<..<1}. (f (a + u) - f a) = (∑i∈Basis. (J (a + t i *⇩R u) u ∙ i) *⇩R i))"
proof -
{
fix i::'b
assume "i ∈ Basis"
have subset: "((λx. a + x *⇩R u)  {0..1}) ⊆ D"
using line_in by force
have "⋀x. ⟦0 ≤ x; x ≤ 1⟧ ⟹ ((λb. f (a + b *⇩R u) ∙ i) has_derivative (λb. b *⇩R J (a + x *⇩R u) u ∙ i)) (at x within {0..1})"
using line_in
by (auto intro!: derivative_eq_intros
has_derivative_subset[OF _ subset]
has_derivative_in_compose[where f="λx. a + x *⇩R u"]
fderiv line_in
with zero_less_one
have "∃x∈{0<..<1}. f (a + 1 *⇩R u) ∙ i - f (a + 0 *⇩R u) ∙ i = (1 - 0) *⇩R J (a + x *⇩R u) u ∙ i"
by (rule mvt_simple)
}
then obtain t where "∀i∈Basis. t i ∈ {0<..<1} ∧ f (a + u) ∙ i - f a ∙ i = J (a + t i *⇩R u) u ∙ i"
by atomize_elim (force intro!: bchoice)
hence "t ∈ Basis → {0<..<1}" "⋀i. i ∈ Basis ⟹ (f (a + u) - f a) ∙ i = J (a + t i *⇩R u) u ∙ i"
by (auto simp: inner_diff_left)
moreover hence "(f (a + u) - f a) = (∑i∈Basis. (J (a + t i *⇩R u) u ∙ i) *⇩R i)"
by (intro euclidean_eqI[where 'a='b]) simp
ultimately show ?thesis by blast
qed

lemma MVT_ivl:
fixes f::"'a::ordered_euclidean_space⇒'b::ordered_euclidean_space"
assumes fderiv: "⋀x. x ∈ D ⟹ (f has_derivative J x) (at x within D)"
assumes J_ivl: "⋀x. x ∈ D ⟹ J x u ∈ {J0 .. J1}"
assumes line_in: "⋀x. x ∈ {0..1} ⟹ a + x *⇩R u ∈ D"
shows "f (a + u) - f a ∈ {J0..J1}"
proof -
from MVT_corrected[OF fderiv line_in] obtain t where
t: "t∈Basis → {0<..<1}" and
mvt: "f (a + u) - f a = (∑i∈Basis. (J (a + t i *⇩R u) u ∙ i) *⇩R i)"
by auto
note mvt
also have "… ∈ {J0 .. J1}"
proof -
have J: "⋀i. i ∈ Basis ⟹ J0 ≤ J (a + t i *⇩R u) u"
"⋀i. i ∈ Basis ⟹ J (a + t i *⇩R u) u ≤ J1"
using J_ivl t line_in by (auto simp: Pi_iff)
show ?thesis
using J
unfolding atLeastAtMost_iff eucl_le[where 'a='b]
by auto
qed
finally show ?thesis .
qed

lemma MVT:
shows
"⋀J J0 J1 a u (f::real*real⇒real*real).
(⋀x. FDERIV f x :> J x) ⟹
(⋀x. J x u ∈ {J0 .. J1}) ⟹
f (a + u) - f a ∈ {J0 .. J1}"
by (rule_tac J = J in MVT_ivl[where D=UNIV]) auto

lemma MVT_ivl':
fixes f::"'a::ordered_euclidean_space⇒'b::ordered_euclidean_space"
assumes fderiv: "(⋀x. x ∈ D ⟹ (f has_derivative J x) (at x within D))"
assumes J_ivl: "⋀x. x ∈ D ⟹ J x (a - b) ∈ {J0..J1}"
assumes line_in: "⋀x. x ∈ {0..1} ⟹ b + x *⇩R (a - b) ∈ D"
shows "f a ∈ {f b + J0..f b + J1}"
proof -
have "f (b + (a - b)) - f b ∈ {J0 .. J1}"
using J_ivl MVT_ivl fderiv line_in by blast
thus ?thesis
by (auto simp: diff_le_eq le_diff_eq ac_simps)
qed

end


# Theory Vector_Derivative_On

theory
Vector_Derivative_On
imports
"HOL-Analysis.Analysis"
begin

subsection ‹Vector derivative on a set›
― ‹TODO: also for the other derivatives?!›
― ‹TODO: move to repository and rewrite assumptions of common lemmas?›

definition
has_vderiv_on :: "(real ⇒ 'a::real_normed_vector) ⇒ (real ⇒ 'a) ⇒ real set ⇒ bool"
(infix "(has'_vderiv'_on)" 50)
where
"(f has_vderiv_on f') S ⟷ (∀x ∈ S. (f has_vector_derivative f' x) (at x within S))"

lemma has_vderiv_on_empty[intro, simp]: "(f has_vderiv_on f') {}"
by (auto simp: has_vderiv_on_def)

lemma has_vderiv_on_subset:
assumes "(f has_vderiv_on f') S"
assumes "T ⊆ S"
shows "(f has_vderiv_on f') T"
by (meson assms(1) assms(2) contra_subsetD has_vderiv_on_def has_vector_derivative_within_subset)

lemma has_vderiv_on_compose:
assumes "(f has_vderiv_on f') (g  T)"
assumes "(g has_vderiv_on g') T"
shows "(f o g has_vderiv_on (λx. g' x *⇩R f' (g x))) T"
using assms
unfolding has_vderiv_on_def
by (auto intro!: vector_diff_chain_within)

lemma has_vderiv_on_open:
assumes "open T"
shows "(f has_vderiv_on f') T ⟷ (∀t ∈ T. (f has_vector_derivative f' t) (at t))"
by (auto simp: has_vderiv_on_def at_within_open[OF _ ‹open T›])

lemma has_vderiv_on_eq_rhs:― ‹TODO: integrate intro ‹derivative_eq_intros››
"(f has_vderiv_on g') T ⟹ (⋀x. x ∈ T ⟹ g' x = f' x) ⟹ (f has_vderiv_on f') T"
by (auto simp: has_vderiv_on_def)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
shows has_vderiv_on_id: "((λx. x) has_vderiv_on (λx. 1)) T"
and has_vderiv_on_const: "((λx. c) has_vderiv_on (λx. 0)) T"
by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
fixes f::"real ⇒ 'a::real_normed_vector"
assumes "(f has_vderiv_on f') T"
shows has_vderiv_on_uminus: "((λx. - f x) has_vderiv_on (λx. - f' x)) T"
using assms
by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
fixes f g::"real ⇒ 'a::real_normed_vector"
assumes "(f has_vderiv_on f') T"
assumes "(g has_vderiv_on g') T"
shows has_vderiv_on_add: "((λx. f x + g x) has_vderiv_on (λx. f' x + g' x)) T"
and has_vderiv_on_diff: "((λx. f x - g x) has_vderiv_on (λx. f' x - g' x)) T"
using assms
by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
fixes f::"real ⇒ real" and g::"real ⇒ 'a::real_normed_vector"
assumes "(f has_vderiv_on f') T"
assumes "(g has_vderiv_on g') T"
shows has_vderiv_on_scaleR: "((λx. f x *⇩R g x) has_vderiv_on (λx. f x *⇩R g' x + f' x *⇩R g x)) T"
using assms
by (auto simp: has_vderiv_on_def has_field_derivative_iff_has_vector_derivative
intro!: derivative_eq_intros)

lemma [THEN has_vderiv_on_eq_rhs, derivative_intros]:
fixes f g::"real ⇒ 'a::real_normed_algebra"
assumes "(f has_vderiv_on f') T"
assumes "(g has_vderiv_on g') T"
shows has_vderiv_on_mult: "((λx. f x * g x) has_vderiv_on (λx. f x * g' x + f' x * g x)) T"
using assms
by (auto simp: has_vderiv_on_def intro!: derivative_eq_intros)

lemma has_vderiv_on_ln[THEN has_vderiv_on_eq_rhs, derivative_intros]:
fixes g::"real ⇒ real"
assumes "⋀x. x ∈ s ⟹ 0 < g x"
assumes "(g has_vderiv_on g') s"
shows "((λx. ln (g x)) has_vderiv_on (λx. g' x / g x)) s"
using assms
unfolding has_vderiv_on_def
by (auto simp: has_vderiv_on_def has_field_derivative_iff_has_vector_derivative[symmetric]
intro!: derivative_eq_intros)

lemma fundamental_theorem_of_calculus':
fixes f :: "real ⇒ 'a::banach"
shows "a ≤ b ⟹ (f has_vderiv_on f') {a .. b} ⟹ (f' has_integral (f b - f a)) {a .. b}"
by (auto intro!: fundamental_theorem_of_calculus simp: has_vderiv_on_def)

lemma has_vderiv_on_If:
assumes "U = S ∪ T"
assumes "(f has_vderiv_on f') (S ∪ (closure T ∩ closure S))"
assumes "(g has_vderiv_on g') (T ∪ (closure T ∩ closure S))"
assumes "⋀x. x ∈ closure T ⟹ x ∈ closure S ⟹ f x = g x"
assumes "⋀x. x ∈ closure T ⟹ x ∈ closure S ⟹ f' x = g' x"
shows "((λt. if t ∈ S then f t else g t) has_vderiv_on (λt. if t ∈ S then f' t else g' t)) U"
using assms
by (auto simp: has_vderiv_on_def ac_simps
intro!: has_vector_derivative_If_within_closures
split del: if_split)

lemma mvt_very_simple_closed_segmentE:
fixes f::"real⇒real"
assumes "(f has_vderiv_on f') (closed_segment a b)"
obtains y where "y ∈ closed_segment a b"  "f b - f a = (b - a) * f' y"
proof cases
assume "a ≤ b"
with mvt_very_simple[of a b f "λx i. i *⇩R f' x"] assms
obtain y where "y ∈ closed_segment a b"  "f b - f a = (b - a) * f' y"
by (auto simp: has_vector_derivative_def closed_segment_eq_real_ivl has_vderiv_on_def)
thus ?thesis ..
next
assume "¬ a ≤ b"
with mvt_very_simple[of b a f "λx i. i *⇩R f' x"] assms
obtain y where "y ∈ closed_segment a b"  "f b - f a = (b - a) * f' y"
by (force simp: has_vector_derivative_def has_vderiv_on_def closed_segment_eq_real_ivl algebra_simps)
thus ?thesis ..
qed

lemma mvt_simple_closed_segmentE:
fixes f::"real⇒real"
assumes "(f has_vderiv_on f') (closed_segment a b)"
assumes "a ≠ b"
obtains y where "y ∈ open_segment a b"  "f b - f a = (b - a) * f' y"
proof cases
assume "a ≤ b"
with assms have "a < b" by simp
with mvt_simple[of a b f "λx i. i *⇩R f' x"] assms
obtain y where "y ∈ open_segment a b"  "f b - f a = (b - a) * f' y"
by (auto simp: has_vector_derivative_def closed_segment_eq_real_ivl has_vderiv_on_def
open_segment_eq_real_ivl)
thus ?thesis ..
next
assume "¬ a ≤ b"
then have "b < a" by simp
with mvt_simple[of b a f "λx i. i *⇩R f' x"] assms
obtain y where "y ∈ open_segment a b"  "f b - f a = (b - a) * f' y"
by (force simp: has_vector_derivative_def has_vderiv_on_def closed_segment_eq_real_ivl algebra_simps
open_segment_eq_real_ivl)
thus ?thesis ..
qed

lemma differentiable_bound_general_open_segment:
fixes a :: "real"
and b :: "real"
and f :: "real ⇒ 'a::real_normed_vector"
and f' :: "real ⇒ 'a"
assumes "continuous_on (closed_segment a b) f"
assumes "continuous_on (closed_segment a b) g"
and "(f has_vderiv_on f') (open_segment a b)"
and "(g has_vderiv_on g') (open_segment a b)"
and "⋀x. x ∈ open_segment a b ⟹ norm (f' x) ≤ g' x"
shows "norm (f b - f a) ≤ abs (g b - g a)"
proof -
{
assume "a = b"
hence ?thesis by simp
} moreover {
assume "a < b"
with assms
have "continuous_on {a .. b} f"
and "continuous_on {a .. b} g"
and "⋀x. x∈{a<..<b} ⟹ (f has_vector_derivative f' x) (at x)"
and "⋀x. x∈{a<..<b} ⟹ (g has_vector_derivative g' x) (at x)"
and "⋀x. x∈{a<..<b} ⟹ norm (f' x) ≤ g' x"
by (auto simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl has_vderiv_on_def
at_within_open[where S="{a<..<b}"])
from differentiable_bound_general[OF ‹a < b› this]
have ?thesis by auto
} moreover {
assume "b < a"
with assms
have "continuous_on {b .. a} f"
and "continuous_on {b .. a} g"
and "⋀x. x∈{b<..<a} ⟹ (f has_vector_derivative f' x) (at x)"
and "⋀x. x∈{b<..<a} ⟹ (g has_vector_derivative g' x) (at x)"
and "⋀x. x∈{b<..<a} ⟹ norm (f' x) ≤ g' x"
by (auto simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl has_vderiv_on_def
at_within_open[where S="{b<..<a}"])
from differentiable_bound_general[OF ‹b < a› this]
have "norm (f a - f b) ≤ g a - g b" by simp
also have "… ≤ abs (g b - g a)" by simp
finally have ?thesis by (simp add: norm_minus_commute)
} ultimately show ?thesis by arith
qed

lemma has_vderiv_on_union:
assumes "(f has_vderiv_on g) (s ∪ closure s ∩ closure t)"
assumes "(f has_vderiv_on g) (t ∪ closure s ∩ closure t)"
shows "(f has_vderiv_on g) (s ∪ t)"
unfolding has_vderiv_on_def
proof
fix x assume "x ∈ s ∪ t"
with has_vector_derivative_If_within_closures[of x s t "s ∪ t" f g f g] assms
show "(f has_vector_derivative g x) (at x within s ∪ t)"
by (auto simp: has_vderiv_on_def)
qed

lemma has_vderiv_on_union_closed:
assumes "(f has_vderiv_on g) s"
assumes "(f has_vderiv_on g) t"
assumes "closed s" "closed t"
shows "(f has_vderiv_on g) (s ∪ t)"
using has_vderiv_on_If[OF refl, of f g s t f g] assms
by (auto simp: has_vderiv_on_subset)

lemma vderiv_on_continuous_on: "(f has_vderiv_on f') S ⟹ continuous_on S f"
by (auto intro!: continuous_on_vector_derivative simp: has_vderiv_on_def)

lemma has_vderiv_on_cong[cong]:
assumes "⋀x. x ∈ S ⟹ f x = g x"
assumes "⋀x. x ∈ S ⟹ f' x = g' x"
assumes "S = T"
shows "(f has_vderiv_on f') S = (g has_vderiv_on g') T"
using assms
by (metis has_vector_derivative_transform has_vderiv_on_def)

lemma has_vderiv_eq:
assumes "(f has_vderiv_on f') S"
assumes "⋀x. x ∈ S ⟹ f x = g x"
assumes "⋀x. x ∈ S ⟹ f' x = g' x"
assumes "S = T"
shows "(g has_vderiv_on g') T"
using assms by simp

lemma has_vderiv_on_compose':
assumes "(f has_vderiv_on f') (g  T)"
assumes "(g has_vderiv_on g') T"
shows "((λx. f (g x)) has_vderiv_on (λx. g' x *⇩R f' (g x))) T"
using has_vderiv_on_compose[OF assms]
by simp

lemma has_vderiv_on_compose2:
assumes "(f has_vderiv_on f') S"
assumes "(g has_vderiv_on g') T"
assumes "⋀t. t ∈ T ⟹ g t ∈ S"
shows "((λx. f (g x)) has_vderiv_on (λx. g' x *⇩R f' (g x))) T"
using has_vderiv_on_compose[OF has_vderiv_on_subset[OF assms(1)] assms(2)] assms(3)
by force

lemma has_vderiv_on_singleton: "(y has_vderiv_on y') {t0}"
by (auto simp: has_vderiv_on_def has_vector_derivative_def has_derivative_within_singleton_iff
bounded_linear_scaleR_left)

lemma
has_vderiv_on_zero_constant:
assumes "convex s"
assumes "(f has_vderiv_on (λh. 0)) s"
obtains c where "⋀x. x ∈ s ⟹ f x = c"
using has_vector_derivative_zero_constant[of s f] assms
by (auto simp: has_vderiv_on_def)

lemma bounded_vderiv_on_imp_lipschitz:
assumes "(f has_vderiv_on f') X"
assumes convex: "convex X"
assumes "⋀x. x ∈ X ⟹ norm (f' x) ≤ C" "0 ≤ C"
shows "C-lipschitz_on X f"
using assms
by (auto simp: has_vderiv_on_def has_vector_derivative_def onorm_scaleR_left onorm_id
intro!: bounded_derivative_imp_lipschitz[where f' = "λx d. d *⇩R f' x"])

end


# Theory Interval_Integral_HK

theory Interval_Integral_HK
imports Vector_Derivative_On
begin

subsection ‹interval integral›
― ‹TODO: move to repo ?!›
― ‹TODO: replace with Bochner Integral?!
But FTC for Bochner requires continuity and euclidean space!›

definition has_ivl_integral ::
"(real ⇒ 'b::real_normed_vector) ⇒ 'b ⇒ real ⇒ real ⇒ bool"― ‹TODO: generalize?›
(infixr "has'_ivl'_integral" 46)
where "(f has_ivl_integral y) a b ⟷ (if a ≤ b then (f has_integral y) {a .. b} else (f has_integral - y) {b .. a})"

definition ivl_integral::"real ⇒ real ⇒ (real ⇒ 'a) ⇒ 'a::real_normed_vector"
where "ivl_integral a b f = integral {a .. b} f - integral {b .. a} f"

lemma integral_emptyI[simp]:
fixes a b::real
shows  "a ≥ b ⟹ integral {a..b} f = 0" "a > b ⟹ integral {a..b} f = 0"
by (cases "a = b") auto

lemma ivl_integral_unique: "(f has_ivl_integral y) a b ⟹ ivl_integral a b f = y"
using integral_unique[of f y "{a .. b}"] integral_unique[of f "- y" "{b .. a}"]
unfolding ivl_integral_def has_ivl_integral_def
by (auto split: if_split_asm)

lemma fundamental_theorem_of_calculus_ivl_integral:
fixes f :: "real ⇒ 'a::banach"
shows "(f has_vderiv_on f') (closed_segment a b) ⟹ (f' has_ivl_integral f b - f a) a b"
by (auto simp: has_ivl_integral_def closed_segment_eq_real_ivl intro!: fundamental_theorem_of_calculus')

lemma
fixes f :: "real ⇒ 'a::banach"
assumes "f integrable_on (closed_segment a b)"
shows indefinite_ivl_integral_continuous:
"continuous_on (closed_segment a b) (λx. ivl_integral a x f)"
"continuous_on (closed_segment b a) (λx. ivl_integral a x f)"
using assms
by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm
intro!: indefinite_integral_continuous_1 indefinite_integral_continuous_1'
continuous_intros intro: continuous_on_eq)

lemma
fixes f :: "real ⇒ 'a::banach"
assumes "f integrable_on (closed_segment a b)"
assumes "c ∈ closed_segment a b"
shows indefinite_ivl_integral_continuous_subset:
"continuous_on (closed_segment a b) (λx. ivl_integral c x f)"
proof -
from assms have "f integrable_on (closed_segment c a)" "f integrable_on (closed_segment c b)"
by (auto simp: closed_segment_eq_real_ivl integrable_on_subinterval
integrable_on_insert_iff split: if_splits)
then have "continuous_on (closed_segment a c ∪ closed_segment c b) (λx. ivl_integral c x f)"
by (auto intro!: indefinite_ivl_integral_continuous continuous_on_closed_Un)
also have "closed_segment a c ∪ closed_segment c b = closed_segment a b"
using assms by (auto simp: closed_segment_eq_real_ivl)
finally show ?thesis .
qed

lemma real_Icc_closed_segment: fixes a b::real shows "a ≤ b ⟹ {a .. b} = closed_segment a b"
by (auto simp: closed_segment_eq_real_ivl)

lemma ivl_integral_zero[simp]: "ivl_integral a a f = 0"
by (auto simp: ivl_integral_def)

lemma ivl_integral_cong:
assumes "⋀x. x ∈ closed_segment a b ⟹ g x = f x"
assumes "a = c" "b = d"
shows "ivl_integral a b f = ivl_integral c d g"
using assms integral_spike[of "{}" "closed_segment a b" f g]
by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)

lemma ivl_integral_diff:
"f integrable_on (closed_segment s t) ⟹ g integrable_on (closed_segment s t) ⟹
ivl_integral s t (λx. f x - g x) = ivl_integral s t f - ivl_integral s t g"
using Henstock_Kurzweil_Integration.integral_diff[of f "closed_segment s t" g]
by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)

lemma ivl_integral_norm_bound_ivl_integral:
fixes f :: "real ⇒ 'a::banach"
assumes "f integrable_on (closed_segment a b)"
and "g integrable_on (closed_segment a b)"
and "⋀x. x ∈ closed_segment a b ⟹ norm (f x) ≤ g x"
shows "norm (ivl_integral a b f) ≤ abs (ivl_integral a b g)"
using integral_norm_bound_integral[OF assms]
by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)

lemma ivl_integral_norm_bound_integral:
fixes f :: "real ⇒ 'a::banach"
assumes "f integrable_on (closed_segment a b)"
and "g integrable_on (closed_segment a b)"
and "⋀x. x ∈ closed_segment a b ⟹ norm (f x) ≤ g x"
shows "norm (ivl_integral a b f) ≤ integral (closed_segment a b) g"
using integral_norm_bound_integral[OF assms]
by (auto simp: ivl_integral_def closed_segment_eq_real_ivl split: if_split_asm)

lemma norm_ivl_integral_le:
fixes f :: "real ⇒ real"
assumes "f integrable_on (closed_segment a b)"
and "g integrable_on (closed_segment a b)"
and "⋀x. x ∈ closed_segment a b ⟹ f x ≤ g x"
and "⋀x. x ∈ closed_segment a b ⟹ 0 ≤ f x"
shows "abs (ivl_integral a b f) ≤ abs (ivl_integral a b g)"
proof (cases "a = b")
case True then show ?thesis
by simp
next
case False
have "0 ≤ integral {a..b} f" "0 ≤ integral {b..a} f"
by (metis le_cases Henstock_Kurzweil_Integration.integral_nonneg assms(1) assms(4) closed_segment_eq_real_ivl integral_emptyI(1))+
then show ?thesis
using integral_le[OF assms(1-3)]
unfolding ivl_integral_def closed_segment_eq_real_ivl
by (simp split: if_split_asm)
qed

lemma ivl_integral_const [simp]:
shows "ivl_integral a b (λx. c) = (b - a) *⇩R c"
by (auto simp: ivl_integral_def algebra_simps)

lemma ivl_integral_has_vector_derivative:
fixes f :: "real ⇒ 'a::banach"
assumes "continuous_on (closed_segment a b) f"
and "x ∈ closed_segment a b"
shows "((λu. ivl_integral a u f) has_vector_derivative f x) (at x within closed_segment a b)"
proof -
have "((λx. integral {x..a} f) has_vector_derivative 0) (at x within {a..b})" if "a ≤ x" "x ≤ b"
by (rule has_vector_derivative_transform) (auto simp: that)
moreover
have "((λx. integral {a..x} f) has_vector_derivative 0) (at x within {b..a})" if "b ≤ x" "x ≤ a"
by (rule has_vector_derivative_transform) (auto simp: that)
ultimately
show ?thesis
using assms
by (auto simp: ivl_integral_def closed_segment_eq_real_ivl
intro!: derivative_eq_intros
integral_has_vector_derivative[of a b f] integral_has_vector_derivative[of b a "-f"]
integral_has_vector_derivative'[of b a f])
qed

lemma ivl_integral_has_vderiv_on:
fixes f :: "real ⇒ 'a::banach"
assumes "continuous_on (closed_segment a b) f"
shows "((λu. ivl_integral a u f) has_vderiv_on f) (closed_segment a b)"
using ivl_integral_has_vector_derivative[OF assms]
by (auto simp: has_vderiv_on_def)

lemma ivl_integral_has_vderiv_on_subset_segment:
fixes f :: "real ⇒ 'a::banach"
assumes "continuous_on (closed_segment a b) f"
and "c ∈ closed_segment a b"
shows "((λu. ivl_integral c u f) has_vderiv_on f) (closed_segment a b)"
proof -
have "(closed_segment c a) ⊆ (closed_segment a b)" "(closed_segment c b) ⊆ (closed_segment a b)"
using assms by (auto simp: closed_segment_eq_real_ivl split: if_splits)
then have "((λu. ivl_integral c u f) has_vderiv_on f) ((closed_segment c a) ∪ (closed_segment c b))"
by (auto intro!: has_vderiv_on_union_closed ivl_integral_has_vderiv_on assms
intro: continuous_on_subset)
also have "(closed_segment c a) ∪ (closed_segment c b) = (closed_segment a b)"
using assms by (auto simp: closed_segment_eq_real_ivl split: if_splits)
finally show ?thesis .
qed

lemma ivl_integral_has_vector_derivative_subset:
fixes f :: "real ⇒ 'a::banach"
assumes "continuous_on (closed_segment a b) f"
and "x ∈ closed_segment a b"
and "c ∈ closed_segment a b"
shows "((λu. ivl_integral c u f) has_vector_derivative f x) (at x within closed_segment a b)"
using ivl_integral_has_vderiv_on_subset_segment[OF assms(1)] assms(2-)
by (auto simp: has_vderiv_on_def)

lemma
compact_interval_eq_Inf_Sup:
fixes A::"real set"
assumes "is_interval A" "compact A" "A ≠ {}"
shows "A = {Inf A .. Sup A}"
apply (auto simp: closed_segment_eq_real_ivl
intro!: cInf_lower cSup_upper bounded_imp_bdd_below bounded_imp_bdd_above
compact_imp_bounded assms)
by (metis assms(1) assms(2) assms(3) cInf_eq_minimum cSup_eq_maximum compact_attains_inf
compact_attains_sup mem_is_interval_1_I)

lemma ivl_integral_has_vderiv_on_compact_interval:
fixes f :: "real ⇒ 'a::banach"
assumes "continuous_on A f"
and "c ∈ A" "is_interval A" "compact A"
shows "((λu. ivl_integral c u f) has_vderiv_on f) A"
proof -
have "A = {Inf A .. Sup A}"
by (rule compact_interval_eq_Inf_Sup) (use assms in auto)
also have "… = closed_segment (Inf A) (Sup A)" using assms
intro!: cInf_le_cSup bounded_imp_bdd_below bounded_imp_bdd_above compact_imp_bounded)
finally have *: "A = closed_segment (Inf A) (Sup A)" .
show ?thesis
apply (subst *)
apply (rule ivl_integral_has_vderiv_on_subset_segment)
unfolding *[symmetric]
by fact+
qed

lemma ivl_integral_has_vector_derivative_compact_interval:
fixes f :: "real ⇒ 'a::banach"
assumes "continuous_on A f"
and "is_interval A" "compact A" "x ∈ A" "c ∈ A"
shows "((λu. ivl_integral c u f) has_vector_derivative f x) (at x within A)"
using ivl_integral_has_vderiv_on_compact_interval[OF assms(1)] assms(2-)
by (auto simp: has_vderiv_on_def)

lemma ivl_integral_combine:
fixes f::"real ⇒ 'a::banach"
assumes "f integrable_on (closed_segment a b)"
assumes "f integrable_on (closed_segment b c)"
assumes "f integrable_on (closed_segment a c)"
shows "ivl_integral a b f + ivl_integral b c f = ivl_integral a c f"
proof -
show ?thesis
using assms
Henstock_Kurzweil_Integration.integral_combine[of a b c f]
Henstock_Kurzweil_Integration.integral_combine[of a c b f]
Henstock_Kurzweil_Integration.integral_combine[of b a c f]
Henstock_Kurzweil_Integration.integral_combine[of b c a f]
Henstock_Kurzweil_Integration.integral_combine[of c a b f]
Henstock_Kurzweil_Integration.integral_combine[of c b a f]
by (cases "a ≤ b"; cases "b ≤ c"; cases "a ≤ c")
(auto simp: algebra_simps ivl_integral_def closed_segment_eq_real_ivl)
qed

lemma integral_equation_swap_initial_value:
fixes x::"real⇒'a::banach"
assumes "⋀t. t ∈ closed_segment t0 t1 ⟹ x t = x t0 + ivl_integral t0 t (λt. f t (x t))"
assumes t: "t ∈ closed_segment t0 t1"
assumes int: "(λt. f t (x t)) integrable_on closed_segment t0 t1"
shows "x t = x t1 + ivl_integral t1 t (λt. f t (x t))"
proof -
from t int have "(λt. f t (x t)) integrable_on closed_segment t0 t"
"(λt. f t (x t)) integrable_on closed_segment t t1"
by (auto intro: integrable_on_subinterval simp: closed_segment_eq_real_ivl split: if_split_asm)
with assms(1)[of t] assms(2-)
have "x t - x t0 = ivl_integral t0 t1 (λt. f t (x t)) + ivl_integral t1 t (λt. f t (x t))"
by (subst ivl_integral_combine) (auto simp: closed_segment_commute)
then have "x t + x t1 - (x t0 + ivl_integral t0 t1 (λt. f t (x t))) =
x t1 + ivl_integral t1 t (λt. f t (x t))"
also have "x t0 + ivl_integral t0 t1 (λt. f t (x t)) = x t1"
by (auto simp: assms(1)[symmetric])
finally show ?thesis  by simp
qed

lemma has_integral_nonpos:
fixes f :: "'n::euclidean_space ⇒ real"
assumes "(f has_integral i) s"
and "∀x∈s. f x ≤ 0"
shows "i ≤ 0"
by (rule has_integral_nonneg[of "-f" "-i" s, simplified])
(auto intro!: has_integral_neg simp: fun_Compl_def assms)

lemma has_ivl_integral_nonneg:
fixes f :: "real ⇒ real"
assumes "(f has_ivl_integral i) a b"
and "⋀x. a ≤ x ⟹ x ≤ b ⟹ 0 ≤ f x"
and "⋀x. b ≤ x ⟹ x ≤ a ⟹ f x ≤ 0"
shows "0 ≤ i"
using assms has_integral_nonneg[of f i "{a .. b}"] has_integral_nonpos[of f "-i" "{b .. a}"]
by (auto simp: has_ivl_integral_def Ball_def not_le split: if_split_asm)

lemma has_ivl_integral_ivl_integral:
"f integrable_on (closed_segment a b) ⟷ (f has_ivl_integral (ivl_integral a b f)) a b"
by (auto simp: closed_segment_eq_real_ivl has_ivl_integral_def ivl_integral_def)

lemma ivl_integral_nonneg:
fixes f :: "real ⇒ real"
assumes "f integrable_on (closed_segment a b)"
and "⋀x. a ≤ x ⟹ x ≤ b ⟹ 0 ≤ f x"
and "⋀x. b ≤ x ⟹ x ≤ a ⟹ f x ≤ 0"
shows "0 ≤ ivl_integral a b f"
by (rule has_ivl_integral_nonneg[OF assms(1)[unfolded has_ivl_integral_ivl_integral] assms(2-3)])

lemma ivl_integral_bound:
fixes f::"real ⇒ 'a::banach"
assumes "continuous_on (closed_segment a b) f"
assumes "⋀t. t ∈ (closed_segment a b) ⟹ norm (f t) ≤ B"
shows "norm (ivl_integral a b f) ≤ B * abs (b - a)"
using integral_bound[of a b f B]
integral_bound[of b a f B]
assms
by (auto simp: closed_segment_eq_real_ivl has_ivl_integral_def ivl_integral_def split: if_splits)

lemma ivl_integral_minus_sets:
fixes f::"real ⇒ 'a::banach"
shows "f integrable_on (closed_segment c a) ⟹ f integrable_on (closed_segment c b) ⟹ f integrable_on (closed_segment a b) ⟹
ivl_integral c a f - ivl_integral c b f = ivl_integral b a f"
using ivl_integral_combine[of f c b a]
by (auto simp: algebra_simps closed_segment_commute)

lemma ivl_integral_minus_sets':
fixes f::"real ⇒ 'a::banach"
shows "f integrable_on (closed_segment a c) ⟹ f integrable_on (closed_segment b c) ⟹ f integrable_on (closed_segment a b) ⟹
ivl_integral a c f - ivl_integral b c f = ivl_integral a b f"
using ivl_integral_combine[of f a b c]
by (auto simp: algebra_simps closed_segment_commute)

end

# Theory Gronwall

theory Gronwall
imports Vector_Derivative_On
begin

subsection ‹Gronwall›

lemma derivative_quotient_bound:
assumes g_deriv_on: "(g has_vderiv_on g') {a .. b}"
assumes frac_le: "⋀t. t ∈ {a .. b} ⟹ g' t / g t ≤ K"
assumes g'_cont: "continuous_on {a .. b} g'"
assumes g_pos: "⋀t. t ∈ {a .. b} ⟹ g t > 0"
assumes t_in: "t ∈ {a .. b}"
shows "g t ≤ g a * exp (K * (t - a))"
proof -
have g_deriv: "⋀t. t ∈ {a .. b} ⟹ (g has_real_derivative g' t) (at t within {a .. b})"
using g_deriv_on
by (auto simp: has_vderiv_on_def has_field_derivative_iff_has_vector_derivative[symmetric])
from assms have g_nonzero: "⋀t. t ∈ {a .. b} ⟹ g t ≠ 0"
by fastforce
have frac_integrable: "⋀t. t ∈ {a .. b} ⟹ (λt. g' t / g t) integrable_on {a..t}"
by (force simp: g_nonzero intro: assms has_field_derivative_subset[OF g_deriv]
continuous_on_subset[OF g'_cont] continuous_intros integrable_continuous_real
continuous_on_subset[OF vderiv_on_continuous_on[OF g_deriv_on]])
have "⋀t. t ∈ {a..b} ⟹ ((λt. g' t / g t) has_integral ln (g t) - ln (g a)) {a .. t}"
by (rule fundamental_theorem_of_calculus)
(auto intro!: derivative_eq_intros assms has_field_derivative_subset[OF g_deriv]
simp: has_field_derivative_iff_has_vector_derivative[symmetric])
hence *: "⋀t. t ∈ {a .. b} ⟹ ln (g t) - ln (g a) = integral {a .. t} (λt. g' t / g t)"
using integrable_integral[OF frac_integrable]
by (rule has_integral_unique[where f = "λt. g' t / g t"])
from * t_in have "ln (g t) - ln (g a) = integral {a .. t} (λt. g' t / g t)" .
also have "… ≤ integral {a .. t} (λ_. K)"
using ‹t ∈ {a .. b}›
by (intro integral_le) (auto intro!: frac_integrable frac_le integral_le)
also have "… = K * (t - a)" using ‹t ∈ {a .. b}›
by simp
finally have "ln (g t) ≤ K * (t - a) + ln (g a)" (is "?lhs ≤ ?rhs")
by simp
hence "exp ?lhs ≤ exp ?rhs"
by simp
thus ?thesis
using ‹t ∈ {a .. b}› g_pos
qed

lemma derivative_quotient_bound_left:
assumes g_deriv_on: "(g has_vderiv_on g') {a .. b}"
assumes frac_ge: "⋀t. t ∈ {a .. b} ⟹ K ≤ g' t / g t"
assumes g'_cont: "continuous_on {a .. b} g'"
assumes g_pos: "⋀t. t ∈ {a .. b} ⟹ g t > 0"
assumes t_in: "t ∈ {a..b}"
shows "g t ≤ g b * exp (K * (t - b))"
proof -
have g_deriv: "⋀t. t ∈ {a .. b} ⟹ (g has_real_derivative g' t) (at t within {a .. b})"
using g_deriv_on
by (auto simp: has_vderiv_on_def has_field_derivative_iff_has_vector_derivative[symmetric])
from assms have g_nonzero: "⋀t. t ∈ {a..b} ⟹ g t ≠ 0"
by fastforce
have frac_integrable: "⋀t. t ∈ {a .. b} ⟹ (λt. g' t / g t) integrable_on {t..b}"
by (force simp: g_nonzero intro: assms has_field_derivative_subset[OF g_deriv]
continuous_on_subset[OF g'_cont] continuous_intros integrable_continuous_real
continuous_on_subset[OF vderiv_on_continuous_on[OF g_deriv_on]])
have "⋀t. t ∈ {a..b} ⟹ ((λt. g' t / g t) has_integral ln (g b) - ln (g t)) {t..b}"
by (rule fundamental_theorem_of_calculus)
(auto intro!: derivative_eq_intros assms has_field_derivative_subset[OF g_deriv]
simp: has_field_derivative_iff_has_vector_derivative[symmetric])
hence *: "⋀t. t ∈ {a..b} ⟹ ln (g b) - ln (g t) = integral {t..b} (λt. g' t / g t)"
using integrable_integral[OF frac_integrable]
by (rule has_integral_unique[where f = "λt. g' t / g t"])
have "K * (b - t) = integral {t..b} (λ_. K)"
using ‹t ∈ {a..b}›
by simp
also have "... ≤ integral {t..b} (λt. g' t / g t)"
using ‹t ∈ {a..b}›
by (intro integral_le) (auto intro!: frac_integrable frac_ge integral_le)
also have "... = ln (g b) - ln (g t)"
using * t_in by simp
finally have "K * (b - t) + ln (g t) ≤ ln (g b)" (is "?lhs ≤ ?rhs")
by simp
hence "exp ?lhs ≤ exp ?rhs"
by simp
hence "g t * exp (K * (b - t)) ≤ g b"
using ‹t ∈ {a..b}› g_pos
hence "g t / exp (K * (t - b)) ≤ g b"
thus ?thesis
qed

lemma gronwall_general:
fixes g K C a b and t::real
defines "G ≡ λt. C + K * integral {a..t} (λs. g s)"
assumes g_le_G: "⋀t. t ∈ {a..b} ⟹ g t ≤ G t"
assumes g_cont: "continuous_on {a..b} g"
assumes g_nonneg: "⋀t. t ∈ {a..b} ⟹ 0 ≤ g t"
assumes pos: "0 < C" "K > 0"
assumes "t ∈ {a..b}"
shows "g t ≤ C * exp (K * (t - a))"
proof -
have G_pos: "⋀t. t ∈ {a..b} ⟹ 0 < G t"
by (auto simp: G_def intro!: add_pos_nonneg mult_nonneg_nonneg Henstock_Kurzweil_Integration.integral_nonneg
integrable_continuous_real assms intro: less_imp_le continuous_on_subset)
have "g t ≤ G t" using assms by auto
also
{
have "(G has_vderiv_on (λt. K * g t)) {a..b}"
by (auto intro!: derivative_eq_intros integral_has_vector_derivative g_cont
moreover
{
fix t assume "t ∈ {a..b}"
hence "K * g t / G t ≤ K * G t / G t"
using pos g_le_G G_pos
by (intro divide_right_mono mult_left_mono) (auto intro!: less_imp_le)
also have "… = K"
using G_pos[of t] ‹t ∈ {a .. b}› by simp
finally have "K * g t / G t ≤ K" .
}
ultimately have "G t ≤ G a * exp (K * (t - a))"
apply (rule derivative_quotient_bound)
using ‹t ∈ {a..b}›
by (auto intro!: continuous_intros g_cont G_pos simp: field_simps pos)
}
also have "G a = C"
finally show ?thesis
by simp
qed

lemma gronwall_general_left:
fixes g K C a b and t::real
defines "G ≡ λt. C + K * integral {t..b} (λs. g s)"
assumes g_le_G: "⋀t. t ∈ {a..b} ⟹ g t ≤ G t"
assumes g_cont: "continuous_on {a..b} g"
assumes g_nonneg: "⋀t. t ∈ {a..b} ⟹ 0 ≤ g t"
assumes pos: "0 < C" "K > 0"
assumes "t ∈ {a..b}"
shows "g t ≤ C * exp (-K * (t - b))"
proof -
have G_pos: "⋀t. t ∈ {a..b} ⟹ 0 < G t"
by (auto simp: G_def intro!: add_pos_nonneg mult_nonneg_nonneg Henstock_Kurzweil_Integration.integral_nonneg
integrable_continuous_real assms intro: less_imp_le continuous_on_subset)
have "g t ≤ G t" using assms by auto
also
{
have "(G has_vderiv_on (λt. -K * g t)) {a..b}"
by (auto intro!: derivative_eq_intros g_cont integral_has_vector_derivative'
moreover
{
fix t assume "t ∈ {a..b}"
hence "K * g t / G t ≤ K * G t / G t"
using pos g_le_G G_pos
by (intro divide_right_mono mult_left_mono) (auto intro!: less_imp_le)
also have "… = K"
using G_pos[of t] ‹t ∈ {a .. b}› by simp
finally have "K * g t / G t ≤ K" .
hence "-K ≤ -K * g t / G t"
by simp
}
ultimately
have "G t ≤ G b * exp (-K * (t - b))"
apply (rule derivative_quotient_bound_left)
using ‹t ∈ {a..b}›
by (auto intro!: continuous_intros g_cont G_pos simp: field_simps pos)
}
also have "G b = C"
finally show ?thesis
by simp
qed

lemma gronwall_general_segment:
fixes a b::real
assumes "⋀t. t ∈ closed_segment a b ⟹ g t ≤ C + K * integral (closed_segment a t) g"
and "continuous_on (closed_segment a b) g"
and "⋀t. t ∈ closed_segment a b ⟹ 0 ≤ g t"
and "0 < C"
and "0 < K"
and "t ∈ closed_segment a b"
shows "g t ≤ C * exp (K * abs (t - a))"
proof cases
assume "a ≤ b"
then have *: "abs (t - a) = t -a" using assms by (auto simp: closed_segment_eq_real_ivl)
show ?thesis
unfolding *
using assms
by (intro gronwall_general[where b=b]) (auto intro!: simp: closed_segment_eq_real_ivl ‹a ≤ b›)
next
assume "¬a ≤ b"
then have *: "K * abs (t - a) = - K * (t - a)" using assms by (auto simp: closed_segment_eq_real_ivl algebra_simps)
{
fix s :: real
assume a1: "b ≤ s"
assume a2: "s ≤ a"
assume a3: "⋀t. b ≤ t ∧ t ≤ a ⟹ g t ≤ C + K * integral (if a ≤ t then {a..t} else {t..a}) g"
have "s = a ∨ s < a"
using a2 by (meson less_eq_real_def)
then have "g s ≤ C + K * integral {s..a} g"
using a3 a1 by fastforce
} then show ?thesis
unfolding *
using assms  ‹¬a ≤ b›
by (intro gronwall_general_left)
(auto intro!: simp: closed_segment_eq_real_ivl)
qed

lemma gronwall_more_general_segment:
fixes a b c::real
assumes "⋀t. t ∈ closed_segment a b ⟹ g t ≤ C + K * integral (closed_segment c t) g"
and cont: "continuous_on (closed_segment a b) g"
and "⋀t. t ∈ closed_segment a b ⟹ 0 ≤ g t"
and "0 < C"
and "0 < K"
and t: "t ∈ closed_segment a b"
and c: "c ∈ closed_segment a b"
shows "g t ≤ C * exp (K * abs (t - c))"
proof -
from t c have "t ∈ closed_segment c a ∨ t ∈ closed_segment c b"
by (auto simp: closed_segment_eq_real_ivl split_ifs)
then show ?thesis
proof
assume "t ∈ closed_segment c a"
moreover
have subs: "closed_segment c a ⊆ closed_segment a b" using t c
by (auto simp: closed_segment_eq_real_ivl split_ifs)
ultimately show ?thesis
by (intro gronwall_general_segment[where b=a])
(auto intro!: assms intro: continuous_on_subset)
next
assume "t ∈ closed_segment c b"
moreover
have subs: "closed_segment c b ⊆ closed_segment a b" using t c
by (auto simp: closed_segment_eq_real_ivl)
ultimately show ?thesis
by (intro gronwall_general_segment[where b=b])
(auto intro!: assms intro: continuous_on_subset)
qed
qed

lemma gronwall:
fixes g K C and t::real
defines "G ≡ λt. C + K * integral {0..t} (λs. g s)"
assumes g_le_G: "⋀t. 0 ≤ t ⟹ t ≤ a ⟹ g t ≤ G t"
assumes g_cont: "continuous_on {0..a} g"
assumes g_nonneg: "⋀t. 0 ≤ t ⟹ t ≤ a ⟹ 0 ≤ g t"
assumes pos: "0 < C" "0 < K"
assumes "0 ≤ t" "t ≤ a"
shows "g t ≤ C * exp (K * t)"
apply(rule gronwall_general[where a=0, simplified, OF assms(2-6)[unfolded G_def]])
using assms(7,8)
by simp_all

lemma gronwall_left:
fixes g K C and t::real
defines "G ≡ λt. C + K * integral {t..0} (λs. g s)"
assumes g_le_G: "⋀t. a ≤ t ⟹ t ≤ 0 ⟹ g t ≤ G t"
assumes g_cont: "continuous_on {a..0} g"
assumes g_nonneg: "⋀t. a ≤ t ⟹ t ≤ 0 ⟹ 0 ≤ g t"
assumes pos: "0 < C" "0 < K"
assumes "a ≤ t" "t ≤ 0"
shows "g t ≤ C * exp (-K * t)"
apply(simp, rule gronwall_general_left[where b=0, simplified, OF assms(2-6)[unfolded G_def]])
using assms(7,8)
by simp_all

end

# 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}"

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"
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"
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)
― ‹TODO: no idea about mixfix and precedences, check this!›
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"― ‹TODO: weaken this assumption?!›
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"
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"
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"― ‹TODO: weaken this assumption?!›
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)"
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"
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)"
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

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"

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"

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"

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

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"
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"
} 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
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 (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― ‹solution until t1›
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
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"
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)"
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"
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"
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
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"
then show ?thesis using that
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"
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"
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"]
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 (rule refl)
apply (rule refl)
apply (rule refl)
apply (rule refl)
using l.fixed_point_usolves_ode
apply -
apply (simp)
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 `