Theory Upper_Lower_Solution
section ‹Upper and Lower Solutions›
theory Upper_Lower_Solution
imports Flow
begin
text ‹Following Walter~\<^cite>‹"walter"› in section 9›
lemma IVT_min:
fixes f :: "real ⇒ 'b :: {linorder_topology,real_normed_vector,ordered_real_vector}"
assumes y: "f a ≤ y" "y ≤ f b" "a ≤ b"
assumes *: "continuous_on {a .. b} f"
notes [continuous_intros] = *[THEN continuous_on_subset]
obtains x where "a ≤ x" "x ≤ b" "f x = y" "⋀x'. a ≤ x' ⟹ x' < x ⟹ f x' < y"
proof -
let ?s = "((λx. f x - y) -` {0..}) ∩ {a..b}"
have "?s ≠ {}"
using assms
by auto
have "closed ?s"
by (rule closed_vimage_Int) (auto intro!: continuous_intros)
moreover have "bounded ?s"
by (rule bounded_Int) (simp add: bounded_closed_interval)
ultimately have "compact ?s"
using compact_eq_bounded_closed by blast
from compact_attains_inf[OF this ‹?s ≠ {}›]
obtain x where x: "a ≤ x" "x ≤ b" "f x ≥ y"
and min: "⋀z. a ≤ z ⟹ z ≤ b ⟹ f z ≥ y ⟹ x ≤ z"
by auto
have "f x ≤ y"
proof (rule ccontr)
assume n: "¬ f x ≤ y"
then have "∃z≥a. z ≤ x ∧ (λx. f x - y) z = 0"
using x by (intro IVT') (auto intro!: continuous_intros simp: assms)
then obtain z where z: "a ≤ z" "z ≤ x" "f z = y" by auto
then have "a ≤ z" "z ≤ b" "f z ≥ y" using x by auto
from min [OF this] z n
show False by auto
qed
then have "a ≤ x" "x ≤ b" "f x = y"
using x
by (auto )
moreover have "f x' < y" if "a ≤ x'" "x' < x" for x'
apply (rule ccontr)
using min[of x'] that x
by (auto simp: not_less)
ultimately show ?thesis ..
qed
lemma filtermap_at_left_shift: "filtermap (λx. x - d) (at_left a) = at_left (a - d::real)"
by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_shift[symmetric])
context
fixes v v' w w'::"real ⇒ real" and t0 t1 e::real
assumes v': "(v has_vderiv_on v') {t0 <.. t1}"
and w': "(w has_vderiv_on w') {t0 <.. t1}"
assumes pos_ivl: "t0 < t1"
assumes e_pos: "e > 0" and e_in: "t0 + e ≤ t1"
assumes less: "⋀t. t0 < t ⟹ t < t0 + e ⟹ v t < w t"
begin
lemma first_intersection_crossing_derivatives:
assumes na: "t0 < tg" "tg ≤ t1" "v tg ≥ w tg"
notes [continuous_intros] =
vderiv_on_continuous_on[OF v', THEN continuous_on_subset]
vderiv_on_continuous_on[OF w', THEN continuous_on_subset]
obtains x0 where
"t0 < x0" "x0 ≤ tg"
"v' x0 ≥ w' x0"
"v x0 = w x0"
"⋀t. t0 < t ⟹ t < x0 ⟹ v t < w t"
proof -
have "(v - w) (min tg (t0 + e / 2)) ≤ 0" "0 ≤ (v - w) tg"
"min tg (t0 + e / 2) ≤ tg"
"continuous_on {min tg (t0 + e / 2)..tg} (v - w)"
using less[of "t0 + e / 2"]
less[of tg]na ‹e > 0›
by (auto simp: min_def intro!: continuous_intros)
from IVT_min[OF this]
obtain x0 where x0: "min tg (t0 + e / 2) ≤ x0" "x0 ≤ tg" "v x0 = w x0"
"⋀x'. min tg (t0 + e / 2) ≤ x' ⟹ x' < x0 ⟹ v x' < w x'"
by auto
then have x0_in: "t0 < x0" "x0 ≤ t1"
using ‹e > 0› na(1,2)
by (auto)
note ‹t0 < x0› ‹x0 ≤ tg›
moreover
{
from v' x0_in
have "(v has_derivative (λx. x * v' x0)) (at x0 within {t0<..<x0})"
by (force intro: has_derivative_subset simp: has_vector_derivative_def has_vderiv_on_def)
then have v: "((λy. (v y - (v x0 + (y - x0) * v' x0)) / norm (y - x0)) ⤏ 0) (at x0 within {t0<..<x0})"
unfolding has_derivative_within
by (simp add: ac_simps)
from w' x0_in
have "(w has_derivative (λx. x * w' x0)) (at x0 within {t0<..<x0})"
by (force intro: has_derivative_subset simp: has_vector_derivative_def has_vderiv_on_def)
then have w: "((λy. (w y - (w x0 + (y - x0) * w' x0)) / norm (y - x0)) ⤏ 0) (at x0 within {t0<..<x0})"
unfolding has_derivative_within
by (simp add: ac_simps)
have evs: "∀⇩F x in at x0 within {t0<..<x0}. min tg (t0 + e / 2) < x"
"∀⇩F x in at x0 within {t0<..<x0}. t0 < x ∧ x < x0"
using less na(1) na(3) x0(3) x0_in(1)
by (force simp: min_def eventually_at_filter intro!: order_tendstoD[OF tendsto_ident_at])+
then have "∀⇩F x in at x0 within {t0<..<x0}.
(v x - (v x0 + (x - x0) * v' x0)) / norm (x - x0) - (w x - (w x0 + (x - x0) * w' x0)) / norm (x - x0) =
(v x - w x) / norm (x - x0) + (v' x0 - w' x0)"
apply eventually_elim
using x0_in x0 less na ‹t0 < t1› sum_sqs_eq
by (auto simp: divide_simps algebra_simps min_def intro!: eventuallyI split: if_split_asm)
from this tendsto_diff[OF v w]
have 1: "((λx. (v x - w x) / norm (x - x0) + (v' x0 - w' x0)) ⤏ 0) (at x0 within {t0<..<x0})"
by (force intro: tendsto_eq_rhs Lim_transform_eventually)
moreover
from evs have 2: "∀⇩F x in at x0 within {t0<..<x0}. (v x - w x) / norm (x - x0) + (v' x0 - w' x0) ≤ (v' x0 - w' x0)"
by eventually_elim (auto simp: divide_simps intro!: less_imp_le x0(4))
moreover
have "at x0 within {t0<..<x0} ≠ bot"
by (simp add: ‹t0 < x0› at_within_eq_bot_iff less_imp_le)
ultimately
have "0 ≤ v' x0 - w' x0"
by (rule tendsto_upperbound)
then have "v' x0 ≥ w' x0" by simp
}
moreover note ‹v x0 = w x0›
moreover
have "t0 < t ⟹ t < x0 ⟹ v t < w t" for t
by (cases "min tg (t0 + e / 2) ≤ t") (auto intro: x0 less)
ultimately show ?thesis ..
qed
lemma defect_less:
assumes b: "⋀t. t0 < t ⟹ t ≤ t1 ⟹ v' t - f t (v t) < w' t - f t (w t)"
notes [continuous_intros] =
vderiv_on_continuous_on[OF v', THEN continuous_on_subset]
vderiv_on_continuous_on[OF w', THEN continuous_on_subset]
shows "∀t ∈ {t0 <.. t1}. v t < w t"
proof (rule ccontr)
assume " ¬ (∀t∈{t0 <.. t1}. v t < w t)"
then obtain tu where "t0 < tu" "tu ≤ t1" "v tu ≥ w tu" by auto
from first_intersection_crossing_derivatives[OF this]
obtain x0 where "t0 < x0" "x0 ≤ tu" "w' x0 ≤ v' x0" "v x0 = w x0" "⋀t. t0 < t ⟹ t < x0 ⟹ v t < w t"
by metis
with b[of x0] ‹tu ≤ t1›
show False
by simp
qed
end
lemma has_derivatives_less_lemma:
fixes v v' ::"real ⇒ real"
assumes v': "(v has_vderiv_on v') T"
assumes y': "(y has_vderiv_on y') T"
assumes lu: "⋀t. t ∈ T ⟹ t > t0 ⟹ v' t - f t (v t) < y' t - f t (y t)"
assumes lower: "v t0 ≤ y t0"
assumes eq_imp: "v t0 = y t0 ⟹ v' t0 < y' t0"
assumes t: "t0 < t" "t0 ∈ T" "t ∈ T" "is_interval T"
shows "v t < y t"
proof -
have subset: "{t0 .. t} ⊆ T"
by (rule atMostAtLeast_subset_convex) (auto simp: assms is_interval_convex)
obtain d where "0 < d" "t0 < s ⟹ s ≤ t ⟹ s < t0 + d ⟹ v s < y s" for s
proof cases
assume "v t0 = y t0"
from this[THEN eq_imp]
have *: "0 < y' t0 - v' t0"
by simp
have "((λt. y t - v t) has_vderiv_on (λt0. y' t0 - v' t0)) {t0 .. t}"
by (auto intro!: derivative_intros y' v' has_vderiv_on_subset[OF _ subset])
with ‹t0 < t›
have d: "((λt. y t - v t) has_real_derivative y' t0 - v' t0) (at t0 within {t0 .. t})"
by (auto simp: has_vderiv_on_def has_real_derivative_iff_has_vector_derivative)
from has_real_derivative_pos_inc_right[OF d *] ‹v t0 = y t0›
obtain d where "d > 0" and vy: "h > 0 ⟹ t0 + h ≤ t ⟹ h < d ⟹ v (t0 + h) < y (t0 + h)" for h
by auto
have vy: "t0 < s ⟹ s ≤ t ⟹ s < t0 + d ⟹ v s < y s" for s
using vy[of "s - t0"] by simp
with ‹d > 0› show ?thesis ..
next
assume "v t0 ≠ y t0"
then have "v t0 < y t0" using lower by simp
moreover
have "continuous_on {t0 .. t} v" "continuous_on {t0 .. t} y"
by (auto intro!: vderiv_on_continuous_on assms has_vderiv_on_subset[OF _ subset])
then have "(v ⤏ v t0) (at t0 within {t0 .. t})" "(y ⤏ y t0) (at t0 within {t0 .. t})"
by (auto simp: continuous_on)
ultimately have "∀⇩F x in at t0 within {t0 .. t}. 0 < y x - v x"
by (intro order_tendstoD) (auto intro!: tendsto_eq_intros)
then obtain d where "d > 0" "⋀x. t0 < x ⟹ x ≤ t ⟹ x < t0 + d ⟹ v x < y x"
by atomize_elim (auto simp: eventually_at algebra_simps dist_real_def)
then show ?thesis ..
qed
with ‹d > 0› ‹t0 < t›
obtain e where "e > 0" "t0 + e ≤ t" "t0 < s ⟹ s < t0 + e ⟹ v s < y s" for s
by atomize_elim (auto simp: min_def divide_simps intro!: exI[where x="min (d/2) ((t - t0) / 2)"]
split: if_split_asm)
from defect_less[
OF has_vderiv_on_subset[OF v']
has_vderiv_on_subset[OF y']
‹t0 < t›
this lu]
show "v t < y t" using ‹t0 < t› subset
by (auto simp: subset_iff assms)
qed
lemma strict_lower_solution:
fixes v v' ::"real ⇒ real"
assumes sol: "(y solves_ode f) T X"
assumes v': "(v has_vderiv_on v') T"
assumes lower: "⋀t. t ∈ T ⟹ t > t0 ⟹ v' t < f t (v t)"
assumes iv: "v t0 ≤ y t0" "v t0 = y t0 ⟹ v' t0 < f t0 (y t0)"
assumes t: "t0 < t" "t0 ∈ T" "t ∈ T" "is_interval T"
shows "v t < y t"
proof -
note v'
moreover
note solves_odeD(1)[OF sol]
moreover
have 3: "v' t - f t (v t) < f t (y t) - f t (y t)" if "t ∈ T" "t > t0" for t
using lower(1)[OF that]
by arith
moreover note iv
moreover note t
ultimately
show "v t < y t"
by (rule has_derivatives_less_lemma)
qed
lemma strict_upper_solution:
fixes w w'::"real ⇒ real"
assumes sol: "(y solves_ode f) T X"
assumes w': "(w has_vderiv_on w') T"
and upper: "⋀t. t ∈ T ⟹ t > t0 ⟹ f t (w t) < w' t"
and iv: "y t0 ≤ w t0" "y t0 = w t0 ⟹ f t0 (y t0) < w' t0"
assumes t: "t0 < t" "t0 ∈ T" "t ∈ T" "is_interval T"
shows "y t < w t"
proof -
note solves_odeD(1)[OF sol]
moreover
note w'
moreover
have "f t (y t) - f t (y t) < w' t - f t (w t)" if "t ∈ T" "t > t0" for t
using upper(1)[OF that]
by arith
moreover note iv
moreover note t
ultimately
show "y t < w t"
by (rule has_derivatives_less_lemma)
qed
lemma uniform_limit_at_within_subset:
assumes "uniform_limit S x l (at t within T)"
assumes "U ⊆ T"
shows "uniform_limit S x l (at t within U)"
by (metis assms(1) assms(2) eventually_within_Un filterlim_iff subset_Un_eq)
lemma uniform_limit_le:
fixes f::"'c ⇒ 'a ⇒ 'b::{metric_space, linorder_topology}"
assumes I: "I ≠ bot"
assumes u: "uniform_limit X f g I"
assumes u': "uniform_limit X f' g' I"
assumes "∀⇩F i in I. ∀x ∈ X. f i x ≤ f' i x"
assumes "x ∈ X"
shows "g x ≤ g' x"
proof -
have "∀⇩F i in I. f i x ≤ f' i x" using assms by (simp add: eventually_mono)
with I tendsto_uniform_limitI[OF u' ‹x ∈ X›] tendsto_uniform_limitI[OF u ‹x ∈ X›]
show ?thesis by (rule tendsto_le)
qed
lemma uniform_limit_le_const:
fixes f::"'c ⇒ 'a ⇒ 'b::{metric_space, linorder_topology}"
assumes I: "I ≠ bot"
assumes u: "uniform_limit X f g I"
assumes "∀⇩F i in I. ∀x ∈ X. f i x ≤ h x"
assumes "x ∈ X"
shows "g x ≤ h x"
proof -
have "∀⇩F i in I. f i x ≤ h x" using assms by (simp add: eventually_mono)
then show ?thesis by (metis tendsto_upperbound I tendsto_uniform_limitI[OF u ‹x ∈ X›])
qed
lemma uniform_limit_ge_const:
fixes f::"'c ⇒ 'a ⇒ 'b::{metric_space, linorder_topology}"
assumes I: "I ≠ bot"
assumes u: "uniform_limit X f g I"
assumes "∀⇩F i in I. ∀x ∈ X. h x ≤ f i x"
assumes "x ∈ X"
shows "h x ≤ g x"
proof -
have "∀⇩F i in I. h x ≤ f i x" using assms by (simp add: eventually_mono)
then show ?thesis by (metis tendsto_lowerbound I tendsto_uniform_limitI[OF u ‹x ∈ X›])
qed
locale ll_on_open_real = ll_on_open T f X for T f and X::"real set"
begin
lemma lower_solution:
fixes v v' ::"real ⇒ real"
assumes sol: "(y solves_ode f) S X"
assumes v': "(v has_vderiv_on v') S"
assumes lower: "⋀t. t ∈ S ⟹ t > t0 ⟹ v' t < f t (v t)"
assumes iv: "v t0 ≤ y t0"
assumes t: "t0 ≤ t" "t0 ∈ S" "t ∈ S" "is_interval S" "S ⊆ T"
shows "v t ≤ y t"
proof cases
assume "v t0 = y t0"
have "{t0 -- t} ⊆ S" using t by (simp add: closed_segment_subset is_interval_convex)
with sol have "(y solves_ode f) {t0 -- t} X" using order_refl by (rule solves_ode_on_subset)
moreover note refl
moreover
have "{t0 -- t} ⊆ T" using ‹{t0 -- t} ⊆ S› ‹S ⊆ T› by (rule order_trans)
ultimately have t_ex: "t ∈ existence_ivl t0 (y t0)"
by (rule existence_ivl_maximal_segment)
have t0_ex: "t0 ∈ existence_ivl t0 (y t0)"
using in_existence_between_zeroI t_ex by blast
have "t0 ∈ T" using assms(9) t(2) by blast
from uniform_limit_flow[OF t0_ex t_ex] ‹t0 ≤ t›
have "uniform_limit {t0..t} (flow t0) (flow t0 (y t0)) (at (y t0))" by simp
then have "uniform_limit {t0..t} (flow t0) (flow t0 (y t0)) (at_right (y t0))"
by (rule uniform_limit_at_within_subset) simp
moreover
{
have "∀⇩F i in at (y t0). t ∈ existence_ivl t0 i"
by (rule eventually_mem_existence_ivl) fact
then have "∀⇩F i in at_right (y t0). t ∈ existence_ivl t0 i"
unfolding eventually_at_filter
by eventually_elim simp
moreover have "∀⇩F i in at_right (y t0). i ∈ X"
proof -
have f1: "⋀r ra rb. r ∉ existence_ivl ra rb ∨ rb ∈ X"
by (metis existence_ivl_reverse flow_in_domain flows_reverse)
obtain rr :: "(real ⇒ bool) ⇒ (real ⇒ bool) ⇒ real" where
"⋀p f pa fa. (¬ eventually p f ∨ eventually pa f ∨ p (rr p pa)) ∧
(¬ eventually p fa ∨ ¬ pa (rr p pa) ∨ eventually pa fa)"
by (metis (no_types) eventually_mono)
then show ?thesis
using f1 calculation by meson
qed
moreover have "∀⇩F i in at_right (y t0). y t0 < i"
by (simp add: eventually_at_filter)
ultimately have "∀⇩F i in at_right (y t0). ∀x∈{t0..t}. v x ≤ flow t0 i x"
proof eventually_elim
case (elim y')
show ?case
proof safe
fix s assume s: "s ∈ {t0..t}"
show "v s ≤ flow t0 y' s"
proof cases
assume "s = t0" with elim iv show ?thesis
by (simp add: ‹t0 ∈ T› ‹y' ∈ X›)
next
assume "s ≠ t0" with s have "t0 < s" by simp
have "{t0 -- s} ⊆ S" using ‹{t0--t} ⊆ S› closed_segment_eq_real_ivl s by auto
from s elim have "{t0..s} ⊆ existence_ivl t0 y'"
using ivl_subset_existence_ivl by blast
with flow_solves_ode have sol: "(flow t0 y' solves_ode f) {t0 .. s} X"
by (rule solves_ode_on_subset) (auto intro!: ‹y' ∈ X› ‹t0 ∈ T›)
have "{t0 .. s} ⊆ S" using ‹{t0 -- s} ⊆ S› by (simp add: closed_segment_eq_real_ivl split: if_splits)
with v' have v': "(v has_vderiv_on v') {t0 .. s}"
by (rule has_vderiv_on_subset)
from ‹y t0 < y'› ‹v t0 = y t0› have less_init: "v t0 < flow t0 y' t0"
by (simp add: flow_initial_time_if ‹t0 ∈ T› ‹y' ∈ X›)
from strict_lower_solution[OF sol v' lower less_imp_le[OF less_init] _ ‹t0 < s›]
‹{t0 .. s} ⊆ S›
less_init ‹t0 < s›
have "v s < flow t0 y' s" by (simp add: subset_iff is_interval_cc)
then show ?thesis by simp
qed
qed
qed
}
moreover have "t ∈ {t0 .. t}" using ‹t0 ≤ t› by simp
ultimately have "v t ≤ flow t0 (y t0) t"
by (rule uniform_limit_ge_const[OF trivial_limit_at_right_real])
also have "flow t0 (y t0) t = y t"
using sol t
by (intro maximal_existence_flow) auto
finally show ?thesis .
next
assume "v t0 ≠ y t0" then have less: "v t0 < y t0" using iv by simp
show ?thesis
apply (cases "t0 = t")
subgoal using iv by blast
subgoal using strict_lower_solution[OF sol v' lower iv] less t by force
done
qed
lemma upper_solution:
fixes v v' ::"real ⇒ real"
assumes sol: "(y solves_ode f) S X"
assumes v': "(v has_vderiv_on v') S"
assumes upper: "⋀t. t ∈ S ⟹ t > t0 ⟹ f t (v t) < v' t"
assumes iv: "y t0 ≤ v t0"
assumes t: "t0 ≤ t" "t0 ∈ S" "t ∈ S" "is_interval S" "S ⊆ T"
shows "y t ≤ v t"
proof cases
assume "v t0 = y t0"
have "{t0 -- t} ⊆ S" using t by (simp add: closed_segment_subset is_interval_convex)
with sol have "(y solves_ode f) {t0 -- t} X" using order_refl by (rule solves_ode_on_subset)
moreover note refl
moreover
have "{t0 -- t} ⊆ T" using ‹{t0 -- t} ⊆ S› ‹S ⊆ T› by (rule order_trans)
ultimately have t_ex: "t ∈ existence_ivl t0 (y t0)"
by (rule existence_ivl_maximal_segment)
have t0_ex: "t0 ∈ existence_ivl t0 (y t0)"
using in_existence_between_zeroI t_ex by blast
have "t0 ∈ T" using assms(9) t(2) by blast
from uniform_limit_flow[OF t0_ex t_ex] ‹t0 ≤ t›
have "uniform_limit {t0..t} (flow t0) (flow t0 (y t0)) (at (y t0))" by simp
then have "uniform_limit {t0..t} (flow t0) (flow t0 (y t0)) (at_left (y t0))"
by (rule uniform_limit_at_within_subset) simp
moreover
{
have "∀⇩F i in at (y t0). t ∈ existence_ivl t0 i"
by (rule eventually_mem_existence_ivl) fact
then have "∀⇩F i in at_left (y t0). t ∈ existence_ivl t0 i"
unfolding eventually_at_filter
by eventually_elim simp
moreover have "∀⇩F i in at_left (y t0). i ∈ X"
proof -
have f1: "⋀r ra rb. r ∉ existence_ivl ra rb ∨ rb ∈ X"
by (metis existence_ivl_reverse flow_in_domain flows_reverse)
obtain rr :: "(real ⇒ bool) ⇒ (real ⇒ bool) ⇒ real" where
"⋀p f pa fa. (¬ eventually p f ∨ eventually pa f ∨ p (rr p pa)) ∧
(¬ eventually p fa ∨ ¬ pa (rr p pa) ∨ eventually pa fa)"
by (metis (no_types) eventually_mono)
then show ?thesis
using f1 calculation by meson
qed
moreover have "∀⇩F i in at_left (y t0). i < y t0"
by (simp add: eventually_at_filter)
ultimately have "∀⇩F i in at_left (y t0). ∀x∈{t0..t}. flow t0 i x ≤ v x"
proof eventually_elim
case (elim y')
show ?case
proof safe
fix s assume s: "s ∈ {t0..t}"
show "flow t0 y' s ≤ v s"
proof cases
assume "s = t0" with elim iv show ?thesis
by (simp add: ‹t0 ∈ T› ‹y' ∈ X›)
next
assume "s ≠ t0" with s have "t0 < s" by simp
have "{t0 -- s} ⊆ S" using ‹{t0--t} ⊆ S› closed_segment_eq_real_ivl s by auto
from s elim have "{t0..s} ⊆ existence_ivl t0 y'"
using ivl_subset_existence_ivl by blast
with flow_solves_ode have sol: "(flow t0 y' solves_ode f) {t0 .. s} X"
by (rule solves_ode_on_subset) (auto intro!: ‹y' ∈ X› ‹t0 ∈ T›)
have "{t0 .. s} ⊆ S" using ‹{t0 -- s} ⊆ S› by (simp add: closed_segment_eq_real_ivl split: if_splits)
with v' have v': "(v has_vderiv_on v') {t0 .. s}"
by (rule has_vderiv_on_subset)
from ‹y' < y t0› ‹v t0 = y t0› have less_init: "flow t0 y' t0 < v t0"
by (simp add: flow_initial_time_if ‹t0 ∈ T› ‹y' ∈ X›)
from strict_upper_solution[OF sol v' upper less_imp_le[OF less_init] _ ‹t0 < s›]
‹{t0 .. s} ⊆ S›
less_init ‹t0 < s›
have "flow t0 y' s < v s" by (simp add: subset_iff is_interval_cc)
then show ?thesis by simp
qed
qed
qed
}
moreover have "t ∈ {t0 .. t}" using ‹t0 ≤ t› by simp
ultimately have "flow t0 (y t0) t ≤ v t"
by (rule uniform_limit_le_const[OF trivial_limit_at_left_real])
also have "flow t0 (y t0) t = y t"
using sol t
by (intro maximal_existence_flow) auto
finally show ?thesis .
next
assume "v t0 ≠ y t0" then have less: "y t0 < v t0" using iv by simp
show ?thesis
apply (cases "t0 = t")
subgoal using iv by blast
subgoal using strict_upper_solution[OF sol v' upper iv] less t by force
done
qed
end
end