Moving polar and UniformConvex

Stream: mathlib4

[Filippo A. E. Nuccio]

I see that WeakDual.polar is defined in Analysis.Normed but it really only needs that the module (called E ibid.) is a TVS. What about moving it to Mathlib.Analysis.LocallyConvex.WeakDual?

[Filippo A. E. Nuccio]

Also, I think that docs#UniformConvexSpace is misplaced: shouldn't it be either in Mathlib.Analysis.Normed.Module or in Mathlib.Analysis.NormedSpace (btw, I'd be happy to understand the difference between these two folders)?

[Yaël Dillies]

I think there's no difference between the two folders, no :sad:

[Yaël Dillies]

I am not sure why UniformConvexSpace is misplaced

[Filippo A. E. Nuccio]

@Yaël Dillies do you mean

1. Why is it misplaced?
2. Why do I think it is misplaced?

Do we feel like embarking in the long-term (and not terribly exciting...) project of merging the two folders?

[Yaël Dillies]

I feel like merging .NormedSpace and .Normed.Module is a one-PR job! Sorting out .Convex however is a job I've embarked on several years ago...

[Yaël Dillies]

I guess I am asking both 1 and 2 :slight_smile:

[Filippo A. E. Nuccio]

Concerning the merge, you're probably right: let me ping @Anatole Dedecker @Jireh Loreaux @Yury G. Kudryashov @Heather Macbeth, @Christopher Hoskin and @Moritz Doll who worked on these folders to check if there are objections: if not, I'll try the PR (a :thumbs_up: is enough if you agree).

[Filippo A. E. Nuccio]

Concerning the .Convex, I do not have a strong opinion about the whole folder, and in particular about what should be in LocallyConvex and what in Convex. But for this precise notion, I'd argue that most results in .Convex have to do with convex functions, while UniformConvexSpace is a notion about spaces (that only makes sense for (semi?)normed ones, btw), which I see as a sound argument for moving it to the corresponding folder.

[Yaël Dillies]

My eventual goal is for Geometry.Convex to be about pure convexity with no mention of norm, and Analysis.Convex to be about the interaction of convexity and norm. In this sense, I am quite happy with where UniformConvexSpace is at the moment

[Filippo A. E. Nuccio]

OK, seen under this perspective I understand the point. On the other hand, given the current design of (this part of) the library, it is hard to imagine where it would be, don't you find?

[Filippo A. E. Nuccio]

And if one day you'll be able to find (someone else having) enough time to do the refactor, the fact that this notion sits coherently in the NormedSpace (or Normed.Module?) folder won't make your life harder. Am I optimistic?

[Jireh Loreaux]

Before merging those folders we need to check that things in NormedSpace shouldn't go into other Normed.* folders. That NormedSpace folder used to be a catch-all for all normed things.

[Filippo A. E. Nuccio]

Like Normed.Algebra, for instance?

[Filippo A. E. Nuccio]

OK, so it seems like a finer task. Of course, it can be done step by step by cherry-picking results and moving them to the right Normed.* folder....

[Filippo A. E. Nuccio]

And any opinion on UniformConvexSpace?

[Jireh Loreaux]

sorry, will have to check later today, must teach soon.

[Jireh Loreaux]

I think I'm fine with UniformConvexSpace living where it is. If Analysis.Convex is really only about normed stuff, then perhaps at some point it should be moved to Analysis.Normed.Convex, which would fix the issue you have with it I think Filippo.

[Jireh Loreaux]

I've created a tracking issue #28698 for this project. We can decide there what to do with each file, and then we can take action and link PRs to the tracking issue.

[Jireh Loreaux]

I filled out just a few with my suggestions.

[Yaël Dillies]

The argument I could hear, and which I am willing to entertain, is that UniformConvexSpace is not convex analysis, but simply a predicate from Banach space theory with "convex" in the name

[Jireh Loreaux]

Should we move NormedSpace/OperatorNorm/ in its entirety to a new folder Normed/Operator/ or should we distribute its contents according to the kind of things involved? E.g., OperatorNorm/Mul.lean could go in a new file Normed.Algebra.Operator.lean.

[Filippo A. E. Nuccio]

Yes, I think that Yaël's way of putting it is straight to the point. Indeed, having it in Analysis.Normed.Convex would be better, but I would expect things there to relate to convex analysis in normed spaces, rather than normed spaces that satisfy some strong convexity property.

[Filippo A. E. Nuccio]

Jireh Loreaux said:

lean

I would in principle have everything is Normed/Operator but let me have a look at ./Mul.lean to get a more precise feeling. EDIT No, Normed.Algebra.Operator (or Normed.Algebra.MulOperator?) seems a better place.

[Filippo A. E. Nuccio]

OK, so what's the take on this? I will contribute to @Jireh Loreaux 's issue but concerning UniformConvexSpace do we leave it where it is or can/should I move somewhere in .Metric?

[Jireh Loreaux]

I've updated the tracking issue with everywhere I think things should go. Please comment / make changes. I would like to start making this happen in the near future.

[Jireh Loreaux]

@Filippo A. E. Nuccio I could see moving it to Normed/Module/UniformConvex.lean.

[Filippo A. E. Nuccio]

I agree! I am happy to open the PR concerning the UniformConvex (in particular because I have two small additions to it), how do you want to proceed for the others, @Jireh Loreaux ?

[Jireh Loreaux]

After there is some small amount of agreement about where the other files should go, we can move the other files in chunks.

[Filippo A. E. Nuccio]

And forgive my ignorance, but how do I comment your suggestions (eg: why do we prefer a folder "Alternating" rather than "Multilinear", and to have the latter inside the former?)

[Anatole Dedecker]

Yaël Dillies said:

The argument I could hear, and which I am willing to entertain, is that UniformConvexSpace is not convex analysis, but simply a predicate from Banach space theory with "convex" in the name

I haven't followed the whole discussion, but I definitely agree with this. If I had to classify uniform convexity of spaces I would put it under "Geometry of Banach spaces"

[Filippo A. E. Nuccio]

Why of Banach ones? I agree that Milman-Pettis (which I have almost done in #28693) applies to those, but the definition itself does not require completeness, so I think that what Jireh suggests is good.

[Anatole Dedecker]

Sure, it's just that I think the name "Geometry of Banach spaces" is used more than "Geometry of normed spaces"

[Jireh Loreaux]

@Filippo A. E. Nuccio can you not edit the list in that issue? Or you can comment here. I kept Alternating and Multilinear separate because they were already separate, but we could indeed nest them.

[Filippo A. E. Nuccio]

Yes yes, I ended up commenting there directly.

[Jireh Loreaux]

oh I see, I had a typo indeed.

[Jireh Loreaux]

I've started on #28698.

[Jireh Loreaux]

Int move: #29259, deprecation: #29260

[Jireh Loreaux]

BallAction, HomeomorphBall, Pointwise, SphereNormEquiv move: #29261, deprecation: #29262 (I renamed some of the files)

[Jireh Loreaux]

Real, RCLike move: #29263, deprecation: #29264 (I just realized this will conflict with the previous one, which I had tried to avoid; I've marked it as depending on the previous one)

[Jireh Loreaux]

DualNumber move: #29265, deprecation #29266

[Jireh Loreaux]

FunctionSeries, IndicatorFunction move: #29267, deprecation: #29268

[Filippo A. E. Nuccio]

Thanks! My laptop died this afternoon and I'm unable to do any lean-related work, but I'll have a look as soon as the situation improves.

[Jireh Loreaux]

OperatorNorm/* move: #29323, deprecation: I'll used Damiano's tool once this is merged.

[Jireh Loreaux]

deprecation for the above: #29329

[Jireh Loreaux]

#29445: splits and moves Extend

[Jireh Loreaux]

#29447 (depends on the previous one): splits and moves the files in the HahnBanach/ folder

[Jireh Loreaux]

#29448: moves ConformalLinearMap into the Normed/Operator/ folder

[Jireh Loreaux]

Any suggestions about what to do with MultipliableUniformlyOn? I'm tempted to dump it into Analysis/Normed/

[Jireh Loreaux]

After these, we're very close to being able to dump the contents of the NormedSpace folder directly into Normed.Module.

[Jireh Loreaux]

The last two PRs here are:

[Jireh Loreaux]

#29447

[Jireh Loreaux]

#30281 (depends on the previous one)