# Theory 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
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
hence "g t / exp (K * (t - b)) ≤ g b"
thus ?thesis
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
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"
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'
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"
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```