Zulip Chat Archive

Stream: maths

Topic: banach-steinhaus

Jireh Loreaux (Dec 03 2021 at 23:07):

I'm going to add the Banach-Steinhaus theorem (Principle of Uniform Boundedness), unless I missed it somewhere in mathlib. Is this the appropriate statement, or should I phrase it differently?

analysis.normed_space.operator_norm

open_locale ennreal

variables {E : Type*} {F : Type*} {π•œ : Type*}
variables [semi_normed_group E] [semi_normed_group F] [complete_space E]
variables [nondiscrete_normed_field π•œ] [semi_normed_space π•œ E] [semi_normed_space π•œ F]

theorem banach_steinhaus {ΞΉ : Type*} {g : ΞΉ β†’ E β†’L[π•œ] F}
( h : βˆ€ x : E, ⨆ i : ΞΉ, ↑βˆ₯g i xβˆ₯β‚Š < ∞) :
⨆ i : ΞΉ, ↑βˆ₯g iβˆ₯β‚Š < ∞ :=
sorry

Moritz (Dec 04 2021 at 00:50):

Banach-Steinhaus holds in way more generality: for maps from barrelled spaces to locally convex spaces, but both types of spaces are not yet in mathlib. defining locally convex and barrels is simple - I don't know how much more involved the proof for Banach-Steinhaus gets

Jireh Loreaux (Dec 04 2021 at 02:24):

Darn, I was hoping to use Sokal's elementary proof. I'll have a look for the more general version.

Scott Morrison (Dec 05 2021 at 19:16):

Given locally convex spaces and barrels aren't yet defined, it's completely okay, and probably a good idea, to prove and PR the special case first. It might be straightforward to add the definitions, but an API is quite a detour, and needn't prevent some statement of uniform boundedness getting in.

Jireh Loreaux (Dec 05 2021 at 23:53):

Okay, I'll probably get to that sometime this week. Sokal's proof is very elementary.

Jireh Loreaux (Dec 08 2021 at 23:40):

I've written up a proof the standard version of the Banach-Steinhaus theorem at #10663. There are no frills, in part because we don't have nowhere dense or meagre sets defined in mathlib. Is this correct, or should I somehow be using topology/G_delta in a way that I'm not seeing.

Jireh Loreaux (Dec 08 2021 at 23:42):

Along the way, I noticed that topology/metric_space/baire is valid with pseudo_emetric_space instead of just emetric_space (literally zero other changes). Should this be included in this PR (it is currently)?

Jireh Loreaux (Dec 12 2021 at 05:13):

@FrΓ©dΓ©ric Dupuis , @Heather Macbeth , @Rob Lewis : thanks for your refactor for semilinear maps! It is amazingly done. I was able to generalize my proof of Banach-Steinhaus to semilinear maps by changing only the statements (given some recently generalized theorems in analysis/normed_space/operator_norm). So simple and painless.

Anatole Dedecker (Jul 06 2023 at 11:53):

Just wanted to mention that the general version (and the required PRs) are now ready for review in mathlib4! #5676

Last updated: Dec 20 2023 at 11:08 UTC