Hahn banach 2026

[mkerjean]

Motivation for this change

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

I made a pass on the file: moving a few lemmas to mathcomp_extra.v and unstable.v, linting the code, creating a functional_analysis sub-directory, starting the changelog (NB: it contains a fix for the changelog in master which is buggy, my bad).

Since topU is defined at the top-level and therefore exposed, maybe a name like sub_initial_topology is better (btw, it should be documented).

TODO: move the new structures out of this file.

[affeldt-aist]

Compilation is fine with MathComp 2.5.0 but it looks like with a problem with the duplication of the SubNormedZmodule in MathComp and MathComp-Analysis:

Error:
You must declare the hierarchy bottom-up or add a missing join. 
There are two ways out: 
- declare structure SubNormedZmodule before structure Num.SubNormedZmodule if Num.SubNormedZmodule inherits from it; 
- declare an additional structure that inherits from both Num.SemiNormedZmodule and SubType and from which SubNormedZmodule and/or Num.SubNormedZmodule inherit.

It this is really the case, is there a trick to make it compile with both versions? @CohenCyril @gares
(It could even be a feature of HB? Again, not sure whether my diagnosis is correct...)

[affeldt-aist]

Compilation is fine with MathComp 2.5.0 but it looks like with a problem with the duplication of the > is there a trick to make it compile with both versions? @CohenCyril @gares (It could even be a feature of HB? Again, not sure whether my diagnosis is correct...)

Like a "the version 2.X.Y of MathComp only" option?

[affeldt-aist]

we tried this trick to cheat the CI: 4d044c8

but nix fails for other reasons so this is not yet conclusive

[affeldt-aist]

@mkerjean Can this comment be removed? It looks like we have addressed the TODO by creating the factory SubLmodule_isSubNormedmodule (just above in this file).

[mkerjean]

SubLmodule_isSubNormedmodule can indeed turn a given subLmodule into a subnormedmottype, but we struggled to define a lightweight factory doing so, because of a dependency on K. I would leave that comment - or create an issue.

[affeldt-aist]

I completed a pass of cleaning. As far as I am concerned, the scripts are good enough.
We still have to get HB structures (SubNormedModule, etc.) to the right files.
Right now, we are just trying to get SubNormedZmodule out of it, by putting into
mathcomp_extra.v, but we have to trick the CI to make it happy.
As soon as the CI is green (it is still red but for orthogonal reasons), this could be done quickly, and the PR merged imo.

[mkerjean]

I completed a pass of cleaning. As far as I am concerned, the scripts are good enough. We still have to get HB structures (SubNormedModule, etc.) to the right files. Right now, we are just trying to get SubNormedZmodule out of it, by putting it into mathcomp_extra.v, but we have to trick the CI to make it happy. As soon as the CI is green (it is still red but for orthogonal reasons), this could be done quickly, and the PR merged imo.

The solution that uses isTmp in the SubNormedModule mixin apparently isn't enough to make the CI green. Should it still be left in the definition of substructures?

[affeldt-aist]

I completed a pass of cleaning. As far as I am concerned, the scripts are good enough. We still have to get HB structures (SubNormedModule, etc.) to the right files. Right now, we are just trying to get SubNormedZmodule out of it, by putting it into mathcomp_extra.v, but we have to trick the CI to make it happy. As soon as the CI is green (it is still red but for orthogonal reasons), this could be done quickly, and the PR merged imo.

The solution that uses isTmp in the SubNormedModule mixin apparently isn't enough to make the CI green. Should it still be left in the definition of substructures?

I am not sure. The CI error look unrelated, they seem to be related with some build process within nix.