Factoring an operator through the range of a dominating operator

Let g : E →L[𝕜] G and f : E →L[𝕜] F be bounded operators with ‖f x‖ ≤ C ‖g x‖ for every x. Then f vanishes on the kernel of g, so it factors as f = S ∘ g through the range of g, with a factor S of norm at most C. When F is complete, S extends by continuity to the closure of that range, with the same bound. Conversely, any such factorization gives the bound.

The factor on the range is Mathlib's LinearMap.compLeftInverse and its extension to the closure is LinearMap.extendOfNorm. This file records the pointwise and operator-norm bounds for the former and the two factorization criteria.

Main results

• LinearMap.norm_compLeftInverse_apply_le: the pointwise bound C for f.compLeftInverse g.
• LinearMap.opNorm_compLeftInverse_le: the norm of f.compLeftInverse g is at most C.
• ContinuousLinearMap.exists_eq_comp_rangeRestrict_iff: f factors through the range of g with a factor of norm at most C iff ‖f x‖ ≤ C ‖g x‖ for all x.
• ContinuousLinearMap.exists_eq_comp_codRestrict_topologicalClosure_iff: the same criterion for factorizations through the closure of the range, when the target is complete.

theorem LinearMap.norm_compLeftInverse_apply_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E] [Module 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] {f : E →ₛₗ[σ₁₂] F} {g : E →ₗ[𝕜] G} {C : ℝ} (h : ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖) (y : ↥g.range) : ‖(f.compLeftInverse g) y‖ ≤ C * ‖↑y‖

If ‖f x‖ ≤ C ‖g x‖ for all x, the factor f.compLeftInverse g of f through the range of g satisfies ‖f.compLeftInverse g y‖ ≤ C ‖y‖ on that range.

theorem LinearMap.opNorm_compLeftInverse_le {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [AddCommGroup E] [Module 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] {f : E →ₛₗ[σ₁₂] F} {g : E →ₗ[𝕜] G} {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖) : ‖f.compLeftInverse g‖ ≤ C

If ‖f x‖ ≤ C ‖g x‖ for all x, the factor f.compLeftInverse g of f through the range of g has operator norm at most C.

theorem ContinuousLinearMap.denseRange_codRestrict_topologicalClosure {𝕜 : Type u_1} {E : Type u_3} {G : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (g : E →L[𝕜] G) : DenseRange ⇑(g.codRestrict (↑g).range.topologicalClosure ⋯)

The corestriction of an operator to the closure of its range has dense range.

theorem ContinuousLinearMap.exists_eq_comp_rangeRestrict_iff {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F} {g : E →L[𝕜] G} {C : ℝ} (hC : 0 ≤ C) : (∃ (S : ↥(↑g).range →SL[σ₁₂] F), ‖S‖ ≤ C ∧ f = S ∘SL g.rangeRestrict) ↔ ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖

An operator f factors as S ∘ g through the range of g, with ‖S‖ ≤ C, if and only if ‖f x‖ ≤ C ‖g x‖ for all x.

theorem ContinuousLinearMap.exists_eq_comp_codRestrict_topologicalClosure_iff {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [RingHomIsometric σ₁₂] [CompleteSpace F] {f : E →SL[σ₁₂] F} {g : E →L[𝕜] G} {C : ℝ} (hC : 0 ≤ C) : (∃ (S : ↥(↑g).range.topologicalClosure →SL[σ₁₂] F), ‖S‖ ≤ C ∧ f = S ∘SL g.codRestrict (↑g).range.topologicalClosure ⋯) ↔ ∀ (x : E), ‖f x‖ ≤ C * ‖g x‖

When F is complete, an operator f factors as S ∘ g through the closure of the range of g, with ‖S‖ ≤ C, if and only if ‖f x‖ ≤ C ‖g x‖ for all x.