Scalar Gronwall estimates with interior derivatives

These estimates require continuity on a closed interval and derivatives only in its interior. The time origin and initial value are arbitrary. The unperturbed estimates allow any real growth coefficient; the perturbed estimates bound a nonnegative constant forcing error. No positivity assumption on the function itself is needed except to deduce that it vanishes.

The separation of the scalar argument follows Code4me2's NavierStokes/GronwallInterior.lean refactor. The estimates here retain arbitrary initial times and values.

theorem Gronwall.antitoneOn_exp_neg_mul_of_deriv_le {a b K : ℝ} {f f' : ℝ → ℝ} (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hbound : ∀ t ∈ Set.Ioo a b, f' t ≤ K * f t) : AntitoneOn (fun (t : ℝ) => Real.exp (-K * t) * f t) (Set.Icc a b)

The integrating factor turns f' ≤ K * f into a nonincreasing function. There is no sign restriction on K or f.

theorem Gronwall.le_exp_mul_of_deriv_le {a b K : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hbound : ∀ t ∈ Set.Ioo a b, f' t ≤ K * f t) (t : ℝ) : t ∈ Set.Icc a b → f t ≤ f a * Real.exp (K * (t - a))

A scalar differential inequality with only interior derivatives gives the usual exponential bound from the initial value, even when K or f a is negative.

theorem Gronwall.eq_zero_of_deriv_le {a b K : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hcont : ContinuousOn f (Set.Icc a b)) (hinitial : f a = 0) (hnonneg : ∀ t ∈ Set.Icc a b, 0 ≤ f t) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hbound : ∀ t ∈ Set.Ioo a b, f' t ≤ K * f t) (t : ℝ) : t ∈ Set.Icc a b → f t = 0

A nonnegative function that initially vanishes and satisfies f' ≤ K * f in the interior vanishes on the entire closed interval.

theorem Gronwall.exp_neg_mul_le_add_of_deriv_le_add {a b K ε : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hK : 0 ≤ K) (hε : 0 ≤ ε) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hbound : ∀ t ∈ Set.Ioo a b, f' t ≤ K * f t + ε) (t : ℝ) : t ∈ Set.Icc a b → Real.exp (-K * (t - a)) * f t ≤ f a + ε * (t - a)

With nonnegative growth and forcing bounds, the weighted value increases by at most ε * (t - a). The initial value and the function may have either sign.

theorem Gronwall.le_exp_mul_add_of_deriv_le_add {a b K ε : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hK : 0 ≤ K) (hε : 0 ≤ ε) (hcont : ContinuousOn f (Set.Icc a b)) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hbound : ∀ t ∈ Set.Ioo a b, f' t ≤ K * f t + ε) (t : ℝ) : t ∈ Set.Icc a b → f t ≤ (f a + ε * (t - a)) * Real.exp (K * (t - a))

An interior differential inequality f' ≤ K * f + ε yields an exponential bound with arbitrary initial time and initial value.

theorem Gronwall.le_uniform_exp_mul_of_deriv_le_add {a b K ε : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b) (hK : 0 ≤ K) (hε : 0 ≤ ε) (hcont : ContinuousOn f (Set.Icc a b)) (hinitial : f a ≤ 0) (hderiv : ∀ t ∈ Set.Ioo a b, HasDerivAt f (f' t) t) (hbound : ∀ t ∈ Set.Ioo a b, f' t ≤ K * f t + ε) (t : ℝ) : t ∈ Set.Icc a b → f t ≤ ε * (b - a) * Real.exp (K * (b - a))

A nonpositive initial value gives a bound valid uniformly on the closed interval. Only K and ε must be nonnegative; the function need not be.