Composition of bounded nonlinear right inverses #
Right inverses of two continuous linear maps compose in the reverse order of the original
maps. Their norm-bound constants multiply. No linearity, continuity, or completeness assumption
on the right inverses is needed beyond the native NonlinearRightInverse data.
def
ContinuousLinearMap.NonlinearRightInverse.comp
{𝕜 : 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]
{T : E →L[𝕜] F}
{S : F →L[𝕜] G}
(R : T.NonlinearRightInverse)
(Q : S.NonlinearRightInverse)
:
(S ∘SL T).NonlinearRightInverse
Compose bounded nonlinear right inverses. The inverse functions compose in the reverse order of the original continuous linear maps.
Instances For
@[simp]
theorem
ContinuousLinearMap.NonlinearRightInverse.comp_apply
{𝕜 : 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]
{T : E →L[𝕜] F}
{S : F →L[𝕜] G}
(R : T.NonlinearRightInverse)
(Q : S.NonlinearRightInverse)
(z : G)
:
The actual composed inverse is composition of the two inverse functions.
@[simp]
theorem
ContinuousLinearMap.NonlinearRightInverse.comp_nnnorm
{𝕜 : 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]
{T : E →L[𝕜] F}
{S : F →L[𝕜] G}
(R : T.NonlinearRightInverse)
(Q : S.NonlinearRightInverse)
:
The public norm-bound constant of the composition is the product of the constants.