Boundedness near an endpoint from a continuous derivative

A function on the reals whose right derivative just to the right of a is given by a function right-continuous at a stays bounded as the variable tends to a from the right. The derivative is bounded on a short interval (a, a + ε), so the mean value inequality bounds the function there.

Main results

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

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

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