Banachsteinhaus

[mkerjean]

A proof of Baire and Banach-Steinhaus theorem, initiated by Theo Vignon.

Waiting for PR#183 to be merged to rebase on master.

[affeldt-aist]

I tried to simplify a bit the scripts. Tell me if I introduced to much mess, Maybe it is worth doing one more pass and discuss whether to put lemmas in other files. Should le_closed_ball moved in normedtype.v (maybe using the homo notation). Should floor_nat_comp go to reals.v? Should bounded_landau go to landau.v? @CohenCyril

[mkerjean]

I tried to simplify a bit the scripts. Tell me if I introduced to much mess.
Seems good to me, thanks :)

[mkerjean]

I tried to simplify a bit the scripts. Tell me if I introduced to much mess, Maybe it is worth doing one more pass and discuss whether to put lemmas in other files. Should le_closed_ball moved in normedtype.v (maybe using the homo notation). Should floor_nat_comp go to reals.v? Should bounded_landau go to landau.v? @CohenCyril

As bounded_landau depends of the newly introduced defininition bounded_fun_norm, shouldn't it stay in near Banach-Steinhaus theorem for the time being ? And then Banach-Steinhaus needs to be inserted as a section/module in landau.v ?

[affeldt-aist]

As bounded_landau depends of the newly introduced defininition bounded_fun_norm,
shouldn't it stay in near Banach-Steinhaus theorem for the time being ?

I was thinking that bounded_fun_norm would go to landau.v too.

And then Banach-Steinhaus needs to be inserted as a section/module in landau.v ?

Indeed, we wrongly stated that it should go to normedtype.v during the meeting. :-(

[affeldt-aist]

Follow-up to Friday's meeting: I tried to replace floor_nat_comp with more primitive lemmas and the usage of ceil.

[mkerjean]

At the end Baire's theorem depends on sequences, thus Baire's and Banach-Steinhauss theorem have been added in sequences.v, as well as the auxiliary definitions on bounded function (to be removed one day).

[affeldt-aist]

NB: This PR uses the lemma gtz0_norm expecting it to be integrated into MathComp.
This is rather this lemma:

Lemma natr_absz i : `|i|%:R = `|i|%:~R :> R.
Proof. by rewrite -abszE. Qed.

that is likely to be merged into MathComp (see PR math-comp/math-comp#732).
Maybe update this PR accordingly?

[mkerjean]

NB: This PR uses the lemma gtz0_norm expecting it to be integrated into MathComp. This is rather this lemma:

Lemma natr_absz i : `|i|%:R = `|i|%:~R :> R.
Proof. by rewrite -abszE. Qed.

that is likely to be merged into MathComp (see PR math-comp/math-comp#732). Maybe update this PR accordingly?

These lemmas have been integrated to MathComp 1.13 and Analysis seems to depend on math-comp 1.13, but I can't find them within sequence.v in this branch, any idea why ?

[CohenCyril]

These lemmas have been integrated to MathComp 1.13 and Analysis seems to depend on math-comp 1.13, but I can't find them within sequence.v in this branch, any idea why ?

Hi! mathcomp-analysis is compatible with both (and with 1.14 too), and the default nix-shell uses the most conservative of the two (so 1.12.0).
I am strongly in support of dropping 1.12.0 ASAP, that would solve your issue and several of mine :)

[CohenCyril]

Meanwhile is you use nix-shell --argstr bundle 8.14 it will use Coq 8.14 and force mathcomp to 1.13.