balanced hull / seminorm split

Stream: maths

[Moritz Doll]

I have wip PR ( #12537 ) that would add ~200 lines to the balanced set part in analysis.seminorm. If I remember correctly there was a consensus to that this file is already large enough and might be ripe for splitting up. I don't remember whether that was before the gauge part left or after. So my question is whether we should split seminormfurther or just put the balanced hull/core stuff in a new file @Yaël Dillies @Heather Macbeth @Bhavik Mehta

[Yaël Dillies]

Yes, I am planning on splitting this up further.

[Yaël Dillies]

What should we name it? I was happy with analysis.convex.balanced

[Moritz Doll]

I know that I am not happy with putting everything in analysis.convex :laughing: In the case of balanced sets we don't even need an order on the underlying field/ring, so there is not even a notion of convexity. My suggestion is still analysis.locally_convex not because everything is locally convex, but all the topics are related and used for locally convex spaces. There is also the possibility to make a folder (something like) analysis.module for topics about modules over normed fields/rings. The later is probably more in line with the rest of the naming convention of mathlib.

[Moritz Doll]

another possibility would be analysis.normed.module, but thatt sounds like having a norm on the module

[Moritz Doll]

another option (which would lead to less bike-shedding) is to put everything in analysis until that folder becomes too large and then we can decide what to group together

[Moritz Doll]

/poll <Where to put the definition of balanced sets?>
Leave everything as is
analysis.balanced
analysis.convex.balanced
analysis.locally_convex.balanced
analysis.module.balanced

[Yaël Dillies]

And do we keep absorbent/absorbs with it?

[Yaël Dillies]

I'll soon add bornivores

[Moritz Doll]

good point, maybe I should add options for putting it into a basic-file

[Moritz Doll]

(that does not make any sense for analysis.convex right?)

[Yaël Dillies]

It could, but that would mean we should split up anaylsis.convex.basic further (which is going to happeny because we want to turn the dependency of convex and star_convex around).

[Moritz Doll]

Nobody else seems to care and we both like analysis.locally_convex.basic, we should use that. @Yaël Dillies do you want to do the split, or should I do it? I have a few future PRs that add stuff to the seminorm file, so I am waiting with those until the file is divided.

[Yaël Dillies]

I love splitting stuff :grinning: