banach_steinhaus
theorem banach_steinhaus :
∀ {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {𝕜₂ : Type u_4} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
{ι : Type u_5} [inst_7 : CompleteSpace E] {g : ι → E →SL[σ₁₂] F},
(∀ (x : E), ∃ C, ∀ (i : ι), ‖(g i) x‖ ≤ C) → ∃ C', ∀ (i : ι), ‖g i‖ ≤ C'
This theorem is the standard Banach-Steinhaus theorem, also known as the Uniform Boundedness Principle. It states that if we have a family of continuous linear maps (denoted by `g`) from a Banach space `E` into a normed space `F`, and if this family of maps is pointwise bounded (i.e., for every point `x` in `E`, there exists a constant `C` such that for every map `i` in the family, the norm of `i(x)` is less than or equal to `C`), then there exists a uniform bound `C'` such that for every map `i` in the family, the norm of `i` is less than or equal to `C'`. This theorem generalizes to barrelled spaces as well, as indicated by `WithSeminorms.banach_steinhaus`.
More concisely: If a family of continuous linear maps from a Banach space into a normed space is pointwise bounded, then it is uniformly bounded.
|
banach_steinhaus_iSup_nnnorm
theorem banach_steinhaus_iSup_nnnorm :
∀ {E : Type u_1} {F : Type u_2} {𝕜 : Type u_3} {𝕜₂ : Type u_4} [inst : SeminormedAddCommGroup E]
[inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
[inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
{ι : Type u_5} [inst_7 : CompleteSpace E] {g : ι → E →SL[σ₁₂] F},
(∀ (x : E), ⨆ i, ↑‖(g i) x‖₊ < ⊤) → ⨆ i, ↑‖g i‖₊ < ⊤
This theorem, a variant of the Banach-Steinhaus theorem, states that for any types E, F, 𝕜, 𝕜₂, and ι, given that E and F are both semi-normed commutative additive groups, 𝕜 and 𝕜₂ are non-trivially normed fields, E is a normed space over 𝕜, F is a normed space over 𝕜₂, σ₁₂ is a isometric ring homomorphism from 𝕜 to 𝕜₂, E is a complete space, and g is a function from ι to the space of continuous linear maps from E to F, if for every element x of E, the supremum of the non-negative norms of g(i) x (for all i in ι) is less than infinity, then the supremum of the non-negative norms of g(i) (for all i in ι) is also less than infinity. This theorem is a fundamental result in functional analysis and is primarily utilized in the study of bounded operators in Banach spaces.
More concisely: If E and F are normed spaces, 𝕜 and 𝕜₂ are non-trivially normed fields, σ₁₂ is an isometric ring homomorphism from 𝕜 to 𝕜₂, E is complete, and g is a function from a set ι to the space of continuous linear maps from E to F, such that for all x in E and all i in ι, the supremum of the non-negative norms of g(i) x is finite; then the supremum of the non-negative norms of g(i) is also finite.
|