Boundedness near an endpoint from a bounded derivative

A function on the reals whose derivative is bounded just to the right of a stays bounded as the variable tends to a from the right: the mean value inequality bounds it on a short interval (a, b) on which the derivative bound holds.

Main results

• TauCeti.exists_norm_le_of_norm_hasDerivWithin_le: if f' = g on a right neighbourhood of a and ‖g‖ is eventually bounded there, then ‖f t‖ is eventually bounded as t → a⁺.

theorem TauCeti.exists_norm_le_of_norm_hasDerivWithin_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {a C : ℝ} (hf : ∀ᶠ (u : ℝ) in nhdsWithin a (Set.Ioi a), HasDerivWithinAt f (g u) (Set.Ioi a) u) (hg : ∀ᶠ (u : ℝ) in nhdsWithin a (Set.Ioi a), ‖g u‖ ≤ C) : ∃ (B : ℝ), ∀ᶠ (t : ℝ) in nhdsWithin a (Set.Ioi a), ‖f t‖ ≤ B

Boundedness near a⁺ from a bounded derivative. If f : ℝ → E has derivative g u within (a, ∞) at every u in a right neighbourhood of a, and ‖g u‖ ≤ C there, then ‖f t‖ is eventually bounded as t tends to a from the right.