Inverting and differentiating continuous linear maps

This file collects two kinds of facts about inverting continuous linear maps. The first is a perturbation criterion: a map differing from a continuous linear equivalence L by less than ‖L⁻¹‖⁻¹ in operator norm is again invertible, by a Neumann series. The second packages the derivative of a differentiable inverse family of continuous linear maps at an invertible base point, including its action on a varying vector; that is the analytic input for differentiating a vector-field pullback along a parametric family.

Main results

• ContinuousLinearMap.isInvertible_of_norm_sub_lt and ContinuousLinearMap.isInvertible_of_norm_sub_le_half: a continuous linear map closer to an invertible one than the reciprocal norm of its inverse — or than half of it — is itself invertible.
• HasDerivAt.clm_inverse: differentiates (A t)⁻¹.
• HasDerivAt.clm_inverse_apply: differentiates (A t)⁻¹ (w t).
• DifferentiableAt.clm_inverse_of_completeSpace: the inverse of a differentiable family between Banach spaces is differentiable at an invertible base point.
• HasDerivAt.clm_inverse_of_completeSpace: the Banach-space specialization for an inverse family.
• HasDerivAt.clm_inverse_apply_of_completeSpace: the Banach-space specialization acting on a vector curve.

theorem ContinuousLinearMap.isInvertible_of_norm_sub_lt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (L : E ≃L[𝕜] F) {A : E →L[𝕜] F} (h : ‖A - ↑L‖₊ < ‖↑L.symm‖₊⁻¹) : A.IsInvertible

A continuous linear map that differs from a continuous linear equivalence L by less than ‖L⁻¹‖⁻¹ in operator norm is itself invertible: L⁻¹A is close enough to 1 to be a unit of the Banach algebra of endomorphisms of E.

theorem ContinuousLinearMap.isInvertible_of_norm_sub_le_half {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] (L : E ≃L[𝕜] F) {A : E →L[𝕜] F} (h : ‖A - ↑L‖₊ ≤ ‖↑L.symm‖₊⁻¹ / 2) : A.IsInvertible

A continuous linear map within ‖L⁻¹‖⁻¹ / 2 of a continuous linear equivalence L is invertible. This is the shape in which Mathlib's inverse function theorem supplies the estimate.

theorem HasDerivAt.clm_inverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t₀ : 𝕜} {A : 𝕜 → E →L[𝕜] F} {A' : E →L[𝕜] F} (hA : HasDerivAt A A' t₀) (hA0Inv : (A t₀).IsInvertible) (hInvDiff : DifferentiableAt 𝕜 (fun (t : 𝕜) => (A t).inverse) t₀) : HasDerivAt (fun (t : 𝕜) => (A t).inverse) (-(A t₀).inverse ∘SL A' ∘SL (A t₀).inverse) t₀

The derivative of an inverse family of continuous linear maps, assuming the family is invertible at the base point and the inverse family is differentiable there.

theorem HasDerivAt.clm_inverse_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t₀ : 𝕜} {A : 𝕜 → E →L[𝕜] F} {A' : E →L[𝕜] F} {w : 𝕜 → F} {w' : F} (hA : HasDerivAt A A' t₀) (hA0Inv : (A t₀).IsInvertible) (hInvDiff : DifferentiableAt 𝕜 (fun (t : 𝕜) => (A t).inverse) t₀) (hw : HasDerivAt w w' t₀) : HasDerivAt (fun (t : 𝕜) => (A t).inverse (w t)) ((A t₀).inverse w' - (A t₀).inverse (A' ((A t₀).inverse (w t₀)))) t₀

The derivative of an inverse family of continuous linear maps acting on a differentiable vector curve, assuming the family is invertible at the base point and the inverse family is differentiable there.

theorem DifferentiableAt.clm_inverse_of_completeSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t₀ : 𝕜} {A : 𝕜 → E →L[𝕜] F} [CompleteSpace E] (hA : DifferentiableAt 𝕜 A t₀) (hA0Inv : (A t₀).IsInvertible) : DifferentiableAt 𝕜 (fun (t : 𝕜) => (A t).inverse) t₀

In a Banach space, the inverse of a differentiable family is differentiable at an invertible base point.

theorem HasDerivAt.clm_inverse_of_completeSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t₀ : 𝕜} {A : 𝕜 → E →L[𝕜] F} {A' : E →L[𝕜] F} [CompleteSpace E] (hA : HasDerivAt A A' t₀) (hA0Inv : (A t₀).IsInvertible) : HasDerivAt (fun (t : 𝕜) => (A t).inverse) (-(A t₀).inverse ∘SL A' ∘SL (A t₀).inverse) t₀

The derivative of an inverse family of continuous linear maps between Banach spaces.

theorem HasDerivAt.clm_inverse_apply_of_completeSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {t₀ : 𝕜} {A : 𝕜 → E →L[𝕜] F} {A' : E →L[𝕜] F} {w : 𝕜 → F} {w' : F} [CompleteSpace E] (hA : HasDerivAt A A' t₀) (hA0Inv : (A t₀).IsInvertible) (hw : HasDerivAt w w' t₀) : HasDerivAt (fun (t : 𝕜) => (A t).inverse (w t)) ((A t₀).inverse w' - (A t₀).inverse (A' ((A t₀).inverse (w t₀)))) t₀

The derivative of an inverse family of continuous linear maps between Banach spaces, acting on a differentiable vector curve.