Stream: math-comp analysis

Topic: Gihub Notifications

Mathcomp Analysis Github Bot (May 07 2020 at 18:36):

GitHub webhook has been successfully configured by CohenCyril.

Mathcomp Analysis Github Bot (May 07 2020 at 19:45):

affeldt-aist pushed 1 commit to branch fixes155.

• fixes #155 (3b963a9)

Mathcomp Analysis Github Bot (May 07 2020 at 20:10):

affeldt-aist pushed 1 commit to branch bounded.

• typo (842175a)

Mathcomp Analysis Github Bot (May 07 2020 at 20:15):

CohenCyril pushed 6 commits to branch mathcomp_master_sequences. Commits by CohenCyril (3) and affeldt-aist (3).

• a few results about sequences (0b038ef)
• Reusing previous results in more agressive way (15be0fd)
• Convergence theorems (5b58af8)
• Big refactoring in sequences.v (724b76f)
• updating lim_ge, ler_lim and (inc|dec)reasing*cvg (cd3797c)
• prove a few admitteds, one renaming, typos (wip) (6e152ac)

Mathcomp Analysis Github Bot (May 07 2020 at 20:24):

CohenCyril pushed 7 commits to branch cvg_naming. Commits by CohenCyril (4) and affeldt-aist (3).

• Big refactoring about naming conventions (a6210a5)
• a few results about sequences (795d9d6)
• Reusing previous results in more agressive way (00bc34c)
• Convergence theorems (c102919)
• Big refactoring in sequences.v (7ae8e42)
• updating lim_ge, ler_lim and (inc|dec)reasing*cvg (70783ba)
• prove a few admitteds, one renaming, typos (wip) (3eb2294)

Mathcomp Analysis Github Bot (May 07 2020 at 20:25):

CohenCyril pushed the branch cvg_naming.

Mathcomp Analysis Github Bot (May 07 2020 at 20:49):

CohenCyril pushed 2 commits to branch cvg_naming.

• Big refactoring about naming conventions (cd821d2)
• Big refactoring about naming conventions (10e56ee)

Mathcomp Analysis Github Bot (May 07 2020 at 20:52):

CohenCyril pushed 1 commit to branch cvg_naming.

• Big refactoring about naming conventions (9950ef0)

Mathcomp Analysis Github Bot (May 07 2020 at 21:57):

CohenCyril pushed 1 commit to branch cvg_naming.

• Big refactoring about naming conventions (bba89c9)

Mathcomp Analysis Github Bot (May 07 2020 at 22:23):

CohenCyril pushed 1 commit to branch mathcomp_master_sequences. Commits by affeldt-aist (1).

• Main theorems about sequences, series and examples (745021f)

Mathcomp Analysis Github Bot (May 07 2020 at 22:56):

CohenCyril pushed 1 commit to branch mathcomp_master_sequences. Commits by affeldt-aist (1).

• Main theorems about sequences, series and examples (2fc69fc)

Mathcomp Analysis Github Bot (May 07 2020 at 23:04):

CohenCyril pushed 2 commits to branch mathcomp_master_sequences. Commits by CohenCyril (1) and affeldt-aist (1).

• Various renamings (0c50284)
• Main theorems about sequences, series and examples (0752777)

Mathcomp Analysis Github Bot (May 07 2020 at 23:05):

CohenCyril pushed 2 commits to branch master.

• Big refactoring about naming conventions (bba89c9)
• Merge pull request #199 from math-comp/cvg_naming (80044c4)

Mathcomp Analysis Github Bot (May 07 2020 at 23:06):

CohenCyril pushed the branch renamings.

Mathcomp Analysis Github Bot (May 07 2020 at 23:09):

CohenCyril pushed 1 commit to branch renamings. Commits by affeldt-aist (1).

• Various renamings (33e384a)

Mathcomp Analysis Github Bot (May 07 2020 at 23:11):

CohenCyril pushed 1 commit to branch travis_not_twice.

• make travis not run twice! (1d128ee)

Mathcomp Analysis Github Bot (May 07 2020 at 23:28):

CohenCyril pushed 1 commit to branch master. Commits by affeldt-aist (1).

• Various renamings (2eccc5f)

Mathcomp Analysis Github Bot (May 07 2020 at 23:38):

CohenCyril pushed 1 commit to branch mathcomp_master_sequences.

• Main theorems about sequences, series and examples (705fb3c)

Mathcomp Analysis Github Bot (May 08 2020 at 00:32):

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

• wip (d46f236)

Mathcomp Analysis Github Bot (May 08 2020 at 02:36):

CohenCyril pushed 1 commit to branch master.

• make travis not run twice! (fac1196)

Mathcomp Analysis Github Bot (May 08 2020 at 02:36):

CohenCyril deleted the branch travis_not_twice.

Mathcomp Analysis Github Bot (May 08 2020 at 13:58):

CohenCyril pushed 1 commit to branch bounded.

• Generic domination, boundedness and lipshitz (f4c6b19)

Mathcomp Analysis Github Bot (May 08 2020 at 13:59):

CohenCyril pushed 1 commit to branch bounded.

• Generic domination, boundedness and lipschitz (c2cea9a)

Mathcomp Analysis Github Bot (May 08 2020 at 14:19):

CohenCyril pushed 1 commit to branch better_inE.

• in_setE/in_fsetE -> inE (7d5747f)

Mathcomp Analysis Github Bot (May 08 2020 at 15:11):

CohenCyril pushed 1 commit to branch master.

• Generic domination, boundedness and lipschitz (20b79f7)

Mathcomp Analysis Github Bot (May 08 2020 at 15:13):

CohenCyril pushed 1 commit to branch better_inE.

• in_setE/in_fsetE -> inE (3862fb8)

Mathcomp Analysis Github Bot (May 08 2020 at 16:09):

CohenCyril pushed 1 commit to branch better_inE.

• in_setE/in_fsetE -> inE (fe37a38)

Mathcomp Analysis Github Bot (May 08 2020 at 16:09):

CohenCyril pushed 1 commit to branch mathcomp_master_sequences. Commits by affeldt-aist (1).

• Main theorems about sequences, series and examples (7ae1958)

Mathcomp Analysis Github Bot (May 08 2020 at 16:31):

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

• proved nonincreasing_cvg, minor cleaning (53f126e)

Mathcomp Analysis Github Bot (May 08 2020 at 16:50):

CohenCyril pushed 1 commit to branch mathcomp_master_sequences. Commits by affeldt-aist (1).

• Main theorems about sequences, series and examples (26c7366)

Mathcomp Analysis Github Bot (May 08 2020 at 16:50):

CohenCyril pushed 1 commit to branch master.

• in_setE/in_fsetE -> inE (f8d361a)

Mathcomp Analysis Github Bot (May 08 2020 at 17:00):

CohenCyril pushed 1 commit to branch mathcomp_master_sequences. Commits by affeldt-aist (1).

• Main theorems about sequences, series and examples (7d7c97e)

Mathcomp Analysis Github Bot (May 08 2020 at 17:00):

CohenCyril deleted the branch better_inE.

Mathcomp Analysis Github Bot (May 09 2020 at 19:41):

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

• add a few lemmas (7b3435e)

Mathcomp Analysis Github Bot (May 09 2020 at 19:41):

affeldt-aist updated PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs. There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.

Mathcomp Analysis Github Bot (May 09 2020 at 19:47):

affeldt-aist pushed 1 commit to branch contributing_guide.

• add a comment about near tactics vs. filter lemmas (9eaa601)

Mathcomp Analysis Github Bot (May 09 2020 at 19:47):

affeldt-aist updated PR #197 contributing file from contributing_guide to master:

The goal is to explain good practices that are specific to mathcomp-analysis. Still embryonic.

Mathcomp Analysis Github Bot (May 09 2020 at 19:56):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 09 2020 at 21:51):

CohenCyril submitted PR Review for #187 A few lemmas about sequences.

Mathcomp Analysis Github Bot (May 09 2020 at 21:51):

CohenCyril created PR Review Comment on #187 A few lemmas about sequences:

use sum_nat_const

Mathcomp Analysis Github Bot (May 10 2020 at 22:10):

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

• use sum_nat_const_nat in cesaro (6f5eefd)

Mathcomp Analysis Github Bot (May 10 2020 at 22:10):

affeldt-aist updated PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs. There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.

Mathcomp Analysis Github Bot (May 11 2020 at 20:34):

affeldt-aist pushed 2 commits to branch supremums_ereal.

• generalize ub, lb, etc. from reals.v (a1c546f)
• Sets of supremums of extended reals are not empty (3126267)

Mathcomp Analysis Github Bot (May 11 2020 at 20:41):

affeldt-aist opened PR #203 Supremums ereal from supremums_ereal to master:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (May 11 2020 at 23:29):

affeldt-aist pushed 1 commit to branch supremums_ereal.

• Sets of supremums of extended reals are not empty (48661cc)

Mathcomp Analysis Github Bot (May 11 2020 at 23:29):

affeldt-aist updated PR #203 Supremums ereal from supremums_ereal to master:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (May 12 2020 at 16:41):

CohenCyril pushed 1 commit to branch mathcomp_master_sequences.

• simplifying Cesaro (7adaef8)

Mathcomp Analysis Github Bot (May 12 2020 at 16:41):

CohenCyril updated PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs. There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.

Mathcomp Analysis Github Bot (May 13 2020 at 23:19):

CohenCyril closed Issue #165 Canonical structures on a given type:

How could we construct a tool which would unveil all the canonical structures on a given type at some point in a Coq file ? Could the hierarchy builder tool help ?(https://github.com/math-comp/hierarchy-builder) Could we build automatically a graph of the canonical declarations of structures and their dependencies ?

This seems crucial when using mathcomp analysis libraries, where one uses regularly the basic properties of a type endowed with much richer structure.

Mathcomp Analysis Github Bot (May 14 2020 at 09:12):

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

• tentative converse of cesaro (wip) (a69e18a)

Mathcomp Analysis Github Bot (May 14 2020 at 09:12):

affeldt-aist updated PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs. There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.

Mathcomp Analysis Github Bot (May 14 2020 at 11:50):

mkerjean edited PR #188 Topological structures on numDomains and numFields from locallyN_lim_cst_generalization to master:

Is this change of canonical structures correct?

Mathcomp Analysis Github Bot (May 14 2020 at 11:51):

mkerjean edited PR #192 Holomorphy from cauchy_etoile to mathcomp_master_hausdorff_close:

This PR gathers commits that contribute to cauchyetoile.v by @mkerjean. They were cherry-picked from the branch mathcomp_master_integral_ereal. Some are the results of splits of commits from mathcomp_master_integral_ereal.

Mathcomp Analysis Github Bot (May 14 2020 at 12:00):

affeldt-aist pushed 10 commits to branch cauchy_etoile. Commits by affeldt-aist (6), mkerjean (3) and CohenCyril (1).

• Mathcomp analysis now depends on real-closed (d1ed227)
• proof of Cauchy thm; derivx, derivy (7fba627)
• holomorphic is derivable, holomorphic implies Cauchy-Riemann (e3289d5)
• update cauchyetoile.v wrt PR#270 (1f0898f)
• update cauchyetoile.v wrt PR#270 (3010cdc)
• renaming: Uniform -> PseudoMetric (e70d201)
• wip (f47b497)
• update cauchyetoile.v (7f431b8)
• fix to compile (cfaf5e7)
• update wrt master (7be3df2)

Mathcomp Analysis Github Bot (May 14 2020 at 12:00):

affeldt-aist updated PR #192 Holomorphy from cauchy_etoile to mathcomp_master_hausdorff_close:

This PR gathers commits that contribute to cauchyetoile.v by @mkerjean. They were cherry-picked from the branch mathcomp_master_integral_ereal. Some are the results of splits of commits from mathcomp_master_integral_ereal.

Mathcomp Analysis Github Bot (May 14 2020 at 12:00):

affeldt-aist edited PR #192 Holomorphy from cauchy_etoile to master:

This PR gathers commits that contribute to cauchyetoile.v by @mkerjean. They were cherry-picked from the branch mathcomp_master_integral_ereal. Some are the results of splits of commits from mathcomp_master_integral_ereal.

Mathcomp Analysis Github Bot (May 14 2020 at 12:05):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 14 2020 at 13:22):

mkerjean pushed 1 commit to branch cauchy_etoile.

• name change (e09c8a2)

Mathcomp Analysis Github Bot (May 14 2020 at 13:22):

mkerjean updated PR #192 Holomorphy from cauchy_etoile to master:

This PR gathers commits that contribute to cauchyetoile.v by @mkerjean. They were cherry-picked from the branch mathcomp_master_integral_ereal. Some are the results of splits of commits from mathcomp_master_integral_ereal.

Mathcomp Analysis Github Bot (May 14 2020 at 13:24):

mkerjean deleted the branch cauchy_etoile.

Mathcomp Analysis Github Bot (May 14 2020 at 13:24):

mkerjean closed without merge PR #192 Holomorphy.

Mathcomp Analysis Github Bot (May 14 2020 at 13:27):

mkerjean pushed 11 commits to branch holomorphy. Commits by affeldt-aist (6), mkerjean (4) and CohenCyril (1).

• Mathcomp analysis now depends on real-closed (d1ed227)
• proof of Cauchy thm; derivx, derivy (7fba627)
• holomorphic is derivable, holomorphic implies Cauchy-Riemann (e3289d5)
• update cauchyetoile.v wrt PR#270 (1f0898f)
• update cauchyetoile.v wrt PR#270 (3010cdc)
• renaming: Uniform -> PseudoMetric (e70d201)
• wip (f47b497)
• update cauchyetoile.v (7f431b8)
• fix to compile (cfaf5e7)
• update wrt master (7be3df2)
• name change (e09c8a2)

Mathcomp Analysis Github Bot (May 14 2020 at 13:39):

mkerjean opened PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed PR#192.

Mathcomp Analysis Github Bot (May 14 2020 at 13:49):

affeldt-aist pushed 1 commit to branch mathcom_master_pseudoNormedZmod. Commits by mkerjean (1).

• generalizations of several lemmas (7d4bed6)

Mathcomp Analysis Github Bot (May 14 2020 at 13:49):

affeldt-aist updated PR #180 Mathcomp master PseudoMetricNormedZmod from mathcom_master_pseudoNormedZmod to mathcomp_master_hausdorff_close:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

Mathcomp Analysis Github Bot (May 14 2020 at 13:49):

affeldt-aist edited PR #180 Mathcomp master PseudoMetricNormedZmod from mathcom_master_pseudoNormedZmod to master:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

Mathcomp Analysis Github Bot (May 14 2020 at 16:15):

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

• use little-o notation in the statement of cesaro converse (60bb54b)

Mathcomp Analysis Github Bot (May 14 2020 at 16:15):

affeldt-aist updated PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs. There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.

Mathcomp Analysis Github Bot (May 14 2020 at 18:21):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 14 2020 at 18:26):

affeldt-aist deleted the branch mathcomp_master_hausdorff_close.

Mathcomp Analysis Github Bot (May 14 2020 at 18:26):

affeldt-aist deleted the branch bounded.

Mathcomp Analysis Github Bot (May 14 2020 at 18:27):

affeldt-aist deleted the branch fixes155.

Mathcomp Analysis Github Bot (May 14 2020 at 18:27):

affeldt-aist deleted the branch sequences.

Mathcomp Analysis Github Bot (May 14 2020 at 18:28):

affeldt-aist deleted the branch analysis_270.

Mathcomp Analysis Github Bot (May 14 2020 at 18:30):

affeldt-aist deleted the branch mathcomp_master_hausdorff.

Mathcomp Analysis Github Bot (May 14 2020 at 18:32):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 15 2020 at 11:36):

mkerjean pushed 1 commit to branch holomorphy.

• clean (3ead4f3)

Mathcomp Analysis Github Bot (May 15 2020 at 11:36):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed PR#192.

Mathcomp Analysis Github Bot (May 15 2020 at 13:26):

CohenCyril edited PR #193 Renaming flim to cvg from renamings to master:

Fixes #29

• cvg corresponds to _ --> _
• lim corresponds to lim _
• continuous corresponds to continuity
• some suffixes _opp, _add ... renamed to N, D, ...

In order to rebase on top of this, instead of rebase, do:

rm -f *.patch
git remote update
git format-patch upstream/master
git reset --hard upstream/master
sed -i -f etc/pr193.sed *.patch
git am *.patch
rm -f *.patch

Please make backups and if you get in trouble, rebase your work on top of 283b4330aa4327640c6e6a499c861ebc714ddd18 and then contact @CohenCyril

@math-comp/analysis what do you think about this conventions?

Mathcomp Analysis Github Bot (May 15 2020 at 13:30):

mkerjean pushed 1 commit to branch holomorphy.

• within formalisation (83072ba)

Mathcomp Analysis Github Bot (May 15 2020 at 13:30):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed PR#192.

Mathcomp Analysis Github Bot (May 15 2020 at 16:28):

CohenCyril edited PR #188 Topological structures on numFields from locallyN_lim_cst_generalization to master:

Is this change of canonical structures correct?

Mathcomp Analysis Github Bot (May 15 2020 at 16:32):

CohenCyril edited PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 15 2020 at 21:11):

mkerjean pushed 1 commit to branch holomorphy.

• rebase on PR199 (01c534a)

Mathcomp Analysis Github Bot (May 15 2020 at 21:11):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 15 2020 at 21:16):

mkerjean pushed 1 commit to branch holomorphy.

• name change (85aa10a)

Mathcomp Analysis Github Bot (May 15 2020 at 21:16):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 15 2020 at 21:34):

mkerjean pushed 1 commit to branch holomorphy.

• rebase on PR199 (c383ce6)

Mathcomp Analysis Github Bot (May 15 2020 at 21:34):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 15 2020 at 21:40):

mkerjean pushed 1 commit to branch holomorphy.

• update CoqProject (a320f3f)

Mathcomp Analysis Github Bot (May 15 2020 at 21:40):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 15 2020 at 21:48):

mkerjean pushed the branch numfield_topology.

Mathcomp Analysis Github Bot (May 15 2020 at 22:05):

mkerjean pushed 1 commit to branch holomorphy.

• update CoqProject (8339fd8)

Mathcomp Analysis Github Bot (May 15 2020 at 22:05):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 15 2020 at 23:03):

mkerjean pushed 5 commits to branch numfield_topology.

• normedType on numFieldType (56cebec)
• erasing ^o wip (ba32b6a)
• erasing ^o numFieldType_canonical_contd (afc82ce)
• erasing ^o wip (8e5b0c4)
• normedType of realFieldType (ef0368e)

Mathcomp Analysis Github Bot (May 15 2020 at 23:12):

mkerjean opened PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (May 15 2020 at 23:25):

mkerjean pushed 1 commit to branch numfield_topology.

• vecspace of numField (baad880)

Mathcomp Analysis Github Bot (May 15 2020 at 23:25):

mkerjean updated PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (May 16 2020 at 10:11):

affeldt-aist pushed 1 commit to branch supremums_ereal.

• trying to control the unfolding of ub (76e89f1)

Mathcomp Analysis Github Bot (May 16 2020 at 10:11):

affeldt-aist updated PR #203 Supremums ereal from supremums_ereal to master:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (May 17 2020 at 23:17):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• wip (4e710e9)

Mathcomp Analysis Github Bot (May 17 2020 at 23:17):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to master:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (May 18 2020 at 07:13):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• wip (a7ce0de)

Mathcomp Analysis Github Bot (May 18 2020 at 07:13):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to master:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (May 18 2020 at 21:11):

vlj opened PR #206 Add a distrLattice canonical structure to set T. from subset-lattice to master:

Hi,

This add a canonical distrLattice structure to setT and subset relation.
I have far less experience in adding a canonical structure than I have writing lemma so the PR is likely a bit rough, any guidance is appreciated.

Some comments:

• For some reasons coq fails to unify the type of the lemma setU setI ... when passed as argument to MeetJoinMixin. I added "wrapper lemma" SetOrder_setCI SetOrder_setCU ... to force the type. I'm not sure this is the right thing to do (I could also use @setU (set T) directly in the argument but it would be quite hard to read) and the naming is maybe wrong.
• subset is a Prop while distrLattice expects a rel (ie result type is bool). I wrapped the subset relation in asboolsubset. This means that to use lemma in order (like in my case ltux) one need to map subset and asboolsubset forth and back so I provided subsetE. I don't know if it's the usual idiom.

Mathcomp Analysis Github Bot (May 21 2020 at 00:03):

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

• Main theorems about sequences, series and examples (ab09f80)

Mathcomp Analysis Github Bot (May 21 2020 at 00:03):

affeldt-aist updated PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs. There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.

Mathcomp Analysis Github Bot (May 21 2020 at 00:10):

affeldt-aist pushed the branch more_sequences.

Mathcomp Analysis Github Bot (May 21 2020 at 00:11):

affeldt-aist pushed 1 commit to branch more_sequences.

• more lemmas about sequences (d38dd5e)

Mathcomp Analysis Github Bot (May 21 2020 at 00:12):

affeldt-aist opened PR #207 more lemmas about sequences from more_sequences to mathcomp_master_sequences.

Mathcomp Analysis Github Bot (May 21 2020 at 00:15):

affeldt-aist edited PR #207 more lemmas about sequences from more_sequences to mathcomp_master_sequences:

This PR is the result of a split of the PR #187 .
It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for sequences.v.

Mathcomp Analysis Github Bot (May 21 2020 at 00:24):

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

• Main theorems about sequences and series and examples (6aa1b42)

Mathcomp Analysis Github Bot (May 21 2020 at 00:24):

affeldt-aist updated PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs. There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.

Mathcomp Analysis Github Bot (May 21 2020 at 00:25):

affeldt-aist pushed 1 commit to branch more_sequences.

• Examples of sequences and series (ded45f7)

Mathcomp Analysis Github Bot (May 21 2020 at 00:25):

affeldt-aist updated PR #207 more lemmas about sequences from more_sequences to mathcomp_master_sequences:

This PR is the result of a split of the PR #187 .
It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for sequences.v.

Mathcomp Analysis Github Bot (May 21 2020 at 00:27):

affeldt-aist edited PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs. <del>There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.</del>

Mathcomp Analysis Github Bot (May 21 2020 at 00:28):

affeldt-aist edited PR #187 A few lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs (PR #207 is such a PR). <del>There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.</del>

Mathcomp Analysis Github Bot (May 21 2020 at 00:32):

affeldt-aist pushed 1 commit to branch more_sequences.

• Examples of sequences and series (8de5885)

Mathcomp Analysis Github Bot (May 21 2020 at 00:32):

affeldt-aist updated PR #207 more lemmas about sequences from more_sequences to mathcomp_master_sequences:

This PR is the result of a split of the PR #187 .
It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for sequences.v.

Mathcomp Analysis Github Bot (May 21 2020 at 00:33):

affeldt-aist edited PR #187 Basic lemmas about sequences from mathcomp_master_sequences to master:

The purpose of this PR is to add a file sequences.v to gather standard definitions and lemmas about sequences. It certainly deserves to be improved (completed and generalized) but maybe it is worth having it as soon as possible to have a place to share lemmas, e..g, for increasing sequences, and to defer improvements to future PRs (PR #207 is such a PR). <del>There is also a file sequences_examples.v that defines a few standard sequences and proves a few lemmas about them, mostly as a test bed.</del>

Mathcomp Analysis Github Bot (May 21 2020 at 01:13):

affeldt-aist pushed 1 commit to branch ereal_arithmetic.

• a few lemmas about extended reals' arithmetic (db26276)

Mathcomp Analysis Github Bot (May 21 2020 at 01:15):

affeldt-aist opened PR #208 a few lemmas about extended reals' arithmetic from ereal_arithmetic to master:

Just a couple of easy lemmas that I missed during some work on another PR.

Mathcomp Analysis Github Bot (May 21 2020 at 01:45):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• tentative proof that extended reals from a pseudometric space (6b81100)

Mathcomp Analysis Github Bot (May 21 2020 at 01:45):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to master:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (May 21 2020 at 01:48):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• tentative proof that extended reals from a pseudometric space (22ba6a0)

Mathcomp Analysis Github Bot (May 21 2020 at 01:48):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to master:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (May 21 2020 at 12:54):

affeldt-aist pushed 1 commit to branch mathcom_master_pseudoNormedZmod.

• enough generalizations for compilation to go through (55b94bd)

Mathcomp Analysis Github Bot (May 21 2020 at 12:54):

affeldt-aist updated PR #180 Mathcomp master PseudoMetricNormedZmod from mathcom_master_pseudoNormedZmod to master:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

Mathcomp Analysis Github Bot (May 21 2020 at 13:11):

affeldt-aist pushed 1 commit to branch mathcom_master_pseudoNormedZmod.

• remove useless(?) lemma (d01e689)

Mathcomp Analysis Github Bot (May 21 2020 at 13:11):

affeldt-aist updated PR #180 Mathcomp master PseudoMetricNormedZmod from mathcom_master_pseudoNormedZmod to master:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

Mathcomp Analysis Github Bot (May 21 2020 at 13:59):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 21 2020 at 17:29):

affeldt-aist pushed 1 commit to branch subrKA_subr_trans.

• use mathcomp's subrKA instead of sub_trans (81c056c)

Mathcomp Analysis Github Bot (May 21 2020 at 17:30):

affeldt-aist opened PR #209 use mathcomp's subrKA instead of sub_trans from subrKA_subr_trans to master:

small fix

Mathcomp Analysis Github Bot (May 21 2020 at 17:49):

CohenCyril merged PR #209 use mathcomp's subrKA instead of sub_trans.

Mathcomp Analysis Github Bot (May 21 2020 at 17:49):

CohenCyril pushed 1 commit to branch master. Commits by affeldt-aist (1).

• use mathcomp's subrKA instead of sub_trans (e4121de)

Mathcomp Analysis Github Bot (May 21 2020 at 17:49):

CohenCyril deleted the branch subrKA_subr_trans.

Mathcomp Analysis Github Bot (May 23 2020 at 01:36):

CohenCyril pushed 24 commits to branch nix. Commits by CohenCyril (14) and affeldt-aist (10).

• Merge pull request #191 from math-comp/nix (283b433)
• lemmas about bigmaxr and argmaxr (53317c0)
• Renaming flim to cvg (c1a111b)
• Merge pull request #194 from math-comp/bigmax_argmax (fea0d1a)
• Merge pull request #193 from math-comp/renamings (337a80c)
• renaming: is_prop -> is_subset1 (issue 24) (3561139)
• Merge pull request #195 from math-comp/is_prop_is_subset1 (5bef9ab)
• tentative definitions of T2separated and closeness (27a8fc9)
• ported closness to topological spaces and link with hausdorff (5a61fa9)
• topological type mixin for ereal (0639e16)
• add lemmas and perform generalizations (b085a9a)
• fix the definition of le_ereal, lt_ereal (ef24876)
• cleanup (wip) (5475ebe)
• fix lee_pinfty and lee_ninfty (827adb1)
• small renamings and left a comment for later on (7d1689b)
• Merge pull request #177 from math-comp/mathcomp_master_hausdorff_close (900f5a3)
• Big refactoring about naming conventions (bba89c9)
• Merge pull request #199 from math-comp/cvg_naming (80044c4)
• Various renamings (2eccc5f)
• make travis not run twice! (fac1196)
  [and 4 more commit(s)]

Mathcomp Analysis Github Bot (May 23 2020 at 01:36):

CohenCyril opened PR #210 upgrading default.nix from nix to master.

Mathcomp Analysis Github Bot (May 23 2020 at 01:39):

CohenCyril merged PR #208 a few lemmas about extended reals' arithmetic.

Mathcomp Analysis Github Bot (May 23 2020 at 01:39):

CohenCyril pushed 1 commit to branch master. Commits by affeldt-aist (1).

• a few lemmas about extended reals' arithmetic (c8846c6)

Mathcomp Analysis Github Bot (May 23 2020 at 02:16):

CohenCyril merged PR #210 upgrading default.nix.

Mathcomp Analysis Github Bot (May 23 2020 at 02:16):

CohenCyril pushed 1 commit to branch master.

• upgrading default.nix (4fe4b7a)

Mathcomp Analysis Github Bot (May 23 2020 at 02:17):

CohenCyril merged PR #187 Basic lemmas about sequences.

Mathcomp Analysis Github Bot (May 23 2020 at 02:17):

CohenCyril pushed 1 commit to branch master. Commits by affeldt-aist (1).

• Main theorems about sequences and series and examples (b318306)

Mathcomp Analysis Github Bot (May 23 2020 at 02:20):

CohenCyril deleted the branch nix.

Mathcomp Analysis Github Bot (May 23 2020 at 02:23):

CohenCyril pushed 1 commit to branch master.

• Update README.md (1a1648a)

Mathcomp Analysis Github Bot (May 23 2020 at 02:27):

CohenCyril pushed 1 commit to branch master.

• Update README.md (a20000d)

Mathcomp Analysis Github Bot (May 23 2020 at 18:35):

mkerjean pushed 4 commits to branch numfield_topology.

• add complex theory (9619206)
• cvgN and cvgD with explicit arguments (5b03316)
• holomorphy without Ro (bc8d5f0)
• wip (ea1b2e4)

Mathcomp Analysis Github Bot (May 23 2020 at 18:35):

mkerjean updated PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (May 23 2020 at 19:28):

CohenCyril pushed 1 commit to branch nix.

• updating config.nix (efb75d7)

Mathcomp Analysis Github Bot (May 23 2020 at 19:29):

CohenCyril opened PR #211 updating config.nix from nix to master.

Mathcomp Analysis Github Bot (May 23 2020 at 20:04):

CohenCyril merged PR #211 updating config.nix.

Mathcomp Analysis Github Bot (May 23 2020 at 20:04):

CohenCyril pushed 1 commit to branch master.

• updating config.nix (eca06c7)

Mathcomp Analysis Github Bot (May 23 2020 at 20:15):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 24 2020 at 10:49):

mkerjean:

• edited Home

Mathcomp Analysis Github Bot (May 24 2020 at 10:55):

mkerjean pushed 1 commit to branch numfield_topology.

• Impossible NormedModType structure (23f40d5)

Mathcomp Analysis Github Bot (May 24 2020 at 10:55):

mkerjean updated PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (May 24 2020 at 12:05):

mkerjean:

• edited Home

Mathcomp Analysis Github Bot (May 24 2020 at 22:09):

affeldt-aist pushed 7 commits to branch mathcomp_master_integration_ereal.

• update integral.v w.r.t. PR#270 (61cfe51)
• update integral wrt PR#270 (dd126e4)
• Boole's inequality (wip) (56a81a5)
• minor progress in integral.v (46103cc)
• turn axioms into hypotheses, add references to technical report (02d8360)
• any subset of the extended reals has a supremum (d2369b4)
• tentative proof that extended reals from a pseudometric space (15ba457)

Mathcomp Analysis Github Bot (May 24 2020 at 22:09):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to master:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (May 25 2020 at 10:01):

affeldt-aist pushed 4 commits to branch supremums_ereal.

• generalize ub, lb, etc. from reals.v (d5cb8af)
• Sets of supremums of extended reals are not empty (c7e05ea)
• trying to control the unfolding of ub (600024b)
• rebase sequences.v (31f83c2)

Mathcomp Analysis Github Bot (May 25 2020 at 10:01):

affeldt-aist updated PR #203 Supremums ereal from supremums_ereal to master:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (May 25 2020 at 12:29):

mkerjean pushed 1 commit to branch numfield_topology.

• test (e43f6c4)

Mathcomp Analysis Github Bot (May 25 2020 at 12:29):

mkerjean updated PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (May 25 2020 at 14:26):

affeldt-aist:

• created 2020 05 25 Meeting

Mathcomp Analysis Github Bot (May 25 2020 at 14:29):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 25 2020 at 14:39):

affeldt-aist merged PR #114 tentative definition of bigmaxr with bigop.

Mathcomp Analysis Github Bot (May 25 2020 at 14:39):

affeldt-aist pushed 1 commit to branch master.

• tentative definition of bigmaxr with bigop (4c30ca2)

Mathcomp Analysis Github Bot (May 25 2020 at 20:36):

mkerjean pushed 1 commit to branch numfield_topology.

• without ComplexField (3159f85)

Mathcomp Analysis Github Bot (May 25 2020 at 20:36):

mkerjean updated PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (May 25 2020 at 20:39):

affeldt-aist pushed 1 commit to branch changelog.

• tentative changelog (f13a80b)

Mathcomp Analysis Github Bot (May 25 2020 at 20:42):

affeldt-aist opened PR #212 tentative changelog from changelog to master:

I have just copy-pasted information from the commits in master down to circa September 2019, since we started to port on top of MathComp 1.11 in October 2019.

Mathcomp Analysis Github Bot (May 25 2020 at 20:42):

affeldt-aist requested CohenCyril for a review on PR #212 tentative changelog.

Mathcomp Analysis Github Bot (May 25 2020 at 20:42):

mkerjean pushed 1 commit to branch numfield_topology.

• without ComplexField (90cc8e8)

Mathcomp Analysis Github Bot (May 25 2020 at 20:43):

mkerjean updated PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (May 25 2020 at 20:47):

CohenCyril submitted PR Review for #212 tentative changelog.

Mathcomp Analysis Github Bot (May 25 2020 at 20:47):

CohenCyril created PR Review Comment on #212 tentative changelog:

    * a general one `numFieldType`  (`inv_` lemmas in normedtype.v, no differential so far, just continuity)

Mathcomp Analysis Github Bot (May 25 2020 at 20:48):

CohenCyril pushed 1 commit to branch changelog.

• Update CHANGELOG_UNRELEASED.md (d8415e9)

Mathcomp Analysis Github Bot (May 25 2020 at 20:48):

CohenCyril updated PR #212 tentative changelog from changelog to master:

I have just copy-pasted information from the commits in master down to circa September 2019, since we started to port on top of MathComp 1.11 in October 2019.

Mathcomp Analysis Github Bot (May 25 2020 at 20:59):

CohenCyril submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (May 25 2020 at 20:59):

CohenCyril submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (May 25 2020 at 20:59):

CohenCyril created PR Review Comment on #205 Topological structures on numfields:

This section looks dangerous to me. Is it necessary to make things work?

Mathcomp Analysis Github Bot (May 25 2020 at 21:02):

affeldt-aist pushed 1 commit to branch supremums_ereal.

• fix (f29b661)

Mathcomp Analysis Github Bot (May 25 2020 at 21:02):

affeldt-aist updated PR #203 Supremums ereal from supremums_ereal to master:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (May 25 2020 at 21:08):

affeldt-aist deleted the branch ereal_arithmetic.

Mathcomp Analysis Github Bot (May 25 2020 at 21:09):

affeldt-aist deleted the branch analysis_270_integration.

Mathcomp Analysis Github Bot (May 25 2020 at 21:12):

affeldt-aist deleted the branch cvg_naming.

Mathcomp Analysis Github Bot (May 26 2020 at 15:53):

mkerjean pushed 1 commit to branch numfield_topology.

• clean (2c5886e)

Mathcomp Analysis Github Bot (May 26 2020 at 15:53):

mkerjean updated PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (May 26 2020 at 15:53):

mkerjean created PR Review Comment on #205 Topological structures on numfields:

Nope, corrected.

Mathcomp Analysis Github Bot (May 26 2020 at 15:53):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (May 26 2020 at 17:39):

CohenCyril updated PR #212 tentative changelog from changelog to master:

I have just copy-pasted information from the commits in master down to circa September 2019, since we started to port on top of MathComp 1.11 in October 2019.

Mathcomp Analysis Github Bot (May 26 2020 at 17:39):

CohenCyril pushed 1 commit to branch changelog.

• swapping stuff (2716696)

Mathcomp Analysis Github Bot (May 26 2020 at 17:40):

CohenCyril merged PR #212 tentative changelog.

Mathcomp Analysis Github Bot (May 26 2020 at 17:40):

CohenCyril pushed 1 commit to branch master. Commits by affeldt-aist (1).

• tentative changelog (#212) (244f131)

Mathcomp Analysis Github Bot (May 26 2020 at 17:55):

affeldt-aist demilestoned Issue #183 LinearContinuousBounded:

Lemmas showing that for functions between normed vector spaces, boundedness and continuity are equivalent.

These lemmas should maybe be rephrased using landau notations.

Mathcomp Analysis Github Bot (May 26 2020 at 17:55):

affeldt-aist milestoned Issue #183 LinearContinuousBounded:

Lemmas showing that for functions between normed vector spaces, boundedness and continuity are equivalent.

These lemmas should maybe be rephrased using landau notations.

Mathcomp Analysis Github Bot (May 26 2020 at 18:20):

affeldt-aist pushed 1 commit to branch master.

• changelog for version 0.3.0 (f3ec99e)

Mathcomp Analysis Github Bot (May 26 2020 at 18:23):

affeldt-aist milestoned Issue #203 Supremums ereal:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (May 26 2020 at 18:23):

affeldt-aist milestoned Issue #197 contributing file:

The goal is to explain good practices that are specific to mathcomp-analysis. Still embryonic.

Mathcomp Analysis Github Bot (May 26 2020 at 18:29):

affeldt-aist milestoned Issue #206 Add a distrLattice canonical structure to set T.

Hi,

This add a canonical distrLattice structure to setT and subset relation.
I have far less experience in adding a canonical structure than I have writing lemma so the PR is likely a bit rough, any guidance is appreciated.

Some comments:

• For some reasons coq fails to unify the type of the lemma setU setI ... when passed as argument to MeetJoinMixin. I added "wrapper lemma" SetOrder_setCI SetOrder_setCU ... to force the type. I'm not sure this is the right thing to do (I could also use @setU (set T) directly in the argument but it would be quite hard to read) and the naming is maybe wrong.
• subset is a Prop while distrLattice expects a rel (ie result type is bool). I wrapped the subset relation in asboolsubset. This means that to use lemma in order (like in my case ltux) one need to map subset and asboolsubset forth and back so I provided subsetE. I don't know if it's the usual idiom.

Mathcomp Analysis Github Bot (May 26 2020 at 18:33):

affeldt-aist released release MathComp Analysis 0.3.0 for tag v0.3.0.

Mathcomp Analysis Github Bot (May 26 2020 at 18:33):

affeldt-aist created release MathComp Analysis 0.3.0 for tag v0.3.0.

Mathcomp Analysis Github Bot (May 26 2020 at 18:33):

affeldt-aist published release MathComp Analysis 0.3.0 for tag v0.3.0.

Mathcomp Analysis Github Bot (May 26 2020 at 18:33):

affeldt-aist pushed tag v0.3.0.

Mathcomp Analysis Github Bot (May 26 2020 at 19:16):

affeldt-aist edited release MathComp Analysis 0.3.0 for tag v0.3.0.

Mathcomp Analysis Github Bot (May 26 2020 at 19:19):

affeldt-aist pushed 1 commit to branch master.

• fixes (e41a840)

Mathcomp Analysis Github Bot (May 26 2020 at 19:23):

affeldt-aist pushed 1 commit to branch how-to-release.

• tentative how-to-release file (245fec7)

Mathcomp Analysis Github Bot (May 26 2020 at 19:25):

affeldt-aist opened PR #213 tentative how-to-release file from how-to-release to master:

This is the same kind of memo as MathComp has for release managers. It might be useful to double-check release steps.

Mathcomp Analysis Github Bot (May 26 2020 at 21:02):

mkerjean pushed 2 commits to branch holomorphy.

• clean (3bdd6ac)
• clean CR -> holo (cdf3fe0)

Mathcomp Analysis Github Bot (May 26 2020 at 21:02):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 27 2020 at 20:55):

mkerjean pushed 1 commit to branch holomorphy.

• WIP Diff_CR_holo with Rcomplex (d02ddf4)

Mathcomp Analysis Github Bot (May 27 2020 at 20:55):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 29 2020 at 11:44):

affeldt-aist pushed 1 commit to branch supremums_ereal.

• add doc and lemmas about supremum (79880f9)

Mathcomp Analysis Github Bot (May 29 2020 at 11:44):

affeldt-aist updated PR #203 Supremums ereal from supremums_ereal to master:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (May 29 2020 at 12:41):

affeldt-aist requested CohenCyril for a review on PR #203 Supremums ereal.

Mathcomp Analysis Github Bot (May 29 2020 at 12:41):

affeldt-aist assigned PR #203 Supremums ereal to affeldt-aist.

Mathcomp Analysis Github Bot (May 29 2020 at 12:59):

affeldt-aist opened Issue #214 locally better be renamed after neighborhoods:

replace locally by nbhs?

exception: bounded_locally in normedmodtype.v

Mathcomp Analysis Github Bot (May 29 2020 at 12:59):

affeldt-aist milestoned Issue #214 locally better be renamed after neighborhoods:

replace locally by nbhs?

exception: bounded_locally in normedmodtype.v

Mathcomp Analysis Github Bot (May 29 2020 at 12:59):

affeldt-aist labeled Issue #214 locally better be renamed after neighborhoods:

replace locally by nbhs?

exception: bounded_locally in normedmodtype.v

Mathcomp Analysis Github Bot (May 29 2020 at 13:44):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• ereals from a pseudometric type (9c5fca6)

Mathcomp Analysis Github Bot (May 29 2020 at 13:44):

affeldt-aist opened PR #215 ereals from a pseudometric type from ereal_pseudometric to master:

warning: proofs to be cleaned

Mathcomp Analysis Github Bot (May 29 2020 at 13:46):

affeldt-aist edited PR #215 ereals from a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
• further developments in this PR may require the merge of PR #203

Mathcomp Analysis Github Bot (May 29 2020 at 14:00):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• divergence in R is convergence to +oo in {ereal R} (c96cd2d)

Mathcomp Analysis Github Bot (May 29 2020 at 14:00):

affeldt-aist updated PR #215 ereals from a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
• further developments in this PR may require the merge of PR #203

Mathcomp Analysis Github Bot (May 29 2020 at 14:01):

affeldt-aist edited PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
• further developments in this PR may require the merge of PR #203

Mathcomp Analysis Github Bot (May 29 2020 at 14:14):

affeldt-aist pushed 5 commits to branch supremums_ereal.

• generalize ub, lb, etc. from reals.v (8dd160b)
• Sets of supremums of extended reals are not empty (d726417)
• trying to control the unfolding of ub (15a5a70)
• rebase sequences.v (2eef8b5)
• add doc and lemmas about supremum (413e0c3)

Mathcomp Analysis Github Bot (May 29 2020 at 14:14):

affeldt-aist updated PR #203 Supremums ereal (assigned to affeldt-aist) from supremums_ereal to master:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (May 29 2020 at 14:15):

affeldt-aist pushed 2 commits to branch ereal_pseudometric.

• ereals from a pseudometric type (2dd8082)
• divergence in R is convergence to +oo in {ereal R} (1c8889a)

Mathcomp Analysis Github Bot (May 29 2020 at 14:15):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
• further developments in this PR may require the merge of PR #203

Mathcomp Analysis Github Bot (May 29 2020 at 14:16):

affeldt-aist edited PR #215 ereals form a pseudometric type from ereal_pseudometric to supremums_ereal:

warning:

• proofs to be cleaned
• further developments in this PR may require the merge of PR #203

Mathcomp Analysis Github Bot (May 29 2020 at 15:32):

CohenCyril submitted PR Review for #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (May 29 2020 at 15:32):

CohenCyril created PR Review Comment on #215 ereals form a pseudometric type:

ereal_locallyE

Mathcomp Analysis Github Bot (May 29 2020 at 15:32):

CohenCyril edited PR Review Comment on #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (May 29 2020 at 16:38):

mkerjean pushed 1 commit to branch holomorphy.

• wip (a1a741b)

Mathcomp Analysis Github Bot (May 29 2020 at 16:38):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 29 2020 at 20:55):

mkerjean pushed 2 commits to branch holomorphy.

• wip (a3cae4f)
• wip (3ef054d)

Mathcomp Analysis Github Bot (May 29 2020 at 20:55):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (May 29 2020 at 22:52):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• the proof of monotony of contract was a bit too long (7a62289)

Mathcomp Analysis Github Bot (May 29 2020 at 22:52):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to supremums_ereal:

warning:

• proofs to be cleaned
• further developments in this PR may require the merge of PR #203

Mathcomp Analysis Github Bot (May 30 2020 at 11:16):

affeldt-aist:

• edited 2020 05 07 Meeting

Mathcomp Analysis Github Bot (May 30 2020 at 17:28):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• the proof of monotony of contract was a bit too long (9d4c2ce)

Mathcomp Analysis Github Bot (May 30 2020 at 17:28):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to supremums_ereal:

warning:

• proofs to be cleaned
• further developments in this PR may require the merge of PR #203

Mathcomp Analysis Github Bot (May 30 2020 at 17:29):

affeldt-aist edited PR #215 ereals form a pseudometric type from ereal_pseudometric to supremums_ereal:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (May 30 2020 at 17:48):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 30 2020 at 17:59):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (May 31 2020 at 00:24):

CohenCyril submitted PR Review for #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (May 31 2020 at 00:24):

CohenCyril created PR Review Comment on #215 ereals form a pseudometric type:

I suggest that this is called contract_inc and that the proof of homo_contract_lt is inlined in it.

Mathcomp Analysis Github Bot (Jun 01 2020 at 14:54):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• a non-decreasing sequence of ereals converges to its sup (99c0887)

Mathcomp Analysis Github Bot (Jun 01 2020 at 14:54):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to supremums_ereal:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (Jun 01 2020 at 20:58):

affeldt-aist pushed 8 commits to branch mathcomp_master_integration_ereal.

• update integral.v w.r.t. PR#270 (0a504fc)
• update integral wrt PR#270 (9ad3541)
• Boole's inequality (wip) (9d506f0)
• minor progress in integral.v (1ffc388)
• turn axioms into hypotheses, add references to technical report (159e1cc)
• any subset of the extended reals has a supremum (cf926a4)
• tentative proof that extended reals from a pseudometric space (b4fd1df)
• measure satisfies generalized Boole's inequality (0d659c0)

Mathcomp Analysis Github Bot (Jun 01 2020 at 20:58):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to master:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 01 2020 at 20:59):

affeldt-aist edited PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 02 2020 at 04:13):

CohenCyril pushed 1 commit to branch ereal_pseudometric.

• exploiting fully the monotonicity of contract and expand (d38d70a)

Mathcomp Analysis Github Bot (Jun 02 2020 at 04:13):

CohenCyril updated PR #215 ereals form a pseudometric type from ereal_pseudometric to supremums_ereal:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (Jun 02 2020 at 04:18):

CohenCyril submitted PR Review for #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (Jun 02 2020 at 04:18):

CohenCyril created PR Review Comment on #215 ereals form a pseudometric type:

Taking this convention would make expand nondecreasing everywhere, making it possible to use some of the homoRL/homoLR lemma where monoRL/monoLR do not apply...

Mathcomp Analysis Github Bot (Jun 02 2020 at 04:19):

CohenCyril edited PR Review Comment on #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (Jun 02 2020 at 08:35):

affeldt-aist pushed 9 commits to branch mathcomp_master_integration_ereal.

• update integral.v w.r.t. PR#270 (1e3fa3f)
• update integral wrt PR#270 (2924e0d)
• Boole's inequality (wip) (c1e3dc0)
• minor progress in integral.v (4adf8e1)
• turn axioms into hypotheses, add references to technical report (ecad671)
• any subset of the extended reals has a supremum (6e3a4d2)
• tentative proof that extended reals from a pseudometric space (7c2f3fd)
• measure satisfies generalized Boole's inequality (996a91d)
• fix (412b8da)

Mathcomp Analysis Github Bot (Jun 02 2020 at 08:35):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 02 2020 at 11:54):

affeldt-aist pushed 1 commit to branch supremums_ereal.

• add changelog information (fb9adc7)

Mathcomp Analysis Github Bot (Jun 02 2020 at 11:54):

affeldt-aist updated PR #203 Supremums ereal (assigned to affeldt-aist) from supremums_ereal to master:

The goal of this PR is to prove that a set of extended reals always has a supremum. For this purpose, I needed to generalize the definition of greatest elements, supremums, etc. from reals.v. I tried for a while to stick to the original pred-base definitions but sets from classical_sets.v turned out to be more handy and simplify proofs a bit.The first commit does the generalization, the second one adds the lemmas about extended reals.

Mathcomp Analysis Github Bot (Jun 02 2020 at 11:55):

mkerjean:

• edited Home

Mathcomp Analysis Github Bot (Jun 03 2020 at 09:16):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• sup of contract is contract of sup (86aa1ce)

Mathcomp Analysis Github Bot (Jun 03 2020 at 09:16):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to supremums_ereal:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (Jun 03 2020 at 09:25):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 03 2020 at 09:35):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 03 2020 at 09:56):

affeldt-aist pushed 1 commit to branch issue103_fix.

• addition to the documentation of landau.v (32387ef)

Mathcomp Analysis Github Bot (Jun 03 2020 at 09:58):

affeldt-aist opened PR #216 Improve documentation of landau.v from issue103_fix to master:

PR intended to fix (at least partially) issue 103.

Mathcomp Analysis Github Bot (Jun 03 2020 at 10:03):

affeldt-aist edited Issue #103 Rework landau's documentation and naming convention:

This is related to #101.

Since we force user to use the equational notations by removing the defintions, we should be very clear on how to use this library. In particular the documentation should:

• [x] detail how to state a lemma using the notations, e.g. should I use f =O_F g or f = [O_F g of h]?

• [ ] list all the possibilities to prove such relations, with the important steps, e.g. apply: eqoE is not to be forgotten, filter reasoning is possible but thought of as a last resort…

• [ ] clarify anything that can confuse the user about the notations, e.g.:

  • [ ] what is the difference between f =o_F g and f = o_F g?
  • [x] why does f =O_ (0 : U) g work but not f =O_(0 : U) g, while f =O_F g does work?

• [ ] what are the naming conventions. I believe this library should be used as bigop: since it is hard and tedious to search lemmas using notations, we should have a clear naming convention so that it is easy to find a lemma by its name.

Mathcomp Analysis Github Bot (Jun 03 2020 at 10:04):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 03 2020 at 10:05):

affeldt-aist edited Issue #103 Rework landau's documentation and naming convention:

This is related to #101. [NB(rei): PR which has been merged]

Since we force user to use the equational notations by removing the defintions, we should be very clear on how to use this library. In particular the documentation should:

• [x] detail how to state a lemma using the notations, e.g. should I use f =O_F g or f = [O_F g of h]?

• [ ] list all the possibilities to prove such relations, with the important steps, e.g. apply: eqoE is not to be forgotten, filter reasoning is possible but thought of as a last resort…

• [ ] clarify anything that can confuse the user about the notations, e.g.:

  • [ ] what is the difference between f =o_F g and f = o_F g?
  • [x] why does f =O_ (0 : U) g work but not f =O_(0 : U) g, while f =O_F g does work?

• [ ] what are the naming conventions. I believe this library should be used as bigop: since it is hard and tedious to search lemmas using notations, we should have a clear naming convention so that it is easy to find a lemma by its name.

Mathcomp Analysis Github Bot (Jun 03 2020 at 10:29):

CohenCyril closed Issue #67 Put littleo_linear0 in 0 (assigned to affeldt-aist):

https://github.com/math-comp/analysis/blob/b6aa8eb636dee230ecb29b836fa8ff1eca55a513/derive.v#L320

As it is, this theorem is seldom rewritable from left to right, I'd rather have this theorem with x = 0 and provide lemmas to bring any o_x to o_0 instead.

Mathcomp Analysis Github Bot (Jun 03 2020 at 10:41):

CohenCyril merged PR #203 Supremums ereal.

Mathcomp Analysis Github Bot (Jun 03 2020 at 10:41):

CohenCyril pushed 7 commits to branch master. Commits by affeldt-aist (6) and CohenCyril (1).

• generalize ub, lb, etc. from reals.v (8dd160b)
• Sets of supremums of extended reals are not empty (d726417)
• trying to control the unfolding of ub (15a5a70)
• rebase sequences.v (2eef8b5)
• add doc and lemmas about supremum (413e0c3)
• add changelog information (fb9adc7)
• Merge pull request #203 from math-comp/supremums_ereal (d2d010f)

Mathcomp Analysis Github Bot (Jun 03 2020 at 11:05):

affeldt-aist pushed 6 commits to branch ereal_pseudometric. Commits by affeldt-aist (5) and CohenCyril (1).

• ereals from a pseudometric type (79b5859)
• divergence in R is convergence to +oo in {ereal R} (289c8db)
• the proof of monotony of contract was a bit too long (52e7c4e)
• a non-decreasing sequence of ereals converges to its sup (7e90d3c)
• exploiting fully the monotonicity of contract and expand (33ddb2c)
• sup of contract is contract of sup (572d272)

Mathcomp Analysis Github Bot (Jun 03 2020 at 11:05):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to supremums_ereal:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (Jun 03 2020 at 11:05):

affeldt-aist edited PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (Jun 03 2020 at 11:07):

affeldt-aist pushed 9 commits to branch mathcomp_master_integration_ereal.

• update integral.v w.r.t. PR#270 (a4b14b1)
• update integral wrt PR#270 (bc110f5)
• Boole's inequality (wip) (0794a6f)
• minor progress in integral.v (928c7e8)
• turn axioms into hypotheses, add references to technical report (e25a0e8)
• any subset of the extended reals has a supremum (b0e88fa)
• tentative proof that extended reals from a pseudometric space (7af07cb)
• measure satisfies generalized Boole's inequality (cee900d)
• fix (bbcff2e)

Mathcomp Analysis Github Bot (Jun 03 2020 at 11:07):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 03 2020 at 12:11):

affeldt-aist deleted the branch analysis_270_hahnbanach.

Mathcomp Analysis Github Bot (Jun 03 2020 at 13:40):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• renaming (5e5a8e5)

Mathcomp Analysis Github Bot (Jun 03 2020 at 13:40):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 03 2020 at 17:09):

affeldt-aist opened Issue #217 Rename existsP:

https://github.com/math-comp/analysis/blob/d2d010f71587ac48338213e3c7e652351baac503/theories/boolp.v#L564

Naming conflicts with fintype.existsP; the same for forallP.

Mathcomp Analysis Github Bot (Jun 03 2020 at 17:09):

affeldt-aist labeled Issue #217 Rename existsP:

https://github.com/math-comp/analysis/blob/d2d010f71587ac48338213e3c7e652351baac503/theories/boolp.v#L564

Naming conflicts with fintype.existsP; the same for forallP.

Mathcomp Analysis Github Bot (Jun 04 2020 at 16:58):

CohenCyril pushed 1 commit to branch maxr.

• Adapting to new Order.max (b82fa34)

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:00):

CohenCyril opened PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:19):

affeldt-aist pushed tag 0.3.0.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:19):

CohenCyril edited release MathComp Analysis 0.3.0 for tag 0.3.0.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:21):

CohenCyril removed tag 0.3.0.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:21):

ghost unpublished release MathComp Analysis 0.3.0 for tag 0.3.0.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:22):

CohenCyril published release MathComp Analysis 0.3.0 for tag v0.3.0.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:22):

CohenCyril released release MathComp Analysis 0.3.0 for tag v0.3.0.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:23):

CohenCyril pushed tag 0.3.0.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:35):

CohenCyril updated PR #213 tentative how-to-release file from how-to-release to master:

This is the same kind of memo as MathComp has for release managers. It might be useful to double-check release steps.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:35):

CohenCyril pushed 1 commit to branch how-to-release.

• fix version naming (b264352)

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:36):

CohenCyril updated PR #213 tentative how-to-release file from how-to-release to master:

This is the same kind of memo as MathComp has for release managers. It might be useful to double-check release steps.

Mathcomp Analysis Github Bot (Jun 04 2020 at 17:36):

CohenCyril pushed 1 commit to branch how-to-release.

• fixup (ff2b7d2)

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:14):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• add !=- -oo hypo and propagate (wip) (b27bc5b)

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:14):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:16):

affeldt-aist deleted the branch changelog.

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:20):

affeldt-aist deleted the branch entourages_bigmax.

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:32):

affeldt-aist deleted the branch analysis_270_numFieldType.

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:32):

CohenCyril updated PR #213 tentative how-to-release file from how-to-release to master:

This is the same kind of memo as MathComp has for release managers. It might be useful to double-check release steps.

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:32):

CohenCyril pushed 1 commit to branch how-to-release.

• Update HOWTORELEASE.md (a0d0a51)

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:35):

affeldt-aist pushed 1 commit to branch how-to-release.

• fix (29dfcba)

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:35):

affeldt-aist updated PR #213 tentative how-to-release file from how-to-release to master:

This is the same kind of memo as MathComp has for release managers. It might be useful to double-check release steps.

Mathcomp Analysis Github Bot (Jun 04 2020 at 22:42):

affeldt-aist deleted the branch supremums_ereal.

Mathcomp Analysis Github Bot (Jun 05 2020 at 09:40):

affeldt-aist:

• created HOWTORELEASE

Mathcomp Analysis Github Bot (Jun 05 2020 at 09:41):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 05 2020 at 14:09):

affeldt-aist pushed 1 commit to branch fix_issue_217.

• rename lemmas for classical reasoning to avoid clash with fintype (b16ec63)

Mathcomp Analysis Github Bot (Jun 05 2020 at 14:10):

affeldt-aist opened PR #219 rename lemmas for classical reasoning to avoid clash with fintype from fix_issue_217 to master:

fixes #217

Mathcomp Analysis Github Bot (Jun 05 2020 at 14:58):

affeldt-aist pushed 1 commit to branch ub_lb_renaming.

• rename the short ub and lb to ubound and lbound (08d32bd)

Mathcomp Analysis Github Bot (Jun 05 2020 at 14:59):

affeldt-aist opened PR #220 rename the short ub and lb to ubound and lbound from ub_lb_renaming to master:

I have understood that it can be argued that ub and lb are too short identifiers. What about this renaming? @CohenCyril

Mathcomp Analysis Github Bot (Jun 05 2020 at 15:07):

CohenCyril closed Issue #217 Rename existsP:

https://github.com/math-comp/analysis/blob/d2d010f71587ac48338213e3c7e652351baac503/theories/boolp.v#L564

Naming conflicts with fintype.existsP; the same for forallP.

Mathcomp Analysis Github Bot (Jun 05 2020 at 15:07):

CohenCyril merged PR #219 rename lemmas for classical reasoning to avoid clash with fintype.

Mathcomp Analysis Github Bot (Jun 05 2020 at 15:07):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and affeldt-aist (1).

• rename lemmas for classical reasoning to avoid clash with fintype (b16ec63)
• Merge pull request #219 from math-comp/fix_issue_217 (955e621)

Mathcomp Analysis Github Bot (Jun 05 2020 at 15:30):

affeldt-aist pushed the branch update_installmd.

Mathcomp Analysis Github Bot (Jun 05 2020 at 15:31):

affeldt-aist pushed 1 commit to branch update_installmd.

• update to last version (c347ce1)

Mathcomp Analysis Github Bot (Jun 05 2020 at 15:32):

affeldt-aist opened PR #221 update to last version from update_installmd to master:

@mkerjean observed the INSTALL.md was a bit outdated.

Mathcomp Analysis Github Bot (Jun 05 2020 at 15:39):

affeldt-aist pushed 1 commit to branch update_installmd.

• update to last version (64d8345)

Mathcomp Analysis Github Bot (Jun 05 2020 at 15:39):

affeldt-aist updated PR #221 update to last version from update_installmd to master:

@mkerjean observed the INSTALL.md was a bit outdated.

Mathcomp Analysis Github Bot (Jun 05 2020 at 16:22):

affeldt-aist deleted the branch fix_issue_217.

Mathcomp Analysis Github Bot (Jun 05 2020 at 17:17):

affeldt-aist merged PR #221 update to last version.

Mathcomp Analysis Github Bot (Jun 05 2020 at 17:17):

affeldt-aist pushed 1 commit to branch master.

• update to last version (9773dc1)

Mathcomp Analysis Github Bot (Jun 05 2020 at 21:09):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• use the predicate measurable instead of != -oo%E (7359bd7)

Mathcomp Analysis Github Bot (Jun 05 2020 at 21:09):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 05 2020 at 21:23):

CohenCyril submitted PR Review for #189 Mathcomp master integration ereal.

Mathcomp Analysis Github Bot (Jun 05 2020 at 21:23):

CohenCyril submitted PR Review for #189 Mathcomp master integration ereal.

Mathcomp Analysis Github Bot (Jun 05 2020 at 21:23):

CohenCyril created PR Review Comment on #189 Mathcomp master integration ereal:

@affeldt-aist you need to allow countable unions (or intersection).

Mathcomp Analysis Github Bot (Jun 05 2020 at 21:23):

CohenCyril created PR Review Comment on #189 Mathcomp master integration ereal:

This is redundant because stability by union, complement and setT => stability by intersection

Mathcomp Analysis Github Bot (Jun 05 2020 at 22:31):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• cleaning (ada2736)

Mathcomp Analysis Github Bot (Jun 05 2020 at 22:31):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 05 2020 at 22:34):

affeldt-aist deleted the branch update_installmd.

Mathcomp Analysis Github Bot (Jun 05 2020 at 22:48):

affeldt-aist pushed 1 commit to branch ereal_ninfty_arithmetic.

• two lemmas about arithmetic with ninfty + typos in the documentation (15e5cb4)

Mathcomp Analysis Github Bot (Jun 05 2020 at 22:49):

affeldt-aist opened PR #222 two lemmas about arithmetic with ninfty + typos in the documentation from ereal_ninfty_arithmetic to master:

Again a micro addition to ereal.v.

Mathcomp Analysis Github Bot (Jun 05 2020 at 23:12):

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

• remove redundant lemmas, move ereal lemmas to another PR, add an easy (f57cbf5)

Mathcomp Analysis Github Bot (Jun 05 2020 at 23:13):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 05 2020 at 23:37):

affeldt-aist pushed 1 commit to branch ub_lb_renaming.

• rename the short ub and lb to ubound and lbound (a0a2a6c)

Mathcomp Analysis Github Bot (Jun 05 2020 at 23:37):

affeldt-aist updated PR #220 rename the short ub and lb to ubound and lbound from ub_lb_renaming to master:

I have understood that it can be argued that ub and lb are too short identifiers. What about this renaming? @CohenCyril

Mathcomp Analysis Github Bot (Jun 06 2020 at 10:16):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 06 2020 at 10:18):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 07 2020 at 01:47):

CohenCyril closed without merge PR #213 tentative how-to-release file.

Mathcomp Analysis Github Bot (Jun 08 2020 at 23:47):

affeldt-aist pushed 5 commits to branch ereal_pseudometric. Commits by affeldt-aist (4) and CohenCyril (1).

• ereals from a pseudometric type (4b3281e)
• divergence in R is convergence to +oo in {ereal R} (6e7ad00)
• a non-decreasing sequence of ereals converges to its sup (021e7a1)
• exploiting fully the monotonicity of contract and expand (25d8408)
• sup (resp. inf) of contract is contract of sup (resp. inf) (ae0f332)

Mathcomp Analysis Github Bot (Jun 08 2020 at 23:47):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (Jun 08 2020 at 23:52):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• sup (resp. inf) of contract is contract of sup (resp. inf) (ff2de7d)

Mathcomp Analysis Github Bot (Jun 08 2020 at 23:52):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (Jun 08 2020 at 23:52):

affeldt-aist milestoned Issue #215 ereals form a pseudometric type:

warning:

• proofs to be cleaned
• PR based on PR #203

Mathcomp Analysis Github Bot (Jun 08 2020 at 23:53):

affeldt-aist edited PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
  - PR based on PR #203 (has been merged)

Mathcomp Analysis Github Bot (Jun 08 2020 at 23:53):

affeldt-aist has marked PR #215 as ready for review.

Mathcomp Analysis Github Bot (Jun 09 2020 at 01:01):

affeldt-aist pushed 3 commits to branch mathcomp_master_integration_ereal.

• add integral.v file (dfe5877)
• minor progress in integral.v (98b7694)
• add measure.v file (8de8cb7)

Mathcomp Analysis Github Bot (Jun 09 2020 at 01:01):

affeldt-aist updated PR #189 Mathcomp master integration ereal from mathcomp_master_integration_ereal to ereal_pseudometric:

work in progress, supersedes PR #137

Mathcomp Analysis Github Bot (Jun 09 2020 at 02:47):

CohenCyril submitted PR Review for #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (Jun 09 2020 at 02:47):

CohenCyril created PR Review Comment on #215 ereals form a pseudometric type:

@affeldt-aist you should document expand as well.

Mathcomp Analysis Github Bot (Jun 09 2020 at 02:48):

CohenCyril submitted PR Review for #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (Jun 09 2020 at 02:48):

CohenCyril created PR Review Comment on #215 ereals form a pseudometric type:

remove the comment or replace it by added in mathcomp-1.11.0 ssrnum as ...

Mathcomp Analysis Github Bot (Jun 09 2020 at 02:49):

CohenCyril submitted PR Review for #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (Jun 09 2020 at 02:49):

CohenCyril created PR Review Comment on #215 ereals form a pseudometric type:

why?

Mathcomp Analysis Github Bot (Jun 09 2020 at 09:37):

affeldt-aist edited PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
  - PR based on PR #203 (has been merged into master)

Mathcomp Analysis Github Bot (Jun 09 2020 at 09:51):

affeldt-aist submitted PR Review for #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (Jun 09 2020 at 09:51):

affeldt-aist created PR Review Comment on #215 ereals form a pseudometric type:

So that it type-checks in Lemma nondecreasing_seq_ereal_cvg.

Mathcomp Analysis Github Bot (Jun 09 2020 at 10:01):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• fix (bcf7815)

Mathcomp Analysis Github Bot (Jun 09 2020 at 10:01):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
  - PR based on PR #203 (has been merged into master)

Mathcomp Analysis Github Bot (Jun 09 2020 at 22:52):

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

• minor fixes (861a90d)

Mathcomp Analysis Github Bot (Jun 09 2020 at 22:52):

affeldt-aist updated PR #215 ereals form a pseudometric type from ereal_pseudometric to master:

warning:

• proofs to be cleaned
  - PR based on PR #203 (has been merged into master)

Mathcomp Analysis Github Bot (Jun 09 2020 at 23:30):

affeldt-aist pushed 1 commit to branch boole_inequality.

• tentative proof of Boole's inequality (224ca9d)

Mathcomp Analysis Github Bot (Jun 09 2020 at 23:31):

affeldt-aist opened PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 09 2020 at 23:31):

affeldt-aist edited PR #223 Boole inequality from boole_inequality to ereal_pseudometric:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 09 2020 at 23:33):

affeldt-aist pushed 1 commit to branch integral_sketch.

• integral.v file written with all members during mathcomp-analysis-dev meeting (2ac4f21)

Mathcomp Analysis Github Bot (Jun 09 2020 at 23:33):

affeldt-aist opened PR #224 Integral sketch from integral_sketch to master.

Mathcomp Analysis Github Bot (Jun 09 2020 at 23:33):

affeldt-aist edited PR #224 Integral sketch from integral_sketch to boole_inequality.

Mathcomp Analysis Github Bot (Jun 09 2020 at 23:44):

affeldt-aist deleted the branch renamings.

Mathcomp Analysis Github Bot (Jun 10 2020 at 13:27):

CohenCyril closed without merge PR #189 Mathcomp master integration ereal.

Mathcomp Analysis Github Bot (Jun 10 2020 at 13:32):

affeldt-aist pushed the branch update_installmd_1.11.

Mathcomp Analysis Github Bot (Jun 10 2020 at 13:34):

affeldt-aist pushed 1 commit to branch update_installmd_1.11.

• update INSTALL.md now that 1.11.0 has been released (4177146)

Mathcomp Analysis Github Bot (Jun 10 2020 at 13:34):

affeldt-aist opened PR #225 update INSTALL.md now that 1.11.0 has been released from update_installmd_1.11 to master.

Mathcomp Analysis Github Bot (Jun 10 2020 at 13:44):

CohenCyril submitted PR Review for #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (Jun 10 2020 at 13:46):

CohenCyril merged PR #215 ereals form a pseudometric type.

Mathcomp Analysis Github Bot (Jun 10 2020 at 13:46):

CohenCyril pushed 7 commits to branch master. Commits by affeldt-aist (5) and CohenCyril (2).

• ereals from a pseudometric type (4b3281e)
• divergence in R is convergence to +oo in {ereal R} (6e7ad00)
• a non-decreasing sequence of ereals converges to its sup (021e7a1)
• exploiting fully the monotonicity of contract and expand (25d8408)
• sup (resp. inf) of contract is contract of sup (resp. inf) (ff2de7d)
• minor fixes (861a90d)
• Merge pull request #215 from math-comp/ereal_pseudometric (5c8f6d8)

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:06):

CohenCyril pushed 1 commit to branch renaming_le_expand.

• Small renamings about expand. (ccbc1a3)

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:06):

CohenCyril opened PR #226 Small renamings about expand from renaming_le_expand to master:

• partial strict monotonicity le_expand is renamed le_expand_in
• reattribute le_expand to total large monotonicity (and simplify proof)
• remove (le|lt)_contract(LR|RL) which were redundant with the symmetric of (le|lt)_expand(LR|RL)

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:06):

affeldt-aist pushed 1 commit to branch maxr.

• remove kludge for finamp from travis.yml (4bbd259)

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:06):

affeldt-aist updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:09):

CohenCyril updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:09):

CohenCyril pushed 1 commit to branch maxr.

• Update config.nix (83bf207)

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:12):

CohenCyril edited PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:12):

CohenCyril deleted the branch ereal_pseudometric.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:12):

CohenCyril deleted the branch mathcomp_master_integration_ereal.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:22):

affeldt-aist pushed 1 commit to branch maxr.

• fix suggested by erik (46ea01c)

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:22):

affeldt-aist updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:35):

CohenCyril edited PR #224 Integral sketch from integral_sketch to boole_inequality:

Depends on #223 (EDIT by Cyril)

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:36):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:36):

CohenCyril created PR Review Comment on #223 Boole inequality:

Unused

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:39):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:39):

CohenCyril created PR Review Comment on #223 Boole inequality:

It's better to have Record mixin_of := and then Notation class_of := mixin_of to maintain the invariant that every structure has both a mixin and a class, although it looks a bit cosmetic.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:40):

CohenCyril edited PR Review Comment on #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:59):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:59):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:59):

CohenCyril created PR Review Comment on #223 Boole inequality:

I would prefer is_sigma_algebra.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:59):

CohenCyril created PR Review Comment on #223 Boole inequality:

rename le_measure

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:59):

CohenCyril created PR Review Comment on #223 Boole inequality:

and Notation MesurableMixin := Mixin.

Mathcomp Analysis Github Bot (Jun 10 2020 at 14:59):

CohenCyril created PR Review Comment on #223 Boole inequality:

Using exact: is dangerous as a hint with priority 0 in core. I guess there is no other choice right now because is_measure0 leaves a goal is_measure _ unsolved, but this is because we miss a canonical structure

Module measure.
Record axioms ... (* ranaming of is_measure *)
...
Structure map := { apply :> X -> {ereal R}; _: axioms apply};
...
End measure.
...

cf https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/ssralg.v#L1793-L1824

Mathcomp Analysis Github Bot (Jun 10 2020 at 15:02):

affeldt-aist pushed 1 commit to branch update_installmd_1.11.

• remove technical explanations about betas (4f39f26)

Mathcomp Analysis Github Bot (Jun 10 2020 at 15:02):

affeldt-aist updated PR #225 update INSTALL.md now that 1.11.0 has been released from update_installmd_1.11 to master.

Mathcomp Analysis Github Bot (Jun 10 2020 at 15:29):

affeldt-aist pushed 2 commits to branch maxr. Commits by CohenCyril (1) and affeldt-aist (1).

• Update config.nix (486f26e)
• fix suggested by erik (7f4b92e)

Mathcomp Analysis Github Bot (Jun 10 2020 at 15:29):

affeldt-aist updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 10 2020 at 15:39):

affeldt-aist pushed 1 commit to branch maxr.

• fix suggested by erik (701e73e)

Mathcomp Analysis Github Bot (Jun 10 2020 at 15:39):

affeldt-aist updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 10 2020 at 17:11):

CohenCyril merged PR #226 Small renamings about expand.

Mathcomp Analysis Github Bot (Jun 10 2020 at 17:11):

CohenCyril pushed 2 commits to branch master.

• Small renamings about expand. (ccbc1a3)
• Merge pull request #226 from math-comp/renaming_le_expand (96a5493)

Mathcomp Analysis Github Bot (Jun 10 2020 at 17:11):

CohenCyril deleted the branch renaming_le_expand.

Mathcomp Analysis Github Bot (Jun 10 2020 at 23:25):

CohenCyril updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 10 2020 at 23:25):

CohenCyril pushed 1 commit to branch maxr.

• Update .travis.yml (24e46c1)

Mathcomp Analysis Github Bot (Jun 10 2020 at 23:26):

CohenCyril updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 10 2020 at 23:26):

CohenCyril pushed 1 commit to branch maxr.

• Update config.nix (e3af28e)

Mathcomp Analysis Github Bot (Jun 10 2020 at 23:27):

CohenCyril pushed 5 commits to branch maxr. Commits by CohenCyril (4) and affeldt-aist (1).

• Adapting to new Order.max (b719d35)
• Update config.nix (8a32b30)
• fix suggested by erik (285cce0)
• Update .travis.yml (ca6cecb)
• Update config.nix (a88d7ff)

Mathcomp Analysis Github Bot (Jun 10 2020 at 23:27):

CohenCyril updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 10 2020 at 23:42):

CohenCyril pushed 1 commit to branch maxr.

• Adapting to new Order.max (e562b94)

Mathcomp Analysis Github Bot (Jun 10 2020 at 23:42):

CohenCyril updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 11 2020 at 00:08):

CohenCyril pushed 1 commit to branch maxr.

• Adapting to new Order.max (f30323e)

Mathcomp Analysis Github Bot (Jun 11 2020 at 00:08):

CohenCyril updated PR #218 Adapting to new Order.max from maxr to master:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 11 2020 at 00:17):

CohenCyril merged PR #218 Adapting to new Order.max.

Mathcomp Analysis Github Bot (Jun 11 2020 at 00:17):

CohenCyril pushed 2 commits to branch master.

• Adapting to new Order.max (f30323e)
• Merge pull request #218 from math-comp/maxr (a1e6ba9)

Mathcomp Analysis Github Bot (Jun 11 2020 at 00:19):

CohenCyril deleted the branch maxr.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:04):

CohenCyril updated PR #225 update INSTALL.md now that 1.11.0 has been released from update_installmd_1.11 to master.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:04):

CohenCyril pushed 1 commit to branch update_installmd_1.11.

• Update INSTALL.md (5c11fdc)

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:04):

CohenCyril has marked PR #225 as ready for review.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:04):

CohenCyril merged PR #225 update INSTALL.md now that 1.11.0 has been released.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:04):

CohenCyril pushed 4 commits to branch master. Commits by CohenCyril (2) and affeldt-aist (2).

• update INSTALL.md now that 1.11.0 has been released (4177146)
• remove technical explanations about betas (4f39f26)
• Update INSTALL.md (5c11fdc)
• Merge pull request #225 from math-comp/update_installmd_1.11 (3016b45)

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:05):

CohenCyril edited release MathComp Analysis 0.3.0 for tag 0.3.0.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:05):

CohenCyril released release MathComp Analysis 0.3.0 for tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:05):

CohenCyril created release MathComp Analysis 0.3.0 for tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:05):

CohenCyril published release MathComp Analysis 0.3.0 for tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:05):

CohenCyril pushed tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:05):

CohenCyril deleted release MathComp Analysis 0.3.0 for tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:06):

CohenCyril removed tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:09):

CohenCyril pushed 1 commit to branch changelog.

• preparing changelog (a37d394)

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:09):

CohenCyril opened PR #227 preparing changelog from changelog to master.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:10):

CohenCyril updated PR #227 preparing changelog from changelog to master.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:10):

CohenCyril pushed 1 commit to branch changelog.

• fixup (d9923c2)

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:11):

CohenCyril merged PR #227 preparing changelog.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:11):

CohenCyril pushed 1 commit to branch master.

• preparing changelog (#227) (c1ee376)

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:12):

CohenCyril milestoned Issue #227 preparing changelog.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:12):

CohenCyril milestoned Issue #226 Small renamings about expand:

• partial strict monotonicity le_expand is renamed le_expand_in
• reattribute le_expand to total large monotonicity (and simplify proof)
• remove (le|lt)_contract(LR|RL) which were redundant with the symmetric of (le|lt)_expand(LR|RL)

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:12):

CohenCyril milestoned Issue #225 update INSTALL.md now that 1.11.0 has been released.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:12):

CohenCyril milestoned Issue #221 update to last version:

@mkerjean observed the INSTALL.md was a bit outdated.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:12):

CohenCyril milestoned Issue #219 rename lemmas for classical reasoning to avoid clash with fintype:

fixes #217

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:12):

CohenCyril milestoned Issue #218 Adapting to new Order.max:

Patch for math-comp/math-comp#516

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:12):

CohenCyril milestoned Issue #212 tentative changelog:

I have just copy-pasted information from the commits in master down to circa September 2019, since we started to port on top of MathComp 1.11 in October 2019.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:12):

CohenCyril milestoned Issue #211 updating config.nix.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:13):

CohenCyril milestoned Issue #210 upgrading default.nix.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:15):

CohenCyril milestoned Issue #208 a few lemmas about extended reals' arithmetic:

Just a couple of easy lemmas that I missed during some work on another PR.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:15):

CohenCyril demilestoned Issue #206 Add a distrLattice canonical structure to set T.

Hi,

This add a canonical distrLattice structure to setT and subset relation.
I have far less experience in adding a canonical structure than I have writing lemma so the PR is likely a bit rough, any guidance is appreciated.

Some comments:

• For some reasons coq fails to unify the type of the lemma setU setI ... when passed as argument to MeetJoinMixin. I added "wrapper lemma" SetOrder_setCI SetOrder_setCU ... to force the type. I'm not sure this is the right thing to do (I could also use @setU (set T) directly in the argument but it would be quite hard to read) and the naming is maybe wrong.
• subset is a Prop while distrLattice expects a rel (ie result type is bool). I wrapped the subset relation in asboolsubset. This means that to use lemma in order (like in my case ltux) one need to map subset and asboolsubset forth and back so I provided subsetE. I don't know if it's the usual idiom.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:15):

CohenCyril milestoned Issue #206 Add a distrLattice canonical structure to set T.

Hi,

This add a canonical distrLattice structure to setT and subset relation.
I have far less experience in adding a canonical structure than I have writing lemma so the PR is likely a bit rough, any guidance is appreciated.

Some comments:

• For some reasons coq fails to unify the type of the lemma setU setI ... when passed as argument to MeetJoinMixin. I added "wrapper lemma" SetOrder_setCI SetOrder_setCU ... to force the type. I'm not sure this is the right thing to do (I could also use @setU (set T) directly in the argument but it would be quite hard to read) and the naming is maybe wrong.
• subset is a Prop while distrLattice expects a rel (ie result type is bool). I wrapped the subset relation in asboolsubset. This means that to use lemma in order (like in my case ltux) one need to map subset and asboolsubset forth and back so I provided subsetE. I don't know if it's the usual idiom.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:16):

CohenCyril demilestoned Issue #183 LinearContinuousBounded:

Lemmas showing that for functions between normed vector spaces, boundedness and continuity are equivalent.

These lemmas should maybe be rephrased using landau notations.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:16):

CohenCyril milestoned Issue #183 LinearContinuousBounded:

Lemmas showing that for functions between normed vector spaces, boundedness and continuity are equivalent.

These lemmas should maybe be rephrased using landau notations.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:16):

CohenCyril demilestoned Issue #197 contributing file:

The goal is to explain good practices that are specific to mathcomp-analysis. Still embryonic.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:16):

CohenCyril milestoned Issue #197 contributing file:

The goal is to explain good practices that are specific to mathcomp-analysis. Still embryonic.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:16):

CohenCyril demilestoned Issue #214 locally better be renamed after neighborhoods:

replace locally by nbhs?

exception: bounded_locally in normedmodtype.v

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:16):

CohenCyril milestoned Issue #214 locally better be renamed after neighborhoods:

replace locally by nbhs?

exception: bounded_locally in normedmodtype.v

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:17):

CohenCyril demilestoned Issue #2 Fix 'the_* landau notation to improve readability:

• Make the notation f = g +o_e stable (e.g. by putting a definition)
  https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L199

• Remove the "'the" tag which makes things unreadable
  https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L135
  ...

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:17):

CohenCyril milestoned Issue #2 Fix 'the_* landau notation to improve readability:

• Make the notation f = g +o_e stable (e.g. by putting a definition)
  https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L199

• Remove the "'the" tag which makes things unreadable
  https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L135
  ...

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:17):

CohenCyril demilestoned Issue #7 Remove this lemma about derivative and replace. (assigned to affeldt-aist):

https://github.com/math-comp/analysis/blob/e2d3d4c57f3c0797d06891669c336ba587eb2ae5/derive.v#L135

'd_a f x / x although valid is a non canonical way for getting the coefficient of a linear map (no need to take a limit by the way, it is supposed to be constant). The canonical way is to first take the Jacobian (using lin1_mx) and in dimension 1 (since R^o is), just take the only coefficient: jacobian f 0 0.

derivative1 f a = 'J_a f 0 0

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:17):

CohenCyril milestoned Issue #7 Remove this lemma about derivative and replace. (assigned to affeldt-aist):

https://github.com/math-comp/analysis/blob/e2d3d4c57f3c0797d06891669c336ba587eb2ae5/derive.v#L135

'd_a f x / x although valid is a non canonical way for getting the coefficient of a linear map (no need to take a limit by the way, it is supposed to be constant). The canonical way is to first take the Jacobian (using lin1_mx) and in dimension 1 (since R^o is), just take the only coefficient: jacobian f 0 0.

derivative1 f a = 'J_a f 0 0

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:23):

CohenCyril released release MathComp Analysis 0.3.1 for tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:23):

CohenCyril created release MathComp Analysis 0.3.1 for tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:23):

CohenCyril published release MathComp Analysis 0.3.1 for tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 03:23):

CohenCyril pushed tag 0.3.1.

Mathcomp Analysis Github Bot (Jun 11 2020 at 09:34):

affeldt-aist pushed 1 commit to branch ereal_ninfty_arithmetic.

• two lemmas about arithmetic with ninfty + typos in the documentation (dde0ca4)

Mathcomp Analysis Github Bot (Jun 11 2020 at 09:34):

affeldt-aist updated PR #222 two lemmas about arithmetic with ninfty + typos in the documentation from ereal_ninfty_arithmetic to master:

Again a micro addition to ereal.v.

Mathcomp Analysis Github Bot (Jun 11 2020 at 14:16):

affeldt-aist pushed 2 commits to branch boole_inequality.

• tentative proof of Boole's inequality (e038a87)
• fixes following comments by Cyril (5c88acb)

Mathcomp Analysis Github Bot (Jun 11 2020 at 14:16):

affeldt-aist updated PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 11 2020 at 14:40):

CohenCyril submitted PR Review for #222 two lemmas about arithmetic with ninfty + typos in the documentation.

Mathcomp Analysis Github Bot (Jun 11 2020 at 14:40):

CohenCyril merged PR #222 two lemmas about arithmetic with ninfty + typos in the documentation.

Mathcomp Analysis Github Bot (Jun 11 2020 at 14:40):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and affeldt-aist (1).

• two lemmas about arithmetic with ninfty + typos in the documentation (dde0ca4)
• Merge pull request #222 from math-comp/ereal_ninfty_arithmetic (f5324c0)

Mathcomp Analysis Github Bot (Jun 11 2020 at 14:41):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 11 2020 at 14:44):

affeldt-aist pushed 1 commit to branch ub_lb_renaming.

• rename the short ub and lb to ubound and lbound (b8414e4)

Mathcomp Analysis Github Bot (Jun 11 2020 at 14:44):

affeldt-aist updated PR #220 rename the short ub and lb to ubound and lbound from ub_lb_renaming to master:

I have understood that it can be argued that ub and lb are too short identifiers. What about this renaming? @CohenCyril

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:35):

affeldt-aist pushed 2 commits to branch more_sequences.

• Examples of sequences and series (4ff0439)
• rebasing (4cd6ba8)

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:35):

affeldt-aist updated PR #207 more lemmas about sequences from more_sequences to mathcomp_master_sequences:

This PR is the result of a split of the PR #187 .
It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for sequences.v.

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:35):

affeldt-aist edited PR #207 more lemmas about sequences from more_sequences to master:

This PR is the result of a split of the PR #187 .
It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for sequences.v.

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:41):

affeldt-aist pushed 4 commits to branch contributing_guide.

• start a contributing file (wip) (eee738a)
• add link to mathcomp's contribution guide (3678ba2)
• add a comment about near tactics vs. filter lemmas (a4a7d00)
• move comment about PR from readme.md to contributing.md (df6a140)

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:41):

affeldt-aist updated PR #197 contributing file from contributing_guide to master:

The goal is to explain good practices that are specific to mathcomp-analysis. Still embryonic.

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:43):

affeldt-aist deleted the branch ereal_ninfty_arithmetic.

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:44):

affeldt-aist deleted the branch update_installmd_1.11.

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:44):

affeldt-aist deleted the branch how-to-release.

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:44):

affeldt-aist deleted the branch mathcomp_master_sequences.

Mathcomp Analysis Github Bot (Jun 11 2020 at 15:44):

affeldt-aist deleted the branch changelog.

Mathcomp Analysis Github Bot (Jun 11 2020 at 20:58):

affeldt-aist pushed 4 commits to branch boole_inequality.

• tentative proof of Boole's inequality (c29e3f5)
• fixes following comments by Cyril (9e30843)
• technical lemmas about ereal and minor generalization (4901c30)
• wip (8a0f507)

Mathcomp Analysis Github Bot (Jun 11 2020 at 20:58):

affeldt-aist updated PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 11 2020 at 21:14):

CohenCyril created PR Review Comment on #223 Boole inequality:

Maybe Theorem Boole_inequality instead. Otherwise by convention bool means bool : Type

Mathcomp Analysis Github Bot (Jun 11 2020 at 21:14):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 11 2020 at 21:30):

affeldt-aist pushed 4 commits to branch boole_inequality.

• tentative proof of Boole's inequality (2d78495)
• fixes following comments by Cyril (b4a6cad)
• technical lemmas about ereal and minor generalization (39a037c)
• wip (ddb134b)

Mathcomp Analysis Github Bot (Jun 11 2020 at 21:30):

affeldt-aist updated PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 11 2020 at 21:34):

affeldt-aist pushed 1 commit to branch boole_inequality.

• wip (3e040e6)

Mathcomp Analysis Github Bot (Jun 11 2020 at 21:34):

affeldt-aist updated PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 12 2020 at 22:48):

affeldt-aist pushed 2 commits to branch boole_inequality.

• technical lemmas about ereal and minor generalization (5272de4)
• proofs that mu_ext is an outer measure (cc6af70)

Mathcomp Analysis Github Bot (Jun 12 2020 at 22:48):

affeldt-aist updated PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 13 2020 at 07:41):

affeldt-aist opened Issue #228 move to boolp:

forallN, eqNNP, and existsN from

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/normedtype.v#L451-L468

should be moved to boolp.v near existsPN, existsNP. forallNP, forallPN

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/boolp.v#L556-L582

Wanted: better names.

Mathcomp Analysis Github Bot (Jun 13 2020 at 07:42):

affeldt-aist labeled Issue #228 move to boolp:

forallN, eqNNP, and existsN from

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/normedtype.v#L451-L468

should be moved to boolp.v near existsPN, existsNP. forallNP, forallPN

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/boolp.v#L556-L582

Wanted: better names.

Mathcomp Analysis Github Bot (Jun 13 2020 at 07:42):

affeldt-aist labeled Issue #228 move to boolp:

forallN, eqNNP, and existsN from

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/normedtype.v#L451-L468

should be moved to boolp.v near existsPN, existsNP. forallNP, forallPN

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/boolp.v#L556-L582

Wanted: better names.

Mathcomp Analysis Github Bot (Jun 13 2020 at 07:42):

affeldt-aist unlabeled Issue #228 move to boolp:

forallN, eqNNP, and existsN from

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/normedtype.v#L451-L468

should be moved to boolp.v near existsPN, existsNP. forallNP, forallPN

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/boolp.v#L556-L582

Wanted: better names.

Mathcomp Analysis Github Bot (Jun 13 2020 at 07:42):

affeldt-aist labeled Issue #228 move to boolp:

forallN, eqNNP, and existsN from

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/normedtype.v#L451-L468

should be moved to boolp.v near existsPN, existsNP. forallNP, forallPN

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/boolp.v#L556-L582

Wanted: better names.

Mathcomp Analysis Github Bot (Jun 13 2020 at 07:42):

affeldt-aist milestoned Issue #228 move to boolp:

forallN, eqNNP, and existsN from

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/normedtype.v#L451-L468

should be moved to boolp.v near existsPN, existsNP. forallNP, forallPN

https://github.com/math-comp/analysis/blob/f5324c0122537ceaf653a02621158232d9cec982/theories/boolp.v#L556-L582

Wanted: better names.

Mathcomp Analysis Github Bot (Jun 16 2020 at 22:13):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 17 2020 at 08:57):

affeldt-aist pushed 1 commit to branch boole_inequality.

• cosmetics (410d110)

Mathcomp Analysis Github Bot (Jun 17 2020 at 08:57):

affeldt-aist updated PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 17 2020 at 09:41):

CohenCyril merged PR #220 rename the short ub and lb to ubound and lbound

Mathcomp Analysis Github Bot (Jun 17 2020 at 09:41):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and affeldt-aist (1).

• rename the short ub and lb to ubound and lbound (b8414e4)
• Merge pull request #220 from math-comp/ub_lb_renaming (55e6be3)

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:41):

affeldt-aist:

• created 2020 06 17 Meeting

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:44):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:52):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:52):

CohenCyril created PR Review Comment on #223 Boole inequality:

Statements of {homo : ... } or {mono : ...} shouldn't be named after homo, or mono, just as for {morph ...} lemmas. Instead please use the head of the unfolded statement (for homo) or the head of the LHS of the equality (for mono). In this case: sub_bigUB_of.

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:55):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:55):

CohenCyril created PR Review Comment on #223 Boole inequality:

When a mono lemma subsumes homo, it gets priority for the short name, and if really needed the corresponding homo lemma can be suffixed with W. If the mono lemma is only valid on a subdomain, then the homo lemma takes the short name, and the mono lemma gets the suffix in.
(This should all be added to CONTRIBUTING.md I guess)

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:55):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:55):

CohenCyril created PR Review Comment on #223 Boole inequality:

lee_mu_ext

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:56):

CohenCyril edited PR Review Comment on #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:58):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:58):

CohenCyril created PR Review Comment on #223 Boole inequality:

No is_ prefix anymore, since it is not about a predicate but a packaged operator.
Same is true everywhere incuding in outer_measure.

The exception is is_measure f := (axioms f) itself, which is a predicate.

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:59):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 12:59):

CohenCyril created PR Review Comment on #223 Boole inequality:

I would name it cvg_mu_inc.

Mathcomp Analysis Github Bot (Jun 17 2020 at 13:02):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 13:02):

CohenCyril created PR Review Comment on #223 Boole inequality:

This name is nice for historical purposes and external eye.
Internally I suspect it will become annoying and we should at least provide an alias: e.g. le_mu_bigsetU.
(and the generalized one \le_mu_bigcup)

Mathcomp Analysis Github Bot (Jun 17 2020 at 13:02):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 13:02):

CohenCyril created PR Review Comment on #223 Boole inequality:

@affeldt-aist I would vouch for cutting here for this PR.

Mathcomp Analysis Github Bot (Jun 17 2020 at 14:59):

affeldt-aist pushed 1 commit to branch fixes_228.

• renaming of lemmas for classical reasoning (ecd914f)

Mathcomp Analysis Github Bot (Jun 17 2020 at 14:59):

affeldt-aist opened PR #229 renaming of lemmas for classical reasoning from fixes_228 to master:

fixes #228

Mathcomp Analysis Github Bot (Jun 17 2020 at 16:48):

affeldt-aist:

• edited 2020 06 17 Meeting

Mathcomp Analysis Github Bot (Jun 17 2020 at 18:12):

affeldt-aist pushed 3 commits to branch boole_inequality.

• tentative proof of Boole's inequality (f001775)
• technical lemmas about ereal and minor generalization (8c499a4)
• improved presentation (3a1d8a7)

Mathcomp Analysis Github Bot (Jun 17 2020 at 18:12):

affeldt-aist updated PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 17 2020 at 18:47):

affeldt-aist pushed 2 commits to branch integral_sketch.

• integral.v file written with all members during mathcomp-analysis-dev meeting (0e0ba3c)
• tentative definition of outer measure and basic properties (5c6ea4c)

Mathcomp Analysis Github Bot (Jun 17 2020 at 18:47):

affeldt-aist updated PR #224 Integral sketch from integral_sketch to boole_inequality:

Depends on #223 (EDIT by Cyril)

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:00):

affeldt-aist pushed 1 commit to branch contributing_guide.

• naming convention about homo/mono lemmas (01e58b8)

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:00):

affeldt-aist updated PR #197 contributing file from contributing_guide to master:

The goal is to explain good practices that are specific to mathcomp-analysis. Still embryonic.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:02):

pi8027 opened PR #230 Fix inheritance from pseudoMetricNormedZmodType to completeNormedModType from fix-inheritance to master.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:20):

affeldt-aist deleted the branch ub_lb_renaming.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:24):

affeldt-aist:

• edited Home

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:25):

CohenCyril merged PR #230 Fix inheritance from pseudoMetricNormedZmodType to completeNormedModType.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:25):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and pi8027 (1).

• Fix inheritance from pseudoMetricNormedZmodType to completeNormedModType (4e5561e)
• Merge pull request #230 from pi8027/fix-inheritance (eb14886)

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:26):

affeldt-aist deleted the branch mathcomp_master_integration.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:26):

affeldt-aist deleted the branch mathcomp_master.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:26):

CohenCyril submitted PR Review for #229 renaming of lemmas for classical reasoning.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:26):

CohenCyril created PR Review Comment on #229 renaming of lemmas for classical reasoning:

Lemma not_forallP T (P : T -> Prop) :

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:27):

CohenCyril submitted PR Review for #229 renaming of lemmas for classical reasoning.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:27):

CohenCyril created PR Review Comment on #229 renaming of lemmas for classical reasoning:

while you're at it, could you add andC if it's not already here.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:36):

affeldt-aist pushed 1 commit to branch fixes_228.

• renaming of lemmas for classical reasoning (7c59b85)

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:36):

affeldt-aist updated PR #229 renaming of lemmas for classical reasoning from fixes_228 to master:

fixes #228

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:38):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:38):

CohenCyril created PR Review Comment on #223 Boole inequality:

My appologies I got carried away and did not realize the homo was not even the conclusion.
In fact the right name would be eq_bigsetUB_of.

Lemma eq_bigsetUB_of (A : (set T) ^nat) n :

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:38):

CohenCyril submitted PR Review for #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:38):

CohenCyril created PR Review Comment on #223 Boole inequality:

And here

Lemma eq_bugcupB_of (A : (set T) ^nat) : {homo A : n m / (n <= m)%nat >-> n `<=` m} ->

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:38):

CohenCyril edited PR Review Comment on #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:40):

CohenCyril submitted PR Review for #229 renaming of lemmas for classical reasoning.

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:40):

CohenCyril created PR Review Comment on #229 renaming of lemmas for classical reasoning:

(and add it to the changelog ;))

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:44):

affeldt-aist pushed 1 commit to branch fixes_228.

• renaming of lemmas for classical reasoning (6d3990d)

Mathcomp Analysis Github Bot (Jun 17 2020 at 19:44):

affeldt-aist updated PR #229 renaming of lemmas for classical reasoning from fixes_228 to master:

fixes #228

Mathcomp Analysis Github Bot (Jun 17 2020 at 21:09):

affeldt-aist pushed 1 commit to branch boole_inequality.

• improved presentation (1785dfe)

Mathcomp Analysis Github Bot (Jun 17 2020 at 21:09):

affeldt-aist updated PR #223 Boole inequality from boole_inequality to master:

Tentative formalization of Boole's inequality (wip).

Mathcomp Analysis Github Bot (Jun 17 2020 at 21:23):

affeldt-aist opened Issue #231 Get rid of filter_index_enum warnings:

In normedtype.v, two occurrences of filter_index_enum cause

Warning: filter_index_enum is deprecated; use big_enumP instead

Mathcomp Analysis Github Bot (Jun 17 2020 at 21:47):

affeldt-aist pushed 3 commits to branch mathcom_master_pseudoNormedZmod. Commits by affeldt-aist (2) and mkerjean (1).

• generalizations of several lemmas (3d1c552)
• enough generalizations for compilation to go through (aeea00d)
• remove useless(?) lemma (22d4e78)

Mathcomp Analysis Github Bot (Jun 17 2020 at 21:47):

affeldt-aist updated PR #180 Mathcomp master PseudoMetricNormedZmod from mathcom_master_pseudoNormedZmod to master:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

Mathcomp Analysis Github Bot (Jun 17 2020 at 21:52):

affeldt-aist pushed 2 commits to branch more_sequences.

• Examples of sequences and series (db2462f)
• rebasing (3f7f609)

Mathcomp Analysis Github Bot (Jun 17 2020 at 21:52):

affeldt-aist updated PR #207 more lemmas about sequences from more_sequences to master:

This PR is the result of a split of the PR #187 .
It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for sequences.v.

Mathcomp Analysis Github Bot (Jun 17 2020 at 21:53):

affeldt-aist closed without merge PR #137 integral.v draft.

Mathcomp Analysis Github Bot (Jun 19 2020 at 03:01):

CohenCyril merged PR #223 Boole inequality.

Mathcomp Analysis Github Bot (Jun 19 2020 at 03:01):

CohenCyril pushed 4 commits to branch master. Commits by affeldt-aist (3) and CohenCyril (1).

• tentative proof of Boole's inequality (f001775)
• technical lemmas about ereal and minor generalization (8c499a4)
• improved presentation (1785dfe)
• Merge pull request #223 from math-comp/boole_inequality (8daddda)

Mathcomp Analysis Github Bot (Jun 19 2020 at 06:28):

pi8027 opened PR #232 Generalize prod_pseudoMetricNormedZmodType from prod_pseudoMetricNormedZmodType to master:

I'm trying to fix #180 and discovered this generalization, but this does not help us to fix it.

Mathcomp Analysis Github Bot (Jun 19 2020 at 06:28):

pi8027 edited PR #232 Generalize prod_pseudoMetricNormedZmodType from prod_pseudoMetricNormedZmodType to master:

I'm trying to fix PR #180 and discovered this generalization, but this does not help us to fix it.

Mathcomp Analysis Github Bot (Jun 19 2020 at 10:59):

affeldt-aist pushed 1 commit to branch rename_locally.

• rename "locally" to "nbhs" and propagate (fa0566a)

Mathcomp Analysis Github Bot (Jun 19 2020 at 11:02):

affeldt-aist pushed 1 commit to branch rename_locally.

• rename "locally" to "nbhs" and propagate (9ec416b)

Mathcomp Analysis Github Bot (Jun 19 2020 at 11:04):

affeldt-aist opened PR #233 rename "locally" to "nbhs" and propagate from rename_locally to master:

fixes #214

(this is in progress, not all occurrences have been treated yet on purpose)

Mathcomp Analysis Github Bot (Jun 22 2020 at 08:08):

pi8027 opened PR #234 Get rid of filter_index_enum from remove-filter_index_enum to master:

Closes #231

Mathcomp Analysis Github Bot (Jun 22 2020 at 08:16):

pi8027 updated PR #234 Get rid of filter_index_enum from remove-filter_index_enum to master:

Closes #231

Mathcomp Analysis Github Bot (Jun 22 2020 at 08:17):

pi8027 edited PR #234 Get rid of deprecated lemmas filter_index_enum, uniq_perm_eq, and perm_eq_small from remove-filter_index_enum to master:

Closes #231

Mathcomp Analysis Github Bot (Jun 23 2020 at 00:40):

CohenCyril closed Issue #231 Get rid of filter_index_enum warnings:

In normedtype.v, two occurrences of filter_index_enum cause

Warning: filter_index_enum is deprecated; use big_enumP instead

Mathcomp Analysis Github Bot (Jun 23 2020 at 00:40):

CohenCyril merged PR #234 Get rid of deprecated lemmas filter_index_enum, uniq_perm_eq, and perm_eq_small.

Mathcomp Analysis Github Bot (Jun 23 2020 at 00:40):

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and pi8027 (1).

• Get rid of deprecated lemmas filter_index_enum, uniq_perm_eq, and perm_eq_small (04f77b7)
• Merge pull request #234 from pi8027/remove-filter_index_enum (10aed13)

Mathcomp Analysis Github Bot (Jun 23 2020 at 05:46):

pi8027 edited PR #232 Generalize prod_pseudoMetricNormedZmodType from prod_pseudoMetricNormedZmodType to master:

This PR generalizes the parameters of prod_pseudoMetricNormedZmodType from normedModType to pseudoMetricNormedZmodType. I'm trying to fix PR #180 and discovered this generalization, but this does not help us to fix it.

Mathcomp Analysis Github Bot (Jun 23 2020 at 11:39):

affeldt-aist pushed 1 commit to branch rename_locally.

• remote more "locally" into "nbhs" and propagate (dd46b4d)

Mathcomp Analysis Github Bot (Jun 23 2020 at 11:39):

affeldt-aist updated PR #233 rename "locally" to "nbhs" and propagate from rename_locally to master:

fixes #214

(this is in progress, not all occurrences have been treated yet on purpose)

Mathcomp Analysis Github Bot (Jun 23 2020 at 11:40):

affeldt-aist has marked PR #233 as ready for review.

Mathcomp Analysis Github Bot (Jun 28 2020 at 12:29):

Zimmi48 opened PR #235 Fix links of projects moved to coq-community. from patch-1 to master:

Both of these projects are now maintained by @amiloradovsky as part of coq-community.

Mathcomp Analysis Github Bot (Jun 30 2020 at 07:02):

affeldt-aist merged PR #235 Fix links of projects moved to coq-community.

Mathcomp Analysis Github Bot (Jun 30 2020 at 07:02):

affeldt-aist pushed 1 commit to branch master. Commits by Zimmi48 (1).

• Fix links of projects moved to coq-community. (b8d9c78)

Mathcomp Analysis Github Bot (Jul 07 2020 at 21:28):

mkerjean pushed 14 commits to branch numfield_topology.

• normedType on numFieldType (e67bef9)
• erasing ^o wip (3b55366)
• erasing ^o numFieldType_canonical_contd (3bf1573)
• erasing ^o wip (615db17)
• normedType of realFieldType (f6a60f2)
• vecspace of numField (3123c22)
• add complex theory (979fae0)
• cvgN and cvgD with explicit arguments (a0dbdb0)
• holomorphy without Ro (93874c7)
• wip (411fb77)
• Impossible NormedModType structure (fe59d6f)
• test (3848e94)
• without ComplexField (49bc459)
• clean (a5f6075)

Mathcomp Analysis Github Bot (Jul 07 2020 at 21:28):

mkerjean updated PR #205 Topological structures on numfields from numfield_topology to master:

This PR aims to get rid of the notation ^ o, by endowing any numFieldType with a canonical normedModType structure.

Mathcomp Analysis Github Bot (Jul 08 2020 at 14:36):

mkerjean pushed 21 commits to branch holomorphy. Commits by mkerjean (14), affeldt-aist (6) and CohenCyril (1).

• Mathcomp analysis now depends on real-closed (e241ab8)
• proof of Cauchy thm; derivx, derivy (eeaf376)
• holomorphic is derivable, holomorphic implies Cauchy-Riemann (8b32589)
• update cauchyetoile.v wrt PR#270 (5c01410)
• update cauchyetoile.v wrt PR#270 (18cb251)
• renaming: Uniform -> PseudoMetric (1c11c06)
• wip (fd439ed)
• update cauchyetoile.v (47ab6be)
• fix to compile (f9e006e)
• update wrt master (8c6d1f1)
• name change (ffe47d0)
• clean (96c08bd)
• within formalisation (be8bc35)
• rebase on PR199 (c1a3103)
• update CoqProject (534f5d3)
• clean (3f59527)
• clean CR -> holo (6800d47)
• WIP Diff_CR_holo with Rcomplex (0ab448d)
• wip (6946570)
• wip (bec1b90)
  [and 1 more commit(s)]

Mathcomp Analysis Github Bot (Jul 08 2020 at 14:36):

mkerjean updated PR #204 Holomorphy from holomorphy to master:

Formalization of complex analysis, following the closed #192.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:02):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:02):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:02):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

This is wrong. pseudoMetric_of_normedDomain produces a mixin, not a structure instance.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:02):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

This Canonical declaration makes numFieldType inheriting from pointedType, but by construction rather than inclusion. Actually, this can be generalized to make zmodType inheriting from pointedType, and then you have to declare unification hints between Pointed.sort and all the subclasses of zmodType. Even if you do not generalize it, similar unification hints for numClosedFieldType, realFieldType, archiFieldType, rcfType, and realType have to be declared.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:08):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:08):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

I guess similar issues appear almost everywhere, and it is too painful to fix.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:30):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:30):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

There is an easier way to do this by relying on the regular (^o) instances.

Canonical numfield_lmodType := [lmodType K of K for [lmodType K of K^o]].
Canonical numfield_lalgType := [lalgType K of K for [lalgType K of K^o]].
Canonical numfield_algType := [algType K of K for [algType K of K^o]].

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:54):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:54):

mkerjean created PR Review Comment on #205 Topological structures on numfields:

I guess I would like not to rely on the canonical ^o instances, as I'm afraid this will introduce the usual confusion on the lmodType structure of K^o.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:56):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 19:56):

mkerjean created PR Review Comment on #205 Topological structures on numfields:

Indeed, thanks.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:02):

mkerjean edited PR Review Comment on #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:10):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:10):

mkerjean created PR Review Comment on #205 Topological structures on numfields:

By almost everywhere, do you mean unification hints between numfieldType (and its restructions) and pointed/filtered/etc ?

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:35):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:35):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

The above numfield_lmodType is constructed using regular_lmodType, but the unification hint synthesized from it is Num.NumField.sort <- GRing.Lmodule.sort. So it makes numFieldType inheriting from lmodType by construction.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:38):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:38):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

I meant almost every new canonical declarations (but actually they are not that many). But numfield_lmodType below has the same issue.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:48):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:48):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

As in Cyril's comment above, numFieldType should inherit from fieldExtType (by construction) after this PR. By transitivity, the structures (A) should inherit from all the structures (B) below.

• (A): numFieldType, numClosedFieldType, realFieldType, archiFieldType, rcfType, and realType,
• (B): lmodType, lalgType, algType, comAlgType, unitAlgType, comUnitAlgType, vectType, falgType, and fieldExtType.

So we need the following 6 × 9 = 54 unification hints for them.

Canonical numField_lmodType (K : numFieldType) :=
  [lmodType K of K for [lmodType K of K^o]].
Canonical numField_lalgType (K : numFieldType) :=
  [lalgType K of K for [lalgType K of K^o]].
Canonical numField_algType (K : numFieldType) :=
  [algType K of K for [algType K of K^o]].
Canonical numField_comAlgType (K : numFieldType) := [comAlgType K of K].
Canonical numField_unitAlgType (K : numFieldType) := [unitAlgType K of K].
Canonical numField_comUnitAlgType (K : numFieldType) := [comUnitAlgType K of K].
Canonical numField_vectType (K : numFieldType) :=
  [vectType K of K for [vectType K of K^o]].
Canonical numField_falgType (K : numFieldType) := [FalgType K of K].
Canonical numField_fieldExtType (K : numFieldType) :=
  [fieldExtType K of K for regular_fieldExtType K].

Canonical numClosedField_lmodType (K : numClosedFieldType) :=
  [lmodType K of K for [lmodType K of K^o]].
Canonical numClosedField_lalgType (K : numClosedFieldType) :=
  [lalgType K of K for [lalgType K of K^o]].
Canonical numClosedField_algType (K : numClosedFieldType) :=
  [algType K of K for [algType K of K^o]].
Canonical numClosedField_comAlgType (K : numClosedFieldType) :=
  [comAlgType K of K].
Canonical numClosedField_unitAlgType (K : numClosedFieldType) :=
  [unitAlgType K of K].
Canonical numClosedField_comUnitAlgType (K : numClosedFieldType) :=
  [comUnitAlgType K of K].
Canonical numClosedField_vectType (K : numClosedFieldType) :=
  [vectType K of K for [vectType K of K^o]].
Canonical numClosedField_falgType (K : numClosedFieldType) := [FalgType K of K].
Canonical numClosedField_fieldExtType (K : numClosedFieldType) :=
  [fieldExtType K of K for regular_fieldExtType K].

Canonical realField_lmodType (K : realFieldType) :=
  [lmodType K of K for [lmodType K of K^o]].
Canonical realField_lalgType (K : realFieldType) :=
  [lalgType K of K for [lalgType K of K^o]].
Canonical realField_algType (K : realFieldType) :=
  [algType K of K for [algType K of K^o]].
Canonical realField_comAlgType (K : realFieldType) := [comAlgType K of K].
Canonical realField_unitAlgType (K : realFieldType) := [unitAlgType K of K].
Canonical realField_comUnitAlgType (K : realFieldType) :=
  [comUnitAlgType K of K].
Canonical realField_vectType (K : realFieldType) :=
  [vectType K of K for [vectType K of K^o]].
Canonical realField_falgType (K : realFieldType) := [FalgType K of K].
Canonical realField_fieldExtType (K : realFieldType) :=
  [fieldExtType K of K for regular_fieldExtType K].

Canonical archiField_lmodType (K : archiFieldType) :=
  [lmodType K of K for [lmodType K of K^o]].
Canonical archiField_lalgType (K : archiFieldType) :=
  [lalgType K of K for [lalgType K of K^o]].
Canonical archiField_algType (K : archiFieldType) :=
  [algType K of K for [algType K of K^o]].
Canonical archiField_comAlgType (K : archiFieldType) := [comAlgType K of K].
Canonical archiField_unitAlgType (K : archiFieldType) := [unitAlgType K of K].
Canonical archiField_comUnitAlgType (K : archiFieldType) :=
  [comUnitAlgType K of K].
Canonical archiField_vectType (K : archiFieldType) :=
  [vectType K of K for [vectType K of K^o]].
Canonical archiField_falgType (K : archiFieldType) := [FalgType K of K].
Canonical archiField_fieldExtType (K : archiFieldType) :=
  [fieldExtType K of K for regular_fieldExtType K].

Canonical rcf_lmodType (K : rcfType) :=
  [lmodType K of K for [lmodType K of K^o]].
Canonical rcf_lalgType (K : rcfType) :=
  [lalgType K of K for [lalgType K of K^o]].
Canonical rcf_algType (K : rcfType) := [algType K of K for [algType K of K^o]].
Canonical rcf_comAlgType (K : rcfType) := [comAlgType K of K].
Canonical rcf_unitAlgType (K : rcfType) := [unitAlgType K of K].
Canonical rcf_comUnitAlgType (K : rcfType) := [comUnitAlgType K of K].
Canonical rcf_vectType (K : rcfType) :=
  [vectType K of K for [vectType K of K^o]].
Canonical rcf_falgType (K : rcfType) := [FalgType K of K].
Canonical rcf_fieldExtType (K : rcfType) :=
  [fieldExtType K of K for regular_fieldExtType K].

Canonical real_lmodType (K : realType) :=
  [lmodType K of K for [lmodType K of K^o]].
Canonical real_lalgType (K : realType) :=
  [lalgType K of K for [lalgType K of K^o]].
Canonical real_algType (K : realType) :=
  [algType K of K for [algType K of K^o]].
Canonical real_comAlgType (K : realType) := [comAlgType K of K].
Canonical real_unitAlgType (K : realType) := [unitAlgType K of K].
Canonical real_comUnitAlgType (K : realType) := [comUnitAlgType K of K].
Canonical real_vectType (K : realType) :=
  [vectType K of K for [vectType K of K^o]].
Canonical real_falgType (K : realType) := [FalgType K of K].
Canonical real_fieldExtType (K : realType) :=
  [fieldExtType K of K for regular_fieldExtType K].

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:50):

pi8027 edited PR Review Comment on #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:59):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 20:59):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

I think it would be better to declare these canonicals also as implicit coercions, and if Coq reports "ambiguous paths", we should stop coding and discuss.

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:02):

pi8027 edited PR Review Comment on #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:06):

CohenCyril submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:06):

CohenCyril created PR Review Comment on #205 Topological structures on numfields:

@pi8027 spot on!

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:08):

CohenCyril submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:08):

CohenCyril created PR Review Comment on #205 Topological structures on numfields:

I would like not to rely on the canonical ^o instances, as I'm afraid this will introduce the usual confusion on the lmodType structure of K^o.

In the sentence [lmodType K of X for Y], Y is only used to get the mixin and the canonical structure is put on X. So using ^o in Y leverages what we already know about ^o to endow X with it.

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:16):

CohenCyril submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:16):

CohenCyril created PR Review Comment on #205 Topological structures on numfields:

@pi8027

coq Canonical numField_fieldExtType (K : numFieldType) := [fieldExtType K of K for regular_fieldExtType K].

I would rather not rely on the name of a canonical structure, doesn't [fieldExtType K of K^o] work? (i.e. isn't regular_fieldExtType K canonical?)

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:16):

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:21):

pi8027 submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 08 2020 at 21:21):

pi8027 created PR Review Comment on #205 Topological structures on numfields:

I would rather not rely on the name of a canonical definition, doesn't [fieldExtType K of K^o] work? (i.e. isn't regular_fieldExtType K canonical?)

No, it doesn't work. I think it is broken on the MathComp side. Let me check.

Mathcomp Analysis Github Bot (Jul 09 2020 at 07:07):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 07:07):

mkerjean created PR Review Comment on #205 Topological structures on numfields:

I would like not to rely on the canonical ^o instances, as I'm afraid this will introduce the usual confusion on the lmodType structure of K^o.

In the sentence [lmodType K of X for Y], Y is only used to get the mixin and the canonical structure is put on X. So using ^o in Y leverages what we already know about ^o to endow X with it.

My goal i this PR was to suppress any use of K^o as a topological object. Is there any advantage in using K^o as an intermediate object ?

Mathcomp Analysis Github Bot (Jul 09 2020 at 07:53):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 07:53):

mkerjean created PR Review Comment on #205 Topological structures on numfields:

I think it would be better to declare these canonicals also as implicit coercions, and if Coq reports "ambiguous paths", we should stop coding and discuss.

Won't this happen if we keep the constructions on K^o as they are ?

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:37):

CohenCyril submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:37):

CohenCyril created PR Review Comment on #205 Topological structures on numfields:

I would like not to rely on the canonical ^o instances, as I'm afraid this will introduce the usual confusion on the lmodType structure of K^o.

In the sentence [lmodType K of X for Y], Y is only used to get the mixin and the canonical structure is put on X. So using ^o in Y leverages what we already know about ^o to endow X with it.

My goal i this PR was to suppress any use of K^o as a topological object. Is there any advantage in using K^o as an intermediate object ?

Yes, as Kazuhuiko demonstrated, most of the work has already done for ^o so using it as an intermediate object saves time and proofs.

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:37):

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:43):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:43):

mkerjean created PR Review Comment on #205 Topological structures on numfields:

Except from time, of course. It seems to me that using K^o as an intermediate object makes the file less readable and accessible to new users. I would be willing to rewrite everything on numFields directly.

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:50):

CohenCyril submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:51):

CohenCyril created PR Review Comment on #205 Topological structures on numfields:

Except from time, of course. It seems to me that using K^o as an intermediate object makes the file less readable and accessible to new users. I would be willing to rewrite everything on numFields directly.

Not only time but also maintainability (= robustness to change + number of loc to update). One should not write twice the same piece of code.
Instead I advocate for a comment that explains what these lines are doing.

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:58):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 12:58):

mkerjean created PR Review Comment on #205 Topological structures on numfields:

Indeed, and this is why my intention was to remove anything related to ^o in the mathcomp/analysis setting. Would you be against that ?

Mathcomp Analysis Github Bot (Jul 09 2020 at 16:32):

CohenCyril submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 16:32):

CohenCyril created PR Review Comment on #205 Topological structures on numfields:

We cannot really remove ^o since it is in core mathcomp and useful there. Actually, all the results about ^o from @pi8027's snippet come from mathcomp core. There is nothing we can do in mathcomp/analysis to get rid of them, so we should rather reuse them (for free).

Mathcomp Analysis Github Bot (Jul 09 2020 at 16:33):

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 16:33):

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 16:33):

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 16:44):

mkerjean submitted PR Review for #205 Topological structures on numfields.

Mathcomp Analysis Github Bot (Jul 09 2020 at 16:44):

mkerjean created PR Review Comment on #205 Topological structures on numfields: