Closed range theorem
TheoremThe range of a bounded operator as a set#✓fully proved
Let \(E'\) and \(F'\) be Hilbert spaces over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(S : E' \to F'\) be a bounded linear operator. The set of values of \(S\) equals the underlying set of the range of \(S\) regarded as a linear subspace of \(F'\).
This lets closedness of the range pass between the anti-Lipschitz criterion, stated for the set of values, and the adjoint orthogonality identities, stated for the linear subspace.
theorem setRange_eq_coe_linearMap_range {E' F' : Type*} [NormedAddCommGroup E']
[InnerProductSpace 𝕜 E'] [CompleteSpace E'] [NormedAddCommGroup F']
[InnerProductSpace 𝕜 F'] [CompleteSpace F'] (S : E' →L[𝕜] F') :
Set.range S = (LinearMap.range S.toLinearMap : Set F')Used by 1
TheoremRestriction to the orthogonal complement of the kernel keeps the range#✓fully proved
Let \(E\) be a Hilbert space and \(F\) an inner product space over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(T : E \to F\) be a bounded linear operator. Then the restriction of \(T\) to the orthogonal complement \((\ker T)^\perp\) of its kernel has the same range as \(T\): every value \(T x\) is attained at the orthogonal projection of \(x\) onto \((\ker T)^\perp\), since the difference lies in \(\ker T\).
theorem range_comp_subtypeL_orthogonalComplement_ker (S : E →L[𝕜] F) :
Set.range (S.comp (Submodule.subtypeL (LinearMap.ker S.toLinearMap)ᗮ)) =
Set.range SUsed by 1
TheoremRestriction to the orthogonal complement of the kernel is injective#✓fully proved
Let \(E\) and \(F\) be inner product spaces over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(T : E \to F\) be a bounded linear operator. Then the restriction of \(T\) to the orthogonal complement \((\ker T)^\perp\) of its kernel is injective: a vector lying in both \(\ker T\) and \((\ker T)^\perp\) is zero.
theorem injective_comp_subtypeL_orthogonalComplement_ker (S : E →L[𝕜] F) :
Function.Injective (S.comp (Submodule.subtypeL (LinearMap.ker S.toLinearMap)ᗮ))Used by 1
TheoremClosed range passes to the adjoint#✓fully proved
Let \(E\) and \(F\) be Hilbert spaces over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(T : E \to F\) be a bounded linear operator with adjoint \(T^\dagger\). If the range of \(T\) is closed in \(F\), then the range of \(T^\dagger\) is closed in \(E\).
Proof sketch: if the range of \(T\) is closed, then \(T\) is bounded below on \((\ker T)^\perp\) (the anti-Lipschitz criterion for its injective restriction), say \(\|x\| \le C \|T x\|\) there. Every \(y \in (\ker T^\dagger)^\perp\) lies in the range of \(T\), because \((\operatorname{ran} T)^\perp = \ker T^\dagger\) and the range is closed. Writing \(y = T x\) with \(x \in (\ker T)^\perp\) gives \(\|y\|^2 = \operatorname{Re} \langle x, T^\dagger y \rangle \le \|x\| \|T^\dagger y\| \le C \|y\| \|T^\dagger y\|\); cancelling \(\|y\|\) shows that \(T^\dagger\) is bounded below on \((\ker T^\dagger)^\perp\), so its range, which is the range of its restriction to \((\ker T^\dagger)^\perp\), is closed.
theorem isClosed_range_adjoint_of_isClosed_range (T : E →L[𝕜] F)
(hT : IsClosed (LinearMap.range T.toLinearMap : Set F)) :
IsClosed (LinearMap.range (adjoint T).toLinearMap : Set E)TheoremClosed range theorem for adjoints#✓fully proved
Let \(E\) and \(F\) be Hilbert spaces over \(\mathbb{K}\), where \(\mathbb{K}\) is \(\mathbb{R}\) or \(\mathbb{C}\), and let \(T : E \to F\) be a bounded linear operator with adjoint \(T^\dagger\). Then the range of \(T\) is closed in \(F\) if and only if the range of \(T^\dagger\) is closed in \(E\).
The reverse direction is the forward direction applied to \(T^\dagger\), using \(T^{\dagger\dagger} = T\).
theorem isClosed_range_adjoint_iff (T : E →L[𝕜] F) :
IsClosed (LinearMap.range T.toLinearMap : Set F) ↔
IsClosed (LinearMap.range (adjoint T).toLinearMap : Set E)Uses 1
TheoremClosed range from a Fredholm \(T^*T\)#●ready to prove
Closed range from a Fredholm \(T^*T\). Let \(X\) and \(Y\) be complex Hilbert spaces and let \(T : X \to Y\) be a bounded linear operator with Hilbert space adjoint \(T^* : Y \to X\). If \(T^*T : X \to X\) is a Fredholm operator, then the range of \(T\) is closed in \(Y\).
Here a Fredholm operator is a bounded linear operator that is open onto its range, whose range is closed and of finite codimension, and whose kernel is finite-dimensional and has a closed complement. The source asks only for a finite-dimensional kernel and a range of finite codimension; between Hilbert spaces the two agree, since a finite-codimensional range of a bounded operator is closed.
public theorem_wanted isClosed_range_of_isFredholm_adjoint_comp {X Y : Type*}
[NormedAddCommGroup X] [InnerProductSpace ℂ X] [CompleteSpace X]
[NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
(T : X →L[ℂ] Y)
(hFredholm : (ContinuousLinearMap.adjoint T ∘L T).IsFredholm) :
IsClosed (LinearMap.range T.toLinearMap : Set Y)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; General theory of linear operators), problem
ma_proofbench_l2_23, with the change above.
TheoremClosed range passes to the Hilbert space adjoint#●ready to prove
Let \(X\) and \(Y\) be complex Hilbert spaces and let \(A : X \to Y\) be a bounded linear operator with Hilbert space adjoint \(A^* : Y \to X\). If the range of \(A\) is closed in \(Y\), then the range of \(A^*\) is closed in \(X\).
public theorem_wanted isClosed_range_adjoint_of_isClosed_range {X Y : Type*}
[NormedAddCommGroup X] [InnerProductSpace ℂ X] [CompleteSpace X]
[NormedAddCommGroup Y] [InnerProductSpace ℂ Y] [CompleteSpace Y]
(A : X →L[ℂ] Y)
(hRan : IsClosed (LinearMap.range A.toLinearMap : Set Y)) :
IsClosed (LinearMap.range A.adjoint.toLinearMap : Set X)Sources
- MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; General theory of linear operators), problem
ma_proofbench_l2_85.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.