Mathcomp master PseudoMetricNormedZmod #180

mkerjean · 2020-04-14T09:45:15Z

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

NB(rei): fixes #382

TODO:

Several explicit arguments are needed with this PR. E.g :

analysis/theories/derive.v

Line 789 in 45e488f

near: x; rewrite !near_simpl; apply/(@nbhs_le_nbhs_norm R (@prod_normedModType R U V')).

Why ?
Update Changelog
Check that no new (post apr. 2019) lemmas are generalizable

mkerjean · 2020-04-14T09:58:37Z

Issue: Sometimes one needs to explicitly mention the pseudoMetricNormedZmodType on which lemmas are applied while it was not necessary with NormedModTypes. It also makes (at least) derive.v fail (here view locally_le_locally_norm can't be applied). What's missing ?

mkerjean · 2020-04-14T12:48:52Z

Issue: Some further generalizations should be possible but lim does not seem to work on PseudoMetricNormedZmodule. See here.

theories/normedtype.v

affeldt-aist · 2020-04-23T15:55:47Z

This branch/PR has been rebased on PR #177 that lifts several lemmas about limits to the level of topological spaces, thus the issues about flim_lim and flim_unique have disappeared. But similar inference problems seem to occur later, e.g., here

analysis/theories/derive.v

Line 786 in b8c628c

near: x; rewrite !near_simpl; apply/locally_le_locally_norm.

.

theories/normedtype.v

affeldt-aist · 2021-05-29T14:33:15Z

theories/normedtype.v

-Lemma norm_cvg_eq x y : x --> y -> x = y. Proof. exact: cvg_eq. Qed.
-Lemma norm_lim_id x : lim x = x. Proof. exact: lim_id. Qed.
+Lemma norm_cvg_eq (x y : V) : x --> y -> x = y. Proof. exact: (@cvg_eq V). Qed.
+Lemma norm_lim_id x : [lim x in V](*NB: was lim x*) = x. Proof. exact: lim_id. Qed.


I guess this is now the main concern of this PR. This notation is properly documented, so this is acceptable to me as long as we keep the comment. @CohenCyril Is this acceptable for you too? Does the modification made to nbhs_le_nbhs_norm ring any bell by any chance?

solved by 8443585 actually...

affeldt-aist

Improve one comment and confirm the notation use with another reviewer (see the conversation).

affeldt-aist

ok with me but I am biased

from normedModType to pseudoMetricNormedZModType Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp> rebase in progress, admits inside

- use `filter_predI` instead of the new `filter_andb` (removed) - `Module BigmaxBigminr` was duplicated

- enforce the type of `nbhs` in `normedtype.v:nbhs_le_nbhs_norm` so that the type of implicit arguments look more as expected + this solves an inference problem in `derive.v:bilinear_eqo` - nitpicking about spaces

- also remove spurious comment

theories/normedtype.v

CohenCyril · 2021-07-22T08:08:59Z

theories/normedtype.v

 rewrite near_map => /nbhs_ballP[_/posnumP[a]] + xl; apply.
-move/cvg_ball : xl => /(_ _ a)/nbhs_ballP[_/posnumP[b]]; apply; exact: ballxx.
+move/(cvg_ball (y := l)): xl=> /(_ _ a)/nbhs_ballP[_/posnumP[b]]; apply; exact: ballxx.


do not use the _ := _ syntax, it is too unstable.

It looks like this actually revealed a wrong definition: 13e50e4

CohenCyril

Ready to merge after my comments have been taken into account.
Also, I would rather have TODO/NBs turned into issues, they are less prone to bitrot.

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>

- this solves at least one inference problem

affeldt-aist · 2021-07-26T06:59:03Z

Ready to merge after my comments have been taken into account.
Also, I would rather have TODO/NBs turned into issues, they are less prone to bitrot.

NBs that were marking issues caused by this PR has been resolved (I think).
There are still TODOs but I think that they predates this PR.
Ok to merge and chase TODOs later?

- generalizations of several lemmas from `normedModType` to `pseudoMetricNormedZModType` - enforce the type of `nbhs` in `normedtype.v:nbhs_le_nbhs_norm` so that the type of implicit arguments look more as expected + this solves an inference problem in `derive.v:bilinear_eqo` Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

mkerjean changed the title ~~Mathcom master pseudo normed zmod~~ Mathcomp master pseudo normed zmod Apr 14, 2020

mkerjean changed the title ~~Mathcomp master pseudo normed zmod~~ Mathcomp master PseudoMetricNormedZmod Apr 14, 2020

mkerjean marked this pull request as draft April 14, 2020 12:16

affeldt-aist reviewed Apr 14, 2020

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

affeldt-aist reviewed Apr 14, 2020

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

affeldt-aist reviewed Apr 14, 2020

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

affeldt-aist reviewed Apr 14, 2020

View reviewed changes

theories/normedtype.v Show resolved Hide resolved

affeldt-aist force-pushed the mathcomp_master branch 12 times, most recently from 5cc9b78 to 0afbda8 Compare April 22, 2020 12:48

CohenCyril force-pushed the mathcomp_master branch from 0afbda8 to b3e7e80 Compare April 22, 2020 13:32

affeldt-aist force-pushed the mathcomp_master branch 2 times, most recently from 4d1cc32 to 4905f3c Compare April 22, 2020 21:09

affeldt-aist force-pushed the mathcom_master_pseudoNormedZmod branch from 7bfee4a to b8c628c Compare April 23, 2020 14:40

affeldt-aist changed the base branch from mathcomp_master to mathcomp_master_hausdorff_close May 4, 2020 17:13

affeldt-aist force-pushed the mathcom_master_pseudoNormedZmod branch from b8c628c to 1327fea Compare May 4, 2020 17:30

CohenCyril force-pushed the mathcomp_master_hausdorff_close branch from 17086dc to 7d1689b Compare May 6, 2020 18:26

affeldt-aist force-pushed the mathcom_master_pseudoNormedZmod branch from 1327fea to 7d4bed6 Compare May 14, 2020 13:49

affeldt-aist reviewed May 29, 2021

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

affeldt-aist self-requested a review May 29, 2021 14:28

affeldt-aist reviewed May 29, 2021

View reviewed changes

affeldt-aist requested changes May 29, 2021

View reviewed changes

affeldt-aist marked this pull request as ready for review May 30, 2021 04:40

affeldt-aist force-pushed the mathcom_master_pseudoNormedZmod branch 2 times, most recently from 595a28a to 6ed13e7 Compare June 4, 2021 06:52

affeldt-aist added this to the 0.3.10 milestone Jun 14, 2021

mkerjean requested review from affeldt-aist and CohenCyril July 5, 2021 12:14

affeldt-aist approved these changes Jul 22, 2021

View reviewed changes

mkerjean and others added 5 commits July 22, 2021 16:15

generalizations of several lemmas

d4f02d2

from normedModType to pseudoMetricNormedZModType Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp> rebase in progress, admits inside

issue with product PseudoNormedZmodType

71a870e

remove useless code

aab5f2f

- use `filter_predI` instead of the new `filter_andb` (removed) - `Module BigmaxBigminr` was duplicated

fix the type of normedtype.v:nbhs_le_nbhs_norm

b62ac50

- enforce the type of `nbhs` in `normedtype.v:nbhs_le_nbhs_norm` so that the type of implicit arguments look more as expected + this solves an inference problem in `derive.v:bilinear_eqo` - nitpicking about spaces

add changelog

79dd6b5

- also remove spurious comment

affeldt-aist force-pushed the mathcom_master_pseudoNormedZmod branch from 6ed13e7 to 79dd6b5 Compare July 22, 2021 07:16

CohenCyril reviewed Jul 22, 2021

View reviewed changes

theories/normedtype.v Outdated Show resolved Hide resolved

CohenCyril reviewed Jul 22, 2021

View reviewed changes

CohenCyril requested changes Jul 22, 2021

View reviewed changes

mkerjean force-pushed the mathcom_master_pseudoNormedZmod branch from caf46d3 to 5b8886f Compare July 22, 2021 09:50

review by @CohenCyril

6cbe24e

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>

mkerjean force-pushed the mathcom_master_pseudoNormedZmod branch from 5b8886f to 6cbe24e Compare July 22, 2021 11:28

affeldt-aist added 2 commits July 26, 2021 14:52

fix filteredType definition

13e50e4

- this solves at least one inference problem

get rid of NB's and some TODOs

8443585

CohenCyril approved these changes Jul 27, 2021

View reviewed changes

CohenCyril merged commit 5aa0821 into master Jul 27, 2021

affeldt-aist deleted the mathcom_master_pseudoNormedZmod branch July 29, 2021 09:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Mathcomp master PseudoMetricNormedZmod #180

Mathcomp master PseudoMetricNormedZmod #180

mkerjean commented Apr 14, 2020 •

edited

Loading

mkerjean commented Apr 14, 2020

mkerjean commented Apr 14, 2020 •

edited

Loading

affeldt-aist commented Apr 23, 2020

affeldt-aist May 29, 2021

affeldt-aist Jul 26, 2021

affeldt-aist left a comment

affeldt-aist left a comment

CohenCyril Jul 22, 2021

affeldt-aist Jul 26, 2021

CohenCyril left a comment

affeldt-aist commented Jul 26, 2021

Mathcomp master PseudoMetricNormedZmod #180

Mathcomp master PseudoMetricNormedZmod #180

Conversation

mkerjean commented Apr 14, 2020 • edited Loading

mkerjean commented Apr 14, 2020

mkerjean commented Apr 14, 2020 • edited Loading

affeldt-aist commented Apr 23, 2020

affeldt-aist May 29, 2021

Choose a reason for hiding this comment

affeldt-aist Jul 26, 2021

Choose a reason for hiding this comment

affeldt-aist left a comment

Choose a reason for hiding this comment

affeldt-aist left a comment

Choose a reason for hiding this comment

CohenCyril Jul 22, 2021

Choose a reason for hiding this comment

affeldt-aist Jul 26, 2021

Choose a reason for hiding this comment

CohenCyril left a comment

Choose a reason for hiding this comment

affeldt-aist commented Jul 26, 2021

mkerjean commented Apr 14, 2020 •

edited

Loading

mkerjean commented Apr 14, 2020 •

edited

Loading