Uniform boundedness principle

TheoremPointwise convergent operators converge along convergent sequences#●ready to prove

Let \(E\) and \(F\) be real Banach spaces, let \((T_n)\) be a sequence of bounded linear operators from \(E\) to \(F\), and suppose that for every \(x \in E\) the sequence \((T_n x)\) converges to a limit \(T x\). Then for every sequence \(x_n \to x\) in \(E\) we have \(T_n x_n \to T x\) in \(F\).

public theorem_wanted tendsto_apply_of_tendsto_pointwise_of_tendsto {E F : Type*}
    [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
    (Tn : ℕ → E →L[ℝ] F) (T : E → F)
    (hT : ∀ x : E, Tendsto (fun n => Tn n x) atTop (𝓝 (T x))) :
    ∀ (xseq : ℕ → E) (x : E), Tendsto xseq atTop (𝓝 x) →
      Tendsto (fun n => Tn n (xseq n)) atTop (𝓝 (T x))

Sources

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

TheoremWeakly bounded sets of operators are bounded#●ready to prove

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\), let \(H\) and \(K\) be Hilbert spaces over \(\mathbb{K}\), and let \(Q\) be a set of bounded linear operators from \(H\) to \(K\). Suppose \(Q\) is weakly bounded: for every \(f \in H\) and \(g \in K\) there is a real number \(\alpha\) such that \(|\langle A f, g \rangle| \le \alpha\) for all \(A \in Q\). Then \(Q\) is bounded in operator norm: there is a real number \(M\) such that \(\|A\| \le M\) for all \(A \in Q\).

public theorem_wanted exists_bound_opNorm_of_forall_inner_bounded (𝕜 : Type*) [RCLike 𝕜]
    (H K : Type*) [NormedAddCommGroup H] [NormedAddCommGroup K]
    [InnerProductSpace 𝕜 H] [InnerProductSpace 𝕜 K]
    [CompleteSpace H] [CompleteSpace K]
    (Q : Set (H →L[𝕜] K))
    (hQ : ∀ f : H, ∀ g : K, ∃ α : ℝ, ∀ A : H →L[𝕜] K, A ∈ Q → ‖inner 𝕜 (A f) g‖ ≤ α) :
    ∃ M : ℝ, ∀ A : H →L[𝕜] K, A ∈ Q → ‖A‖ ≤ M

Sources

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

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.