One-sided derivatives from one-sided derivative limits

A function continuous at t₀, differentiable on a one-sided punctured neighbourhood, whose derivative tends to L from that side, has one-sided derivative L at t₀. Mathlib's hasDerivWithinAt_Ici_of_tendsto_deriv states this over a set containing a right neighbourhood; these wrappers put it in the 𝓝[>] t₀ / 𝓝[<] t₀ eventual form in which piecewise-C¹ curve data arrives.

Main results

• TauCeti.hasDerivWithinAt_Ioi_of_tendsto_deriv — the right-sided derivative from a right derivative limit.
• TauCeti.hasDerivWithinAt_Iio_of_tendsto_deriv — the left counterpart.

Provenance

Migrated from hasDerivWithinAt_Ioi_of_tendsto and hasDerivWithinAt_Iio_of_tendsto of FlatnessConditions.lean in the AINTLIB LeanModularForms development. Prerequisite for the crossing analysis of the generalized residue theorem on the roadmap, where the one-sided tangents of a piecewise-C¹ curve are recovered from derivative limits.

theorem TauCeti.hasDerivWithinAt_Ioi_of_tendsto_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {t₀ : ℝ} {L : E} (hγ_cont : ContinuousAt γ t₀) (hγ_diff : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Ioi t₀), DifferentiableAt ℝ γ t) (hL : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L)) : HasDerivWithinAt γ L (Set.Ioi t₀) t₀

A function continuous at t₀, eventually differentiable on the right, whose derivative tends to L from the right, has right derivative L at t₀.

theorem TauCeti.hasDerivWithinAt_Iio_of_tendsto_deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {γ : ℝ → E} {t₀ : ℝ} {L : E} (hγ_cont : ContinuousAt γ t₀) (hγ_diff : ∀ᶠ (t : ℝ) in nhdsWithin t₀ (Set.Iio t₀), DifferentiableAt ℝ γ t) (hL : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L)) : HasDerivWithinAt γ L (Set.Iio t₀) t₀

A function continuous at t₀, eventually differentiable on the left, whose derivative tends to L from the left, has left derivative L at t₀.