Norm comparisons passing to derivatives

If two continuous linear images of the increments of a map near x satisfy a norm comparison ‖L (φ y - φ x)‖ ≤ A * ‖M (φ y - φ x)‖, then so do the corresponding images of its derivative at x. For instance, tangent vectors to a set whose points have heights bounded by A times the distances of their base points obey the same bound.

LipschitzWith.norm_fderiv_comp_le applies this comparison to postcomposition by a Lipschitz map, without assuming differentiability of the outer map.

theorem HasFDerivAt.norm_apply_le_mul_norm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {φ : E → F} {φ' : E →L[𝕜] F} {x : E} (hφ : HasFDerivAt φ φ' x) {L : F →L[𝕜] G} {M : F →L[𝕜] H} {A : ℝ} (h : ∀ᶠ (y : E) in nhds x, ‖L (φ y - φ x)‖ ≤ A * ‖M (φ y - φ x)‖) (k : E) : ‖L (φ' k)‖ ≤ A * ‖M (φ' k)‖

A norm comparison ‖L (φ y - φ x)‖ ≤ A * ‖M (φ y - φ x)‖ between two continuous linear images of the increments of φ near x passes to its derivative φ' at x.

theorem LipschitzWith.norm_fderiv_comp_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {g : F → G} {C : NNReal} (hg : LipschitzWith C g) {x : E} (hf : DifferentiableAt 𝕜 f x) : ‖fderiv 𝕜 (g ∘ f) x‖ ≤ ↑C * ‖fderiv 𝕜 f x‖

Postcomposition by a C-Lipschitz map multiplies the norm of the derivative by at most C. The outer map need not be differentiable, even at the value of the inner map.