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