Bounded operators and operator topologies

General bounded operators: Douglas lemma, direct sums, strong and weak operator convergence, uniform boundedness, Hellinger–Toeplitz, invariant subspaces (Lomonosov), hypercyclicity criteria, Wold decomposition.

• Density of invertible operators
• Direct sums of operators
• Douglas factorization lemma
• Hypercyclic operators
• Robertson–Schrödinger uncertainty relation
• Uniform boundedness principle
• Wold decomposition

TheoremA symmetric linear map from a Banach space to its dual is bounded#●ready to prove

Let \(E\) be a real Banach space with dual space \(E^*\) of continuous linear functionals, and let \(T : E \to E^*\) be a linear map that is symmetric: \((Tx)(y) = (Ty)(x)\) for all \(x, y \in E\). Then \(T\) is bounded: there is a constant \(C \ge 0\) such that \(\|Tx\| \le C \|x\|\) for all \(x \in E\), where \(\|Tx\|\) is the operator norm of the functional \(Tx\).

public theorem_wanted exists_bound_of_symmetric_linearMap_to_strongDual
    {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (T : E →ₗ[ℝ] StrongDual ℝ E) (hsym : ∀ x y : E, (T x) y = (T y) x) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ x : E, ‖T x‖ ≤ C * ‖x‖

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Operator theory; General theory of linear operators), problem ma_proofbench_l1_22.

TheoremBartle–Graves theorem#✓fully proved

Let \(E\) and \(F\) be real Banach spaces and let \(T : E \to F\) be a surjective continuous linear map. Then there are a continuous map \(g : F \to E\), in general not linear, and a constant \(C \ge 0\) such that \(T(g(y)) = y\) for every \(y \in F\), \(g(0) = 0\), \(g(t y) = t \, g(y)\) for every real \(t \ge 0\) and every \(y \in F\), and \(\|g(y)\| \le C \|y\|\) for every \(y \in F\).

theorem bartle_graves
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
    (T : E →L[ℝ] F) (hT : Function.Surjective T) :
    ∃ (g : F → E) (C : ℝ), 0 ≤ C ∧ Continuous g ∧ (∀ y, T (g y) = y) ∧ g 0 = 0 ∧
      (∀ (t : ℝ) (y : F), 0 ≤ t → g (t • y) = t • g y) ∧
      (∀ y, ‖g y‖ ≤ C * ‖y‖)

Sources

• R. G. Bartle and L. M. Graves, Mappings between function spaces, Trans. Amer. Math. Soc. 72 (1952), 400–413, DOI 10.1090/S0002-9947-1952-0047910-X; Michael selection theorem precursor; Lean states real Banach case with continuous right inverse, positive homogeneity, and linear growth bound.

TheoremLomonosov's invariant subspace theorem#✓fully proved

Let \(E\) be an infinite-dimensional complex Banach space, let \(K\) be a nonzero compact operator on \(E\), and let \(T\) be a bounded linear operator on \(E\) with \(TK = KT\). Then there is a closed linear subspace \(M\) of \(E\) with \(M \ne \{0\}\) and \(M \ne E\) that is invariant under \(T\): \(T x \in M\) for every \(x \in M\).

theorem lomonosov_invariantSubspace
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
    (hInf : ¬ FiniteDimensional ℂ E)
    (K : E →L[ℂ] E) (hK_compact : IsCompactOperator K) (hK_ne : K ≠ 0)
    (T : E →L[ℂ] E) (hComm : T.comp K = K.comp T) :
    ∃ (M : Submodule ℂ E), M ≠ ⊥ ∧ M ≠ ⊤ ∧ IsClosed (M : Set E) ∧ ∀ x ∈ M, T x ∈ M

Sources

• V. Lomonosov, Functional Anal. Appl. 7 (1973) and J. Hilden elementary proof, Bull. Amer. Math. Soc.; Aronszajn-Smith 1954 precursor; Radjavi-Rosenthal invariant subspace book, 1973; Lean states complex Banach infinite-dimensional case K≠0 compact commuting with T yields nontrivial closed invariant subspace.

TheoremStrong operator convergence characterized by weak operator convergence#●ready to prove

Let \(H\) be a real or complex Hilbert space with inner product \(\langle \cdot, \cdot \rangle\), let \((T_n)_{n \in \mathbb{N}}\) be a sequence of bounded linear operators on \(H\), let \(T\) be a bounded linear operator on \(H\), and write \(S^*\) for the adjoint of an operator \(S\). Then \(T_n \to T\) in the strong operator topology, that is, \(T_n x \to T x\) for every \(x \in H\), if and only if both \(T_n \to T\) in the weak operator topology, that is, \(\langle y, T_n x \rangle \to \langle y, T x \rangle\) for all \(x, y \in H\), and \(T_n^* T_n \to T^* T\) in the weak operator topology, that is, \(\langle y, T_n^* T_n x \rangle \to \langle y, T^* T x \rangle\) for all \(x, y \in H\).

public theorem_wanted tendsto_apply_iff_tendsto_inner_and_tendsto_inner_adjoint_comp
    {𝕜 H : Type*}
    [RCLike 𝕜]
    [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [CompleteSpace H]
    (Tn : ℕ → H →L[𝕜] H)
    (T : H →L[𝕜] H) :
    (∀ x : H, Filter.Tendsto (fun n => Tn n x) Filter.atTop (𝓝 (T x))) ↔
      (∀ x y : H, Filter.Tendsto (fun n => inner 𝕜 y (Tn n x)) Filter.atTop (𝓝 (inner 𝕜 y (T x)))) ∧
        (∀ x y : H, Filter.Tendsto (fun n => inner 𝕜 y (((Tn n).adjoint.comp (Tn n)) x))
            Filter.atTop (𝓝 (inner 𝕜 y ((T.adjoint.comp T) x))))

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Operator theory; General theory of linear operators), problem ma_proofbench_l2_59.

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.