Grönwall-type estimates #
Mathlib's Grönwall inequality (le_gronwallBound_of_liminf_deriv_right_le) bounds a function by
a bound on its derivative. Energy estimates for evolution equations instead produce a bound on a
function by an integral of itself: a continuous φ with φ t ≤ c + K ∫ₐᵗ φ on [a, b], for
some K ≥ 0. This file proves that such a φ satisfies φ t ≤ c exp (K (t - a))
(TauCeti.le_mul_exp_of_le_add_mul_integral).
The hypothesis K ≥ 0 cannot be dropped: a very negative stretch of φ makes c + K ∫ₐᵗ φ
large when K < 0.
For a monotone g the differential form needs neither continuity nor differentiability: if
k g ≤ g' at almost every point of [s, t] and g s ≥ 0, then g s exp (∫ₛᵗ k) ≤ g t
(TauCeti.mul_exp_integral_le_of_mul_le_deriv), because the derivative of the monotone function
log g integrates to at most its increment.
It also writes Mathlib's gronwallBound with a negative rate -λ in terms of the exponential
integral E_λ(T) = ∫₀ᵀ e^{λr} dr (TauCeti.exp_mul_gronwallBound_neg), and records that
E_λ(T) > 0 for T > 0 (TauCeti.integral_exp_mul_pos), that z ↦ E_λ(z - t) has derivative 1
at t (TauCeti.hasDerivAt_integral_exp_mul_sub), and E_λ(T) ≤ T e^{|λ|T}
(TauCeti.integral_exp_mul_le).
Finally, it specializes Mathlib's inequality to exponential decay: a function whose derivative
satisfies g' ≤ -λ g on [T, ∞) is bounded by g T exp (-λ (t - T)) there
(TauCeti.le_mul_exp_of_hasDerivAt_le_neg_mul), hence by C exp (-λ t) for large t
(TauCeti.exists_le_mul_exp_atTop_of_hasDerivAt_le_neg_mul).
Mathlib's uniqueness statement eq_zero_of_abs_deriv_le_mul_abs_self_of_eq_zero_right propagates
the vanishing of a function with ‖f'‖ ≤ K ‖f‖ forward from the left endpoint of an interval.
Reversing time gives the two-sided version: on [a, b] such a function vanishes identically as
soon as it vanishes at one point (TauCeti.eq_zero_of_norm_deriv_le_mul_norm_self_of_mem_Icc).
The general closed-interval bound is supplied by
TauCeti.norm_le_gronwallBound_of_norm_derivWithin_le; its interior-derivative variant is
TauCeti.norm_le_gronwallBound_of_norm_deriv_le. This is the uniqueness argument for linear
differential equations by energy estimates.
Averaging the reversed Grönwall bound over [s, s + 1] shows that such a function, if it is
square integrable on the line, is bounded by its L² norm: ‖f s‖² ≤ exp (2 K) ∫ ‖f‖²
(TauCeti.norm_sq_le_exp_mul_integral_norm_sq).
References #
- T. H. Gronwall, Note on the derivatives with respect to a parameter of the solutions of a system of differential equations, Ann. of Math. 20 (1919), 292–296.
- L. C. Evans, Partial Differential Equations, 2nd ed., Appendix B.2.
Grönwall's inequality, integral form. If φ is continuous on [a, b], 0 ≤ K and
φ t ≤ c + K ∫ₐᵗ φ for every t ∈ [a, b], then φ t ≤ c exp (K (t - a)) on [a, b].
Grönwall's inequality for monotone functions, almost-everywhere form. Let g be monotone
on [s, t] with g s ≥ 0. If k g ≤ g' at almost every point of (s, t), then
g s · exp (∫ₛᵗ k) ≤ g t. No continuity of g is needed. If k is not interval integrable, the
integral is the junk value 0 and the bound is just monotonicity.
The closed form of e^{λT} times the Grönwall bound with rate -λ:
e^{λT} gronwallBound δ (-λ) c T = δ + E_λ(T) c, where E_λ(T) = ∫₀ᵀ e^{λr} dr.
Exponential decay from a differential inequality. If g' ≤ -lam * g on [T, ∞), then
g t ≤ g T * exp (-(lam * (t - T))) for every t ≥ T.
Exponential decay from a differential inequality, eventual form. If g' ≤ -lam * g on
[T, ∞), then g t ≤ C * exp (-(lam * t)) for some C > 0 and all large t.
Two-sided uniqueness from a Grönwall bound. If f is differentiable within [a, b],
satisfies ‖f'‖ ≤ K ‖f‖ there and vanishes at one point of [a, b], then it vanishes on
[a, b]. Mathlib's eq_zero_of_abs_deriv_le_mul_abs_self_of_eq_zero_right is the case where
the point is a.
A square-integrable path with derivative controlled by its norm is bounded. If
‖u'‖ ≤ K ‖u‖ with K ≥ 0 and u is square integrable on the line, then
‖u s‖² ≤ exp (2 K) ∫ ‖u‖² for every s.