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