Seminorm balls

Stream: maths

[Moritz Doll]

Revisiting with_seminorms I have the feeling that the correct thing is to use add_group_seminorm for defining the add_group_filter_basis. For this to work however, we need seminorm.ball for add_group_seminorm and the most natural thing would be to define ball over add_group_seminorm_class. Any thoughts on this @Yaël Dillies @Anatole Dedecker ?

[Yaël Dillies]

Yep, that sounds exactly right.

[Yaël Dillies]

I think we'll lose dot notation unfortunately

[Anatole Dedecker]

That sounds right indeed, although losing dot notation could be annoying because of name clashes with docs#metric.ball. I just wanted to add that when using with_seminorms, it sometimes feel that we could gain something by splitting the "family of seminorms --> topology" step into "one (add group) seminorm --> topology" (which means porting some things about docs#normed_group to docs#group_seminorm) and then define the topology associated to a family of seminorms in terms of the topology associated to each (essentially making docs#seminorm_family.with_seminorms_iff_topological_space_eq_infi true by definition). Of course there would still be some work needed to get the right neighborhood basis, but I feel like this could potentially simplify the construction as a whole

[Moritz Doll]

yes, this is was exactly my reason to propose this. For the Schwartz space it was very awkward to choose the scalar multiplication for some theorems where the content of the theorem had nothing to do with the scalar multiplication.

[Anatole Dedecker]

More generally, when working with with_seminorms spaces, I'm constantly hesitating between "prove things directly about with_seminorms and then deduce the version for normed spaces using docs#norm_with_seminorms" or "prove things for seminormed_group first and then reduce the with_seminorms case to it". I find that I like the latter more and more, but I figured we should agree on a general rule because it defines how to orient the import tree.

[Anatole Dedecker]

Moritz Doll said:

yes, this is was exactly my reason to propose this. For the Schwartz space it was very awkward to choose the scalar multiplication for some theorems where the content of the theorem had nothing to do with the scalar multiplication.

Maybe I should clarify that my message was not that much about the "topological group / topological vector space" split, although it is definitely a good thing to split that in two steps too. It was more about the "one seminorm / a family of seminorms" split

[Moritz Doll]

ah ok, sorry, misread it - it is late and I am tired..

[Anatole Dedecker]

Don't worry, I wasn't particularly clear x)

[Moritz Doll]

so if I remember correctly, this is what I tried initially, but I could make it work (entirely due to my incompetence). I agree that my be the more elegant approach, but at the moment I don't see the practical improvement over what we have. So I will definitively not do that, but if you want to, feel free to do that.

[Anatole Dedecker]

It doesn't bring too much in practice indeed, I just wanted that to be written somewhere.

[Moritz Doll]

make it a issue in the github issue tracker and label it 'good first project' :rolling_on_the_floor_laughing: