Theory Ordinary_Differential_Equations.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}"
  ― ‹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 "za. 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