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}" ― ‹generalize?› 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