Theory Ordinary_Differential_Equations.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_real_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_real_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
    by (simp add: ac_simps exp_add del: exp_le_cancel_iff)
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_real_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_real_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
    by (simp add: ac_simps exp_add del: exp_le_cancel_iff)
  hence "g t / exp (K * (t - b))  g b"
    by (simp add: algebra_simps exp_diff)
  thus ?thesis
    by (simp add: field_simps)
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
        simp add: G_def has_vderiv_on_def)
    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"
    by (simp add: G_def)
  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'
          simp add: G_def has_vderiv_on_def)
    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"
    by (simp add: G_def)
  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