GitHub webhook has been successfully configured by CohenCyril.

affeldt-aist pushed 1 commit to branch fixes155.

- fixes #155 (3b963a9)

affeldt-aist pushed 1 commit to branch bounded.

- typo (842175a)

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)

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)

CohenCyril pushed the branch cvg_naming.

CohenCyril pushed 2 commits to branch cvg_naming.

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

CohenCyril pushed 1 commit to branch cvg_naming.

- Big refactoring about naming conventions (9950ef0)

CohenCyril pushed 1 commit to branch cvg_naming.

- Big refactoring about naming conventions (bba89c9)

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

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

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

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

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

CohenCyril pushed 2 commits to branch master.

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

CohenCyril pushed the branch renamings.

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

- Various renamings (33e384a)

CohenCyril pushed 1 commit to branch travis_not_twice.

- make travis not run twice! (1d128ee)

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

- Various renamings (2eccc5f)

CohenCyril pushed 1 commit to branch mathcomp_master_sequences.

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

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

- wip (d46f236)

CohenCyril pushed 1 commit to branch master.

- make travis not run twice! (fac1196)

CohenCyril deleted the branch travis_not_twice.

CohenCyril pushed 1 commit to branch bounded.

- Generic domination, boundedness and lipshitz (f4c6b19)

CohenCyril pushed 1 commit to branch bounded.

- Generic domination, boundedness and lipschitz (c2cea9a)

CohenCyril pushed 1 commit to branch better_inE.

- in_setE/in_fsetE -> inE (7d5747f)

CohenCyril pushed 1 commit to branch master.

- Generic domination, boundedness and lipschitz (20b79f7)

CohenCyril pushed 1 commit to branch better_inE.

- in_setE/in_fsetE -> inE (3862fb8)

CohenCyril pushed 1 commit to branch better_inE.

- in_setE/in_fsetE -> inE (fe37a38)

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

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

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

- proved nonincreasing_cvg, minor cleaning (53f126e)

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

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

CohenCyril pushed 1 commit to branch master.

- in_setE/in_fsetE -> inE (f8d361a)

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

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

CohenCyril deleted the branch better_inE.

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

- add a few lemmas (7b3435e)

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.

affeldt-aist pushed 1 commit to branch contributing_guide.

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

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.

affeldt-aist:

- edited Home

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

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

use

`sum_nat_const`

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

- use sum_nat_const_nat in cesaro (6f5eefd)

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.

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)

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`set`

s 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.

affeldt-aist pushed 1 commit to branch supremums_ereal.

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

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`set`

s 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.

CohenCyril pushed 1 commit to branch mathcomp_master_sequences.

- simplifying Cesaro (7adaef8)

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.

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.

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

- tentative converse of cesaro (wip) (a69e18a)

affeldt-aist updated PR #187 A few lemmas about sequences from `mathcomp_master_sequences`

to `master`

:

`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.

mkerjean edited PR #188 Topological structures on numDomains and numFields from `locallyN_lim_cst_generalization`

to `master`

:

Is this change of canonical structures correct?

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`

.

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)

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`

.

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`

.

affeldt-aist:

- edited Home

mkerjean pushed 1 commit to branch cauchy_etoile.

- name change (e09c8a2)

mkerjean updated PR #192 Holomorphy from `cauchy_etoile`

to `master`

:

`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`

.

mkerjean deleted the branch cauchy_etoile.

mkerjean closed without merge PR #192 Holomorphy.

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)

mkerjean opened PR #204 Holomorphy from `holomorphy`

to `master`

:

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

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

- generalizations of several lemmas (7d4bed6)

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

to `mathcomp_master_hausdorff_close`

:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

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

to `master`

:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

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

affeldt-aist updated PR #187 A few lemmas about sequences from `mathcomp_master_sequences`

to `master`

:

`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.

affeldt-aist:

- edited Home

affeldt-aist deleted the branch mathcomp_master_hausdorff_close.

affeldt-aist deleted the branch bounded.

affeldt-aist deleted the branch fixes155.

affeldt-aist deleted the branch sequences.

affeldt-aist deleted the branch analysis_270.

affeldt-aist deleted the branch mathcomp_master_hausdorff.

affeldt-aist:

- edited Home

mkerjean pushed 1 commit to branch holomorphy.

- clean (3ead4f3)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

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

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?

mkerjean pushed 1 commit to branch holomorphy.

- within formalisation (83072ba)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

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

CohenCyril edited PR #188 Topological structures on numFields from `locallyN_lim_cst_generalization`

to `master`

:

Is this change of canonical structures correct?

CohenCyril edited PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

mkerjean pushed 1 commit to branch holomorphy.

- rebase on PR199 (01c534a)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

mkerjean pushed 1 commit to branch holomorphy.

- name change (85aa10a)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

mkerjean pushed 1 commit to branch holomorphy.

- rebase on PR199 (c383ce6)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

mkerjean pushed 1 commit to branch holomorphy.

- update CoqProject (a320f3f)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

mkerjean pushed the branch numfield_topology.

mkerjean pushed 1 commit to branch holomorphy.

- update CoqProject (8339fd8)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

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)

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.

mkerjean pushed 1 commit to branch numfield_topology.

- vecspace of numField (baad880)

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.

affeldt-aist pushed 1 commit to branch supremums_ereal.

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

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`set`

s 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.

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

- wip (4e710e9)

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

to `master`

:

work in progress, supersedes PR #137

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

- wip (a7ce0de)

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

to `master`

:

work in progress, supersedes PR #137

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.

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

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

affeldt-aist updated PR #187 A few lemmas about sequences from `mathcomp_master_sequences`

to `master`

:

`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.

affeldt-aist pushed the branch more_sequences.

affeldt-aist pushed 1 commit to branch more_sequences.

- more lemmas about sequences (d38dd5e)

affeldt-aist opened PR #207 more lemmas about sequences from `more_sequences`

to `mathcomp_master_sequences`

.

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`

.

affeldt-aist pushed 1 commit to branch mathcomp_master_sequences.

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

affeldt-aist updated PR #187 A few lemmas about sequences from `mathcomp_master_sequences`

to `master`

:

`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.

affeldt-aist pushed 1 commit to branch more_sequences.

- Examples of sequences and series (ded45f7)

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`

.

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>

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>

affeldt-aist pushed 1 commit to branch more_sequences.

- Examples of sequences and series (8de5885)

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`

.

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>

affeldt-aist pushed 1 commit to branch ereal_arithmetic.

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

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.

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

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

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

to `master`

:

work in progress, supersedes PR #137

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

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

`mathcomp_master_integration_ereal`

to `master`

:

work in progress, supersedes PR #137

affeldt-aist pushed 1 commit to branch mathcom_master_pseudoNormedZmod.

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

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

to `master`

:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

affeldt-aist pushed 1 commit to branch mathcom_master_pseudoNormedZmod.

- remove useless(?) lemma (d01e689)

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

to `master`

:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch subrKA_subr_trans.

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

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

to `master`

:

small fix

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

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

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

CohenCyril deleted the branch subrKA_subr_trans.

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)]

CohenCyril opened PR #210 upgrading default.nix from `nix`

to `master`

.

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

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

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

CohenCyril merged PR #210 upgrading default.nix.

CohenCyril pushed 1 commit to branch master.

- upgrading default.nix (4fe4b7a)

CohenCyril merged PR #187 Basic lemmas about sequences.

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

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

CohenCyril deleted the branch nix.

CohenCyril pushed 1 commit to branch master.

- Update README.md (1a1648a)

CohenCyril pushed 1 commit to branch master.

- Update README.md (a20000d)

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)

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.

CohenCyril pushed 1 commit to branch nix.

- updating config.nix (efb75d7)

CohenCyril opened PR #211 updating config.nix from `nix`

to `master`

.

CohenCyril merged PR #211 updating config.nix.

CohenCyril pushed 1 commit to branch master.

- updating config.nix (eca06c7)

affeldt-aist:

- edited Home

mkerjean:

- edited Home

mkerjean pushed 1 commit to branch numfield_topology.

- Impossible NormedModType structure (23f40d5)

mkerjean updated PR #205 Topological structures on numfields from `numfield_topology`

to `master`

:

mkerjean:

- edited Home

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_master_integration_ereal`

to `master`

:

work in progress, supersedes PR #137

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)

affeldt-aist updated PR #203 Supremums ereal from `supremums_ereal`

to `master`

:

`reals.v`

. I tried for a while to stick to the original`pred`

-base definitions but`set`

s 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.

mkerjean pushed 1 commit to branch numfield_topology.

- test (e43f6c4)

mkerjean updated PR #205 Topological structures on numfields from `numfield_topology`

to `master`

:

affeldt-aist:

- created 2020 05 25 Meeting

affeldt-aist:

- edited Home

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

affeldt-aist pushed 1 commit to branch master.

- tentative definition of bigmaxr with bigop (4c30ca2)

mkerjean pushed 1 commit to branch numfield_topology.

- without ComplexField (3159f85)

mkerjean updated PR #205 Topological structures on numfields from `numfield_topology`

to `master`

:

affeldt-aist pushed 1 commit to branch changelog.

- tentative changelog (f13a80b)

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.

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

mkerjean pushed 1 commit to branch numfield_topology.

- without ComplexField (90cc8e8)

mkerjean updated PR #205 Topological structures on numfields from `numfield_topology`

to `master`

:

CohenCyril submitted PR Review for #212 tentative changelog.

CohenCyril created PR Review Comment on #212 tentative changelog:

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

CohenCyril pushed 1 commit to branch changelog.

- Update CHANGELOG_UNRELEASED.md (d8415e9)

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.

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

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

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

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

affeldt-aist pushed 1 commit to branch supremums_ereal.

- fix (f29b661)

affeldt-aist updated PR #203 Supremums ereal from `supremums_ereal`

to `master`

:

`reals.v`

. I tried for a while to stick to the original`pred`

-base definitions but`set`

s 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.

affeldt-aist deleted the branch ereal_arithmetic.

affeldt-aist deleted the branch analysis_270_integration.

affeldt-aist deleted the branch cvg_naming.

mkerjean pushed 1 commit to branch numfield_topology.

- clean (2c5886e)

mkerjean updated PR #205 Topological structures on numfields from `numfield_topology`

to `master`

:

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

Nope, corrected.

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

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.

CohenCyril pushed 1 commit to branch changelog.

- swapping stuff (2716696)

CohenCyril merged PR #212 tentative changelog.

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

- tentative changelog (#212) (244f131)

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.

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.

affeldt-aist pushed 1 commit to branch master.

- changelog for version 0.3.0 (f3ec99e)

affeldt-aist milestoned Issue #203 Supremums ereal:

`reals.v`

. I tried for a while to stick to the original`pred`

-base definitions but`set`

s 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.

affeldt-aist milestoned Issue #197 contributing file:

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

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.

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

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

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

affeldt-aist pushed tag v0.3.0.

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

affeldt-aist pushed 1 commit to branch master.

- fixes (e41a840)

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

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

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.

mkerjean pushed 2 commits to branch holomorphy.

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

mkerjean pushed 1 commit to branch holomorphy.

- WIP Diff_CR_holo with Rcomplex (d02ddf4)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

affeldt-aist pushed 1 commit to branch supremums_ereal.

- add doc and lemmas about supremum (79880f9)

affeldt-aist updated PR #203 Supremums ereal from `supremums_ereal`

to `master`

:

`reals.v`

. I tried for a while to stick to the original`pred`

-base definitions but`set`

s 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.

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

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

affeldt-aist opened Issue #214 `locally`

better be renamed after neighborhoods:

replace

`locally`

by`nbhs`

?exception:

`bounded_locally`

in`normedmodtype.v`

affeldt-aist milestoned Issue #214 `locally`

better be renamed after neighborhoods:

replace

`locally`

by`nbhs`

?exception:

`bounded_locally`

in`normedmodtype.v`

affeldt-aist labeled Issue #214 `locally`

better be renamed after neighborhoods:

replace

`locally`

by`nbhs`

?exception:

`bounded_locally`

in`normedmodtype.v`

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

- ereals from a pseudometric type (9c5fca6)

affeldt-aist opened PR #215 ereals from a pseudometric type from `ereal_pseudometric`

to `master`

:

warning: proofs to be cleaned

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

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

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

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

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

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)

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

to `master`

:

`reals.v`

. I tried for a while to stick to the original`pred`

-base definitions but`set`

s 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.

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)

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

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

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

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

`ereal_locallyE`

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

mkerjean pushed 1 commit to branch holomorphy.

- wip (a1a741b)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

mkerjean pushed 2 commits to branch holomorphy.

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

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

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

affeldt-aist:

- edited 2020 05 07 Meeting

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

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

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

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

affeldt-aist:

- edited Home

affeldt-aist:

- edited Home

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

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.

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

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

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

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_master_integration_ereal`

to `master`

:

work in progress, supersedes PR #137

affeldt-aist edited PR #189 Mathcomp master integration ereal from `mathcomp_master_integration_ereal`

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

CohenCyril pushed 1 commit to branch ereal_pseudometric.

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

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

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

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...

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

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)

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

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

affeldt-aist pushed 1 commit to branch supremums_ereal.

- add changelog information (fb9adc7)

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

to `master`

:

`reals.v`

. I tried for a while to stick to the original`pred`

-base definitions but`set`

s 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.

mkerjean:

- edited Home

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

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

`ereal_pseudometric`

to `supremums_ereal`

:

warning:

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

affeldt-aist:

- edited Home

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch issue103_fix.

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

affeldt-aist opened PR #216 Improve documentation of landau.v from `issue103_fix`

to `master`

:

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

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.

affeldt-aist:

- edited Home

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.

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.

CohenCyril merged PR #203 Supremums ereal.

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)

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)

`ereal_pseudometric`

to `supremums_ereal`

:

warning:

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

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

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)

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

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

affeldt-aist deleted the branch analysis_270_hahnbanach.

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

- renaming (5e5a8e5)

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

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

affeldt-aist opened Issue #217 Rename existsP:

Naming conflicts with

`fintype.existsP`

; the same for`forallP`

.

affeldt-aist labeled Issue #217 Rename existsP:

Naming conflicts with

`fintype.existsP`

; the same for`forallP`

.

CohenCyril pushed 1 commit to branch maxr.

- Adapting to new Order.max (b82fa34)

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

to `master`

:

Patch for math-comp/math-comp#516

affeldt-aist pushed tag 0.3.0.

CohenCyril edited release MathComp Analysis 0.3.0 for tag 0.3.0.

CohenCyril removed tag 0.3.0.

ghost unpublished release MathComp Analysis 0.3.0 for tag 0.3.0.

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

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

CohenCyril pushed tag 0.3.0.

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.

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

- fix version naming (b264352)

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.

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

- fixup (ff2b7d2)

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

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

`mathcomp_master_integration_ereal`

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

affeldt-aist deleted the branch changelog.

affeldt-aist deleted the branch entourages_bigmax.

affeldt-aist deleted the branch analysis_270_numFieldType.

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

to `master`

:

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

- Update HOWTORELEASE.md (a0d0a51)

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

- fix (29dfcba)

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

to `master`

:

affeldt-aist deleted the branch supremums_ereal.

affeldt-aist:

- created HOWTORELEASE

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch fix_issue_217.

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

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

to `master`

:

fixes #217

affeldt-aist pushed 1 commit to branch ub_lb_renaming.

- rename the short
`ub`

and`lb`

to`ubound`

and`lbound`

(08d32bd)

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

CohenCyril closed Issue #217 Rename existsP:

Naming conflicts with

`fintype.existsP`

; the same for`forallP`

.

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

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)

affeldt-aist pushed the branch update_installmd.

affeldt-aist pushed 1 commit to branch update_installmd.

- update to last version (c347ce1)

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

to `master`

:

@mkerjean observed the

`INSTALL.md`

was a bit outdated.

affeldt-aist pushed 1 commit to branch update_installmd.

- update to last version (64d8345)

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

to `master`

:

@mkerjean observed the

`INSTALL.md`

was a bit outdated.

affeldt-aist deleted the branch fix_issue_217.

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

affeldt-aist pushed 1 commit to branch master.

- update to last version (9773dc1)

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

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

`mathcomp_master_integration_ereal`

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

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

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

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

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

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

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

affeldt-aist pushed 1 commit to branch mathcomp_master_integration_ereal.

- cleaning (ada2736)

`mathcomp_master_integration_ereal`

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

affeldt-aist deleted the branch update_installmd.

affeldt-aist pushed 1 commit to branch ereal_ninfty_arithmetic.

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

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`

.

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_master_integration_ereal`

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

affeldt-aist pushed 1 commit to branch ub_lb_renaming.

- rename the short
`ub`

and`lb`

to`ubound`

and`lbound`

(a0a2a6c)

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

affeldt-aist:

- edited Home

affeldt-aist:

- edited Home

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

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)

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

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

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

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

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

warning:

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

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)

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

affeldt-aist pushed 3 commits to branch mathcomp_master_integration_ereal.

`mathcomp_master_integration_ereal`

to `ereal_pseudometric`

:

work in progress, supersedes PR #137

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

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

@affeldt-aist you should document

`expand`

as well.

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

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 ...

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

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

why?

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)

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

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

So that it type-checks in Lemma

`nondecreasing_seq_ereal_cvg`

.

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

- fix (bcf7815)

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)

affeldt-aist pushed 1 commit to branch ereal_pseudometric.

- minor fixes (861a90d)

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)

affeldt-aist pushed 1 commit to branch boole_inequality.

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

affeldt-aist opened PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

affeldt-aist edited PR #223 Boole inequality from `boole_inequality`

to `ereal_pseudometric`

:

Tentative formalization of Boole's inequality (wip).

affeldt-aist pushed 1 commit to branch integral_sketch.

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

affeldt-aist opened PR #224 Integral sketch from `integral_sketch`

to `master`

.

affeldt-aist edited PR #224 Integral sketch from `integral_sketch`

to `boole_inequality`

.

affeldt-aist deleted the branch renamings.

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

affeldt-aist pushed the branch update_installmd_1.11.

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

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

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

to `master`

.

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

CohenCyril merged PR #215 ereals form a pseudometric type.

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)

CohenCyril pushed 1 commit to branch renaming_le_expand.

- Small renamings about expand. (ccbc1a3)

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)`

affeldt-aist pushed 1 commit to branch maxr.

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

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

to `master`

:

Patch for math-comp/math-comp#516

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

to `master`

:

Patch for math-comp/math-comp#516

CohenCyril pushed 1 commit to branch maxr.

- Update config.nix (83bf207)

CohenCyril edited PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

CohenCyril deleted the branch ereal_pseudometric.

CohenCyril deleted the branch mathcomp_master_integration_ereal.

affeldt-aist pushed 1 commit to branch maxr.

- fix suggested by erik (46ea01c)

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

to `master`

:

Patch for math-comp/math-comp#516

CohenCyril edited PR #224 Integral sketch from `integral_sketch`

to `boole_inequality`

:

Depends on #223 (EDIT by Cyril)

CohenCyril submitted PR Review for #223 Boole inequality.

CohenCyril created PR Review Comment on #223 Boole inequality:

Unused

CohenCyril submitted PR Review for #223 Boole inequality.

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.

CohenCyril edited PR Review Comment on #223 Boole inequality.

CohenCyril submitted PR Review for #223 Boole inequality.

CohenCyril submitted PR Review for #223 Boole inequality.

CohenCyril created PR Review Comment on #223 Boole inequality:

I would prefer

`is_sigma_algebra`

.

CohenCyril created PR Review Comment on #223 Boole inequality:

rename

`le_measure`

CohenCyril created PR Review Comment on #223 Boole inequality:

and

`Notation MesurableMixin := Mixin`

.

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

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

- remove technical explanations about betas (4f39f26)

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

to `master`

.

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

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

to `master`

:

Patch for math-comp/math-comp#516

affeldt-aist pushed 1 commit to branch maxr.

- fix suggested by erik (701e73e)

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

to `master`

:

Patch for math-comp/math-comp#516

CohenCyril merged PR #226 Small renamings about expand.

CohenCyril pushed 2 commits to branch master.

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

CohenCyril deleted the branch renaming_le_expand.

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

to `master`

:

Patch for math-comp/math-comp#516

CohenCyril pushed 1 commit to branch maxr.

- Update .travis.yml (24e46c1)

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

to `master`

:

Patch for math-comp/math-comp#516

CohenCyril pushed 1 commit to branch maxr.

- Update config.nix (e3af28e)

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)

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

to `master`

:

Patch for math-comp/math-comp#516

CohenCyril pushed 1 commit to branch maxr.

- Adapting to new Order.max (e562b94)

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

to `master`

:

Patch for math-comp/math-comp#516

CohenCyril pushed 1 commit to branch maxr.

- Adapting to new Order.max (f30323e)

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

to `master`

:

Patch for math-comp/math-comp#516

CohenCyril merged PR #218 Adapting to new Order.max.

CohenCyril pushed 2 commits to branch master.

CohenCyril deleted the branch maxr.

CohenCyril updated PR #225 update INSTALL.md now that 1.11.0 has been released from `update_installmd_1.11`

to `master`

.

CohenCyril pushed 1 commit to branch update_installmd_1.11.

- Update INSTALL.md (5c11fdc)

**CohenCyril** has marked PR #225 as ready for review.

CohenCyril merged PR #225 update INSTALL.md now that 1.11.0 has been released.

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)

CohenCyril edited release MathComp Analysis 0.3.0 for tag 0.3.0.

CohenCyril released release MathComp Analysis 0.3.0 for tag 0.3.1.

CohenCyril created release MathComp Analysis 0.3.0 for tag 0.3.1.

CohenCyril published release MathComp Analysis 0.3.0 for tag 0.3.1.

CohenCyril pushed tag 0.3.1.

CohenCyril deleted release MathComp Analysis 0.3.0 for tag 0.3.1.

CohenCyril removed tag 0.3.1.

CohenCyril pushed 1 commit to branch changelog.

- preparing changelog (a37d394)

CohenCyril opened PR #227 preparing changelog from `changelog`

to `master`

.

CohenCyril updated PR #227 preparing changelog from `changelog`

to `master`

.

CohenCyril pushed 1 commit to branch changelog.

- fixup (d9923c2)

CohenCyril merged PR #227 preparing changelog.

CohenCyril pushed 1 commit to branch master.

- preparing changelog (#227) (c1ee376)

CohenCyril milestoned Issue #227 preparing changelog.

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)`

CohenCyril milestoned Issue #225 update INSTALL.md now that 1.11.0 has been released.

CohenCyril milestoned Issue #221 update to last version:

@mkerjean observed the

`INSTALL.md`

was a bit outdated.

CohenCyril milestoned Issue #219 rename lemmas for classical reasoning to avoid clash with fintype:

fixes #217

CohenCyril milestoned Issue #218 Adapting to new Order.max:

Patch for math-comp/math-comp#516

CohenCyril milestoned Issue #212 tentative changelog:

CohenCyril milestoned Issue #211 updating config.nix.

CohenCyril milestoned Issue #210 upgrading default.nix.

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.

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.

CohenCyril milestoned Issue #206 Add a distrLattice canonical structure to set T.

Hi,

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:

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.

CohenCyril milestoned Issue #183 LinearContinuousBounded:

These lemmas should maybe be rephrased using landau notations.

CohenCyril demilestoned Issue #197 contributing file:

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

CohenCyril milestoned Issue #197 contributing file:

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

CohenCyril demilestoned Issue #214 `locally`

better be renamed after neighborhoods:

replace

`locally`

by`nbhs`

?exception:

`bounded_locally`

in`normedmodtype.v`

CohenCyril milestoned Issue #214 `locally`

better be renamed after neighborhoods:

replace

`locally`

by`nbhs`

?exception:

`bounded_locally`

in`normedmodtype.v`

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#L199Remove the "'the" tag which makes things unreadable

https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L135

...

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#L199Remove the "'the" tag which makes things unreadable

https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L135

...

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`

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`

CohenCyril released release MathComp Analysis 0.3.1 for tag 0.3.1.

CohenCyril created release MathComp Analysis 0.3.1 for tag 0.3.1.

CohenCyril published release MathComp Analysis 0.3.1 for tag 0.3.1.

CohenCyril pushed tag 0.3.1.

affeldt-aist pushed 1 commit to branch ereal_ninfty_arithmetic.

- two lemmas about arithmetic with ninfty + typos in the documentation (dde0ca4)

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`

.

affeldt-aist pushed 2 commits to branch boole_inequality.

affeldt-aist updated PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

CohenCyril submitted PR Review for #222 two lemmas about arithmetic with ninfty + typos in the documentation.

CohenCyril merged PR #222 two lemmas about arithmetic with ninfty + typos in the documentation.

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)

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch ub_lb_renaming.

- rename the short
`ub`

and`lb`

to`ubound`

and`lbound`

(b8414e4)

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

affeldt-aist pushed 2 commits to branch more_sequences.

affeldt-aist updated PR #207 more lemmas about sequences from `more_sequences`

to `mathcomp_master_sequences`

:

It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for`sequences.v`

.

affeldt-aist edited PR #207 more lemmas about sequences from `more_sequences`

to `master`

:

It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for`sequences.v`

.

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)

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.

affeldt-aist deleted the branch ereal_ninfty_arithmetic.

affeldt-aist deleted the branch update_installmd_1.11.

affeldt-aist deleted the branch how-to-release.

affeldt-aist deleted the branch mathcomp_master_sequences.

affeldt-aist deleted the branch changelog.

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)

affeldt-aist updated PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

CohenCyril created PR Review Comment on #223 Boole inequality:

Maybe

`Theorem Boole_inequality`

instead. Otherwise by convention`bool`

means`bool : Type`

CohenCyril submitted PR Review for #223 Boole inequality.

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)

affeldt-aist updated PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

affeldt-aist pushed 1 commit to branch boole_inequality.

- wip (3e040e6)

affeldt-aist updated PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

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)

affeldt-aist updated PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

affeldt-aist opened Issue #228 move to boolp:

`forallN`

,`eqNNP`

, and`existsN`

fromshould be moved to

`boolp.v`

near`existsPN`

,`existsNP`

.`forallNP`

,`forallPN`

Wanted: better names.

affeldt-aist labeled Issue #228 move to boolp:

`forallN`

,`eqNNP`

, and`existsN`

fromshould be moved to

`boolp.v`

near`existsPN`

,`existsNP`

.`forallNP`

,`forallPN`

Wanted: better names.

affeldt-aist labeled Issue #228 move to boolp:

`forallN`

,`eqNNP`

, and`existsN`

fromshould be moved to

`boolp.v`

near`existsPN`

,`existsNP`

.`forallNP`

,`forallPN`

Wanted: better names.

affeldt-aist unlabeled Issue #228 move to boolp:

`forallN`

,`eqNNP`

, and`existsN`

fromshould be moved to

`boolp.v`

near`existsPN`

,`existsNP`

.`forallNP`

,`forallPN`

Wanted: better names.

affeldt-aist labeled Issue #228 move to boolp:

`forallN`

,`eqNNP`

, and`existsN`

fromshould be moved to

`boolp.v`

near`existsPN`

,`existsNP`

.`forallNP`

,`forallPN`

Wanted: better names.

affeldt-aist milestoned Issue #228 move to boolp:

`forallN`

,`eqNNP`

, and`existsN`

fromshould be moved to

`boolp.v`

near`existsPN`

,`existsNP`

.`forallNP`

,`forallPN`

Wanted: better names.

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch boole_inequality.

- cosmetics (410d110)

affeldt-aist updated PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

CohenCyril merged PR #220 rename the short `ub`

and `lb`

to `ubound`

and `lbound`

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)

affeldt-aist:

- created 2020 06 17 Meeting

affeldt-aist:

- edited Home

CohenCyril submitted PR Review for #223 Boole inequality.

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`

.

CohenCyril submitted PR Review for #223 Boole inequality.

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)

CohenCyril submitted PR Review for #223 Boole inequality.

CohenCyril created PR Review Comment on #223 Boole inequality:

`lee_mu_ext`

CohenCyril edited PR Review Comment on #223 Boole inequality.

CohenCyril submitted PR Review for #223 Boole inequality.

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.

CohenCyril submitted PR Review for #223 Boole inequality.

CohenCyril created PR Review Comment on #223 Boole inequality:

I would name it

`cvg_mu_inc`

.

CohenCyril submitted PR Review for #223 Boole inequality.

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`

)

CohenCyril submitted PR Review for #223 Boole inequality.

CohenCyril created PR Review Comment on #223 Boole inequality:

@affeldt-aist I would vouch for cutting here for this PR.

affeldt-aist pushed 1 commit to branch fixes_228.

- renaming of lemmas for classical reasoning (ecd914f)

affeldt-aist opened PR #229 renaming of lemmas for classical reasoning from `fixes_228`

to `master`

:

fixes #228

affeldt-aist:

- edited 2020 06 17 Meeting

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)

affeldt-aist updated PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

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)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `boole_inequality`

:

Depends on #223 (EDIT by Cyril)

affeldt-aist pushed 1 commit to branch contributing_guide.

- naming convention about homo/mono lemmas (01e58b8)

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.

pi8027 opened PR #230 Fix inheritance from pseudoMetricNormedZmodType to completeNormedModType from `fix-inheritance`

to `master`

.

affeldt-aist deleted the branch ub_lb_renaming.

affeldt-aist:

- edited Home

CohenCyril merged PR #230 Fix inheritance from pseudoMetricNormedZmodType to completeNormedModType.

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)

affeldt-aist deleted the branch mathcomp_master_integration.

affeldt-aist deleted the branch mathcomp_master.

CohenCyril submitted PR Review for #229 renaming of lemmas for classical reasoning.

CohenCyril created PR Review Comment on #229 renaming of lemmas for classical reasoning:

`Lemma not_forallP T (P : T -> Prop) :`

CohenCyril submitted PR Review for #229 renaming of lemmas for classical reasoning.

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.

affeldt-aist pushed 1 commit to branch fixes_228.

- renaming of lemmas for classical reasoning (7c59b85)

affeldt-aist updated PR #229 renaming of lemmas for classical reasoning from `fixes_228`

to `master`

:

fixes #228

CohenCyril submitted PR Review for #223 Boole inequality.

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 :`

CohenCyril submitted PR Review for #223 Boole inequality.

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} ->`

CohenCyril edited PR Review Comment on #223 Boole inequality.

CohenCyril submitted PR Review for #229 renaming of lemmas for classical reasoning.

CohenCyril created PR Review Comment on #229 renaming of lemmas for classical reasoning:

(and add it to the changelog ;))

affeldt-aist pushed 1 commit to branch fixes_228.

- renaming of lemmas for classical reasoning (6d3990d)

affeldt-aist updated PR #229 renaming of lemmas for classical reasoning from `fixes_228`

to `master`

:

fixes #228

affeldt-aist pushed 1 commit to branch boole_inequality.

- improved presentation (1785dfe)

affeldt-aist updated PR #223 Boole inequality from `boole_inequality`

to `master`

:

Tentative formalization of Boole's inequality (wip).

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`

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)

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

to `master`

:

Further generalisations from normedModTypes to PseudoMetricNormedZmodTypes.

affeldt-aist pushed 2 commits to branch more_sequences.

affeldt-aist updated PR #207 more lemmas about sequences from `more_sequences`

to `master`

:

It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for`sequences.v`

.

affeldt-aist closed without merge PR #137 integral.v draft.

CohenCyril merged PR #223 Boole inequality.

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)

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.

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.

affeldt-aist pushed 1 commit to branch rename_locally.

- rename "locally" to "nbhs" and propagate (fa0566a)

affeldt-aist pushed 1 commit to branch rename_locally.

- rename "locally" to "nbhs" and propagate (9ec416b)

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)

pi8027 opened PR #234 Get rid of filter_index_enum from `remove-filter_index_enum`

to `master`

:

Closes #231

pi8027 updated PR #234 Get rid of filter_index_enum from `remove-filter_index_enum`

to `master`

:

Closes #231

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

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`

CohenCyril merged PR #234 Get rid of deprecated lemmas filter_index_enum, uniq_perm_eq, and perm_eq_small.

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)

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.

affeldt-aist pushed 1 commit to branch rename_locally.

- remote more "locally" into "nbhs" and propagate (dd46b4d)

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)

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

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.

affeldt-aist merged PR #235 Fix links of projects moved to coq-community.

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

- Fix links of projects moved to coq-community. (b8d9c78)

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)

mkerjean updated PR #205 Topological structures on numfields from `numfield_topology`

to `master`

:

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)]

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

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

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

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

This is wrong.

`pseudoMetric_of_normedDomain`

produces a mixin, not a structure instance.

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.

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

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.

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

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]].`

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

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.

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

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

Indeed, thanks.

mkerjean edited PR Review Comment on #205 Topological structures on numfields.

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

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 ?

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

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.

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

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.

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

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].`

pi8027 edited PR Review Comment on #205 Topological structures on numfields.

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

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.

pi8027 edited PR Review Comment on #205 Topological structures on numfields.

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

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

@pi8027 spot on!

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

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.

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

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?)

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

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

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.

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

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 ?

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

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 ?

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

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.

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

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

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.

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

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.

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

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 ?

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

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).

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

CohenCyril edited PR Review Comment on #205 Topological structures on numfields.

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

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

Isn't there a risk that defining the topology using the

`^o`

would still leads to an iteration of the`^o`

in the types of objects handled ?

mkerjean deleted PR Review Comment on #205 Topological structures on numfields.

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

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

Using

`^o`

as an intermediate object to declare these canonicals makes sure that they are convertible with the "regular" instances, and, FYI, with PR math-comp/math-comp#545, we can write:`Canonical numField_fieldExtType (K : numFieldType) := [fieldExtType K of K].`

pi8027 edited PR Review Comment on #205 Topological structures on numfields.

mkerjean pushed 1 commit to branch holomorphy.

- clean (e2bab6f)

mkerjean updated PR #204 Holomorphy from `holomorphy`

to `master`

:

Formalization of complex analysis, following the closed #192.

mkerjean pushed 1 commit to branch numfield_topology.

- numfield_lmod from regular (f09ae2b)

mkerjean updated PR #205 Topological structures on numfields from `numfield_topology`

to `master`

:

mkerjean pushed 1 commit to branch numfield_topology.

- canonical and coercions for numfield (db2628f)

mkerjean updated PR #205 Topological structures on numfields from `numfield_topology`

to `master`

:

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

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

So we have the following ambiguous paths here:

`New coercion path [numField_comAlgType; GRing.ComAlgebra.comRingType] : Num.NumField.type >-> GRing.ComRing.type is ambiguous with existing [Num.NumField.comRingType] : Num.NumField.type >-> GRing.ComRing.type. [ambiguous-paths,typechecker]`

I think the problem is twofold:

`regular_comRingType`

uses`GRing.mulrC`

, which is opaque.- Since
`lalgType`

and its subclasses do not take the ring structures as their base, an eta expansion appears in the former path.

pi8027 edited PR Review Comment on #205 Topological structures on numfields.

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

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

FYI, I'm working on a fix of this issue on the MathComp side, which subsumes math-comp/math-comp#545 and math-comp/math-comp#546.

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

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

Now math-comp/math-comp#546 solves this issue. Adding 54 implicit coercions from

`numFieldType`

and its subclasses to`fieldExtType`

and its superclasses does not introduce any ambiguous path.

pi8027 edited PR Review Comment on #205 Topological structures on numfields.

pi8027 edited PR Review Comment on #205 Topological structures on numfields.

CohenCyril submitted PR Review for #233 rename "locally" to "nbhs" and propagate.

CohenCyril submitted PR Review for #233 rename "locally" to "nbhs" and propagate.

CohenCyril created PR Review Comment on #233 rename "locally" to "nbhs" and propagate:

`nbhsW`

->`nearW`

(the current`nearW`

is internal and could be renamed`near_skip_subproof`

.

Indeed this lemma has nothing to do with neighborhoods.

CohenCyril created PR Review Comment on #233 rename "locally" to "nbhs" and propagate:

`loc`

->`nbhs`

CohenCyril created PR Review Comment on #233 rename "locally" to "nbhs" and propagate:

`prod_loc`

->`prod_nbhs`

CohenCyril created PR Review Comment on #233 rename "locally" to "nbhs" and propagate:

`neigh`

->`open_nbhs`

CohenCyril created PR Review Comment on #233 rename "locally" to "nbhs" and propagate:

`loc`

->`nbhs`

CohenCyril edited PR Review Comment on #233 rename "locally" to "nbhs" and propagate.

CohenCyril edited PR Review Comment on #233 rename "locally" to "nbhs" and propagate.

CohenCyril edited PR Review Comment on #233 rename "locally" to "nbhs" and propagate.

CohenCyril edited PR Review Comment on #233 rename "locally" to "nbhs" and propagate.

affeldt-aist pushed 3 commits to branch integral_sketch.

- more technical lemmas about extended numbers' arithmetic (38686d0)
- lemmas about supremum and supremums (3e27272)
- proposition about caratheodory mesurable (wip, first part) (1a6ccc4)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `boole_inequality`

:

Depends on #223 (EDIT by Cyril)

affeldt-aist pushed 5 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (5ca4486)
- tentative definition of outer measure and basic properties (ebd77fb)
- more technical lemmas about extended numbers' arithmetic (08bea3e)
- lemmas about supremum and supremums (2fc75fc)
- proposition about caratheodory mesurable (wip, first part) (efd6792)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `boole_inequality`

:

Depends on #223 (EDIT by Cyril)

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch rename_locally.

- address comments by Cyril (4ad1a42)

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)

affeldt-aist pushed 2 commits to branch rename_locally.

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)

affeldt-aist edited PR #233 rename "locally" to "nbhs" and propagate from `rename_locally`

to `master`

:

fixes #214

(there are remaining occurrences in unused definitions)

affeldt-aist:

- edited Home

affeldt-aist:

- edited Home

affeldt-aist deleted the branch nix.

affeldt-aist pushed 1 commit to branch ereal_arith_20200720.

- more technical lemmas about extended numbers' arithmetic (56a1d09)

affeldt-aist opened PR #236 more technical lemmas about extended numbers' arithmetic from `ereal_arith_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist pushed 1 commit to branch supremum_20200720.

- lemmas about supremum and supremums (817ba17)

affeldt-aist opened PR #237 lemmas about supremum and supremums from `supremum_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist merged PR #216 Improve documentation of landau.v.

affeldt-aist pushed 1 commit to branch master.

- addition to the documentation of landau.v (6d7a134)

affeldt-aist deleted the branch issue103_fix.

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch fixes_228.

- renaming of lemmas for classical reasoning (49f0559)

affeldt-aist updated PR #229 renaming of lemmas for classical reasoning from `fixes_228`

to `master`

:

fixes #228

affeldt-aist closed Issue #228 move to boolp:

`forallN`

,`eqNNP`

, and`existsN`

fromshould be moved to

`boolp.v`

near`existsPN`

,`existsNP`

.`forallNP`

,`forallPN`

Wanted: better names.

affeldt-aist merged PR #229 renaming of lemmas for classical reasoning.

affeldt-aist pushed 1 commit to branch master.

- renaming of lemmas for classical reasoning (3d82bae)

affeldt-aist deleted the branch fixes_228.

affeldt-aist:

- edited Home

affeldt-aist edited PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril)

affeldt-aist pushed 5 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (4578b4f)
- tentative definition of outer measure and basic properties (d993615)
- more technical lemmas about extended numbers' arithmetic (024a177)
- lemmas about supremum and supremums (edc7b09)
- proposition about caratheodory mesurable (114033e)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril)

affeldt-aist pushed 1 commit to branch ereal_arith_20200720.

- more technical lemmas about extended numbers' arithmetic (f5d2f03)

affeldt-aist updated PR #236 more technical lemmas about extended numbers' arithmetic from `ereal_arith_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist pushed the branch classical_sets_20200722.

affeldt-aist pushed 1 commit to branch classical_sets_20200722.

- move lemmas from measure.v to classical_sets.v (6f38d23)

affeldt-aist opened PR #238 move lemmas from measure.v to classical_sets.v from `classical_sets_20200722`

to `master`

.

affeldt-aist pushed 1 commit to branch integral_sketch.

- tentative caratheodory theorem (wip) (06eae34)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril)

affeldt-aist edited PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist edited PR #238 move lemmas from measure.v to classical_sets.v from `classical_sets_20200722`

to `master`

:

This is harmless (it just moves a few things to more appropriate locations).

affeldt-aist merged PR #238 move lemmas from measure.v to classical_sets.v.

affeldt-aist pushed 1 commit to branch master.

- move lemmas from measure.v to classical_sets.v (bff2725)

affeldt-aist deleted the branch classical_sets_20200722.

affeldt-aist pushed 7 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (de22b70)
- tentative definition of outer measure and basic properties (f1b957a)
- more technical lemmas about extended numbers' arithmetic (c9022b7)
- lemmas about supremum and supremums (0b40736)
- proposition about caratheodory mesurable (c8fc8fc)
- tentative caratheodory theorem (wip) (b39c870)
- wip (1ffb6b1)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch integral_sketch.

- tentative caratheodory theorem (wip) (e070f98)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist deleted the branch boole_inequality.

affeldt-aist:

- created 2020 07 24 Meeting

affeldt-aist:

- edited Home

affeldt-aist:

- edited 2020 07 24 Meeting

affeldt-aist:

- edited 2020 07 24 Meeting

affeldt-aist pushed 1 commit to branch integral_sketch.

- tentative caratheodory theorem (wip) (14487e9)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch rename_locally.

- lemma open_nbhsE (4807577)

`rename_locally`

to `master`

:

fixes #214

(there are remaining occurrences in unused definitions)

affeldt-aist pushed 3 commits to branch rename_locally.

- rename "locally" to "nbhs" and propagate (ae58892)
- address comments by Cyril (66529f2)
- lemma open_nbhsE (88dae63)

`rename_locally`

to `master`

:

fixes #214

(there are remaining occurrences in unused definitions)

affeldt-aist pushed 2 commits to branch integral_sketch.

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch integral_sketch.

- wip (a4007e2)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 2 commits to branch more_sequences.

affeldt-aist updated PR #207 more lemmas about sequences from `more_sequences`

to `master`

:

It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for`sequences.v`

.

affeldt-aist pushed the branch sequences_20200726.

affeldt-aist pushed 1 commit to branch sequences_20200726.

- small theory about arithmetic and geometric sequences (77fbfd5)

affeldt-aist opened PR #239 small theory about arithmetic and geometric sequences from `sequences_20200726`

to `master`

:

I would like to have these lemmas from the branch

`more_sequences`

merged into master for use in the branch`integral_sketch`

@CohenCyril

affeldt-aist pushed 1 commit to branch sequences_20200726.

- update changelog (2e5d3e1)

affeldt-aist updated PR #239 small theory about arithmetic and geometric sequences from `sequences_20200726`

to `master`

:

I would like to have these lemmas from the branch

`more_sequences`

merged into master for use in the branch`integral_sketch`

@CohenCyril

affeldt-aist pushed 1 commit to branch classical_sets_20200726.

- more lemmas about classical sets (following the naming convention of (c3d2add)

affeldt-aist opened PR #240 more lemmas about classical sets from `classical_sets_20200726`

to `master`

:

I would like to have these lemmas in master for use in the

`integral_sketch`

branch.

(Naming convention and order of appearance in the file is guided by`finset.v`

.)

affeldt-aist pushed 1 commit to branch ereal_arith_20200720.

- even more lemmas about extended real numbers' arithmetic (4c1a939)

affeldt-aist updated PR #236 more technical lemmas about extended numbers' arithmetic from `ereal_arith_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist milestoned Issue #240 more lemmas about classical sets:

I would like to have these lemmas in master for use in the

`integral_sketch`

branch.

(Naming convention and order of appearance in the file is guided by`finset.v`

.)

affeldt-aist milestoned Issue #239 small theory about arithmetic and geometric sequences:

I would like to have these lemmas from the branch

`more_sequences`

merged into master for use in the branch`integral_sketch`

@CohenCyril

affeldt-aist milestoned Issue #237 lemmas about supremum and supremums:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist milestoned Issue #236 more technical lemmas about extended numbers' arithmetic:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist milestoned Issue #233 rename "locally" to "nbhs" and propagate:

fixes #214

(there are remaining occurrences in unused definitions)

affeldt-aist pushed 1 commit to branch compatibility_coq_8_12.

- compatibility with coq 8.12 (04197b7)

affeldt-aist opened PR #241 compatibility with coq 8.12 from `compatibility_coq_8_12`

to `master`

:

This is to fix a compatibility problem with Coq 8.12 observed by Karl.

affeldt-aist milestoned Issue #241 compatibility with coq 8.12:

This is to fix a compatibility problem with Coq 8.12 observed by Karl.

affeldt-aist pushed 1 commit to branch integral_sketch.

- tentative caratheodory theorem (wip) (4d19407)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch integral_sketch.

- trying to isolate issue with definitions (70d6f18)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch integral_sketch.

- fix (da6b409)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

CohenCyril submitted PR Review for #240 more lemmas about classical sets.

CohenCyril created PR Review Comment on #240 more lemmas about classical sets:

`- by right; exists m => //; rewrite addSnnS.`

CohenCyril submitted PR Review for #240 more lemmas about classical sets.

CohenCyril created PR Review Comment on #240 more lemmas about classical sets:

`- by exists i.+1 => //; rewrite -addSnnS.`

CohenCyril pushed 1 commit to branch classical_sets_20200726.

- Apply suggestions from code review (051b3a6)

CohenCyril updated PR #240 more lemmas about classical sets from `classical_sets_20200726`

to `master`

:

I would like to have these lemmas in master for use in the

`integral_sketch`

branch.

(Naming convention and order of appearance in the file is guided by`finset.v`

.)

CohenCyril submitted PR Review for #236 more technical lemmas about extended numbers' arithmetic.

CohenCyril submitted PR Review for #241 compatibility with coq 8.12.

CohenCyril created PR Review Comment on #241 compatibility with coq 8.12:

@affeldt-aist I wonder if this still compiles with Coq 8.10 and 8.11

CohenCyril created PR Review Comment on #241 compatibility with coq 8.12:

AFAIK Coq < 8.10 is not supported anymore

CohenCyril submitted PR Review for #241 compatibility with coq 8.12.

CohenCyril submitted PR Review for #233 rename "locally" to "nbhs" and propagate.

CohenCyril closed Issue #214 `locally`

better be renamed after neighborhoods:

replace

`locally`

by`nbhs`

?exception:

`bounded_locally`

in`normedmodtype.v`

CohenCyril merged PR #233 rename "locally" to "nbhs" and propagate.

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

- rename "locally" to "nbhs" and propagate (ae58892)
- address comments by Cyril (66529f2)
- lemma open_nbhsE (88dae63)
- Merge pull request #233 from math-comp/rename_locally (0c5f403)

CohenCyril submitted PR Review for #240 more lemmas about classical sets.

affeldt-aist submitted PR Review for #241 compatibility with coq 8.12.

affeldt-aist created PR Review Comment on #241 compatibility with coq 8.12:

It went through. But we'd better get rid of it.

CohenCyril submitted PR Review for #241 compatibility with coq 8.12.

CohenCyril created PR Review Comment on #241 compatibility with coq 8.12:

Sorry, I meant: does removing this still make Coq 8.10 pass?

affeldt-aist created PR Review Comment on #241 compatibility with coq 8.12:

I think so: https://travis-ci.org/github/math-comp/analysis/jobs/711965366.

affeldt-aist submitted PR Review for #241 compatibility with coq 8.12.

affeldt-aist pushed 1 commit to branch compatibility_coq_8_12.

- restrict to Coq 8.10 and add Coq 8.12 to travis (f22b44d)

affeldt-aist updated PR #241 compatibility with coq 8.12 from `compatibility_coq_8_12`

to `master`

:

This is to fix a compatibility problem with Coq 8.12 observed by Karl.

affeldt-aist pushed 1 commit to branch classical_sets_20200726.

- more lemmas about classical sets (following the naming convention of (cc2edd7)

affeldt-aist updated PR #240 more lemmas about classical sets from `classical_sets_20200726`

to `master`

:

`integral_sketch`

branch.

(Naming convention and order of appearance in the file is guided by`finset.v`

.)

affeldt-aist deleted the branch rename_locally.

affeldt-aist demilestoned Issue #183 LinearContinuousBounded:

These lemmas should maybe be rephrased using landau notations.

affeldt-aist milestoned Issue #183 LinearContinuousBounded:

These lemmas should maybe be rephrased using landau notations.

CohenCyril merged PR #240 more lemmas about classical sets.

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

- more lemmas about classical sets (following the naming convention of (cc2edd7)
- Merge pull request #240 from math-comp/classical_sets_20200726 (0deb153)

CohenCyril submitted PR Review for #241 compatibility with coq 8.12.

affeldt-aist pushed 2 commits to branch compatibility_coq_8_12.

affeldt-aist updated PR #241 compatibility with coq 8.12 from `compatibility_coq_8_12`

to `master`

:

This is to fix a compatibility problem with Coq 8.12 observed by Karl.

affeldt-aist deleted the branch classical_sets_20200726.

affeldt-aist pushed 2 commits to branch ereal_arith_20200720.

- more technical lemmas about extended numbers' arithmetic (6640575)
- even more lemmas about extended real numbers' arithmetic (504bb6d)

affeldt-aist updated PR #236 more technical lemmas about extended numbers' arithmetic from `ereal_arith_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

CohenCyril merged PR #241 compatibility with coq 8.12.

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

- compatibility with coq 8.12 (8ce3ddb)
- restrict to Coq 8.10 and add Coq 8.12 to travis (64f2f5e)
- Merge pull request #241 from math-comp/compatibility_coq_8_12 (b8595a1)

affeldt-aist merged PR #236 more technical lemmas about extended numbers' arithmetic.

affeldt-aist pushed 2 commits to branch master.

- more technical lemmas about extended numbers' arithmetic (1ee28be)
- even more lemmas about extended real numbers' arithmetic (8ecb24b)

affeldt-aist deleted the branch ereal_arith_20200720.

affeldt-aist pushed 5 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (63321f5)
- tentative definition of outer measure and basic properties (477dd07)
- lemmas about supremum and supremums (93d655f)
- proposition about caratheodory mesurable (3c9ca47)
- tentative caratheodory theorem (first part) (7b3f296)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

CohenCyril pushed 1 commit to branch sequences_20200726.

- simplifications, extensions, generalizations, fixups, renamings (58ed0d5)

CohenCyril updated PR #239 small theory about arithmetic and geometric sequences from `sequences_20200726`

to `master`

:

`more_sequences`

merged into master for use in the branch`integral_sketch`

@CohenCyril

CohenCyril pushed 1 commit to branch sequences_20200726.

- simplifications, extensions, generalizations, fixups, renamings (1d31824)

CohenCyril updated PR #239 small theory about arithmetic and geometric sequences from `sequences_20200726`

to `master`

:

`more_sequences`

merged into master for use in the branch`integral_sketch`

@CohenCyril

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

- small theory about arithmetic and geometric sequences (c892150)
- simplifications, extensions, generalizations, fixups, renamings (205dba0)

CohenCyril updated PR #239 small theory about arithmetic and geometric sequences from `sequences_20200726`

to `master`

:

`more_sequences`

merged into master for use in the branch`integral_sketch`

@CohenCyril

CohenCyril pushed 1 commit to branch sequences_20200726.

- simplifications, extensions, generalizations, fixups, renamings (f76f033)

`sequences_20200726`

to `master`

:

`more_sequences`

merged into master for use in the branch`integral_sketch`

@CohenCyril

CohenCyril submitted PR Review for #239 small theory about arithmetic and geometric sequences.

CohenCyril pushed 1 commit to branch sequences_20200726.

- simplifications, extensions, generalizations, fixups, renamings (cc6a155)

`sequences_20200726`

to `master`

:

`more_sequences`

merged into master for use in the branch`integral_sketch`

@CohenCyril

affeldt-aist merged PR #239 small theory about arithmetic and geometric sequences.

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

- small theory about arithmetic and geometric sequences (26654a7)
- simplifications, extensions, generalizations, fixups, renamings (93084ac)

affeldt-aist pushed 1 commit to branch more_sequences.

- Examples of sequences and series (e2c81d1)

affeldt-aist updated PR #207 more lemmas about sequences from `more_sequences`

to `master`

:

It defines a few standard sequences and proves a few lemmas about them, mostly as a test bed for`sequences.v`

.

affeldt-aist pushed 6 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (c0e63aa)
- tentative definition of outer measure and basic properties (f301062)
- lemmas about supremum and supremums (9145578)
- proposition about caratheodory mesurable (e9ad24e)
- tentative caratheodory theorem (first part) (e025771)
- wip (3a4c7c0)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch integral_sketch.

- wip (fafd947)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

drouhling pushed 1 commit to branch uniform_spaces.

- Insert a structure of uniform space (02b0765)

drouhling opened PR #242 Insert a structure of uniform space from `uniform_spaces`

to `master`

:

This is meant to replace #119.

Some lemmas can be generalised (from pseudometric to uniform) as in #119 but this should be in another PR.

drouhling closed without merge PR #119 Replace balls with entourages.

drouhling pushed 1 commit to branch uniform_spaces.

- Update documentation (ceee447)

drouhling updated PR #242 Insert a structure of uniform space from `uniform_spaces`

to `master`

:

This is meant to replace #119.

Some lemmas can be generalised (from pseudometric to uniform) as in #119 but this should be in another PR.

affeldt-aist pushed 1 commit to branch integral_sketch.

- tentative caratheodory theorem (aba1d6e)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch measure_minor_cleaning.

- minor fix, generalizations, cleaning (fe461a1)

affeldt-aist opened PR #243 minor fix, generalizations, cleaning from `measure_minor_cleaning`

to `master`

:

Harmless improvement in preparation for more PRs on the topic. @CohenCyril

affeldt-aist pushed 1 commit to branch measure_minor_cleaning.

- update changelog (b8ea635)

affeldt-aist updated PR #243 minor fix, generalizations, cleaning from `measure_minor_cleaning`

to `master`

:

Harmless improvement in preparation for more PRs on the topic. @CohenCyril

affeldt-aist pushed 1 commit to branch ereal_minor_cleaning.

- minor change to ereal (d0246ed)

affeldt-aist opened PR #244 minor change to ereal from `ereal_minor_cleaning`

to `master`

:

again small localized changes:

- renaming
- remove useless uses of notation scopes
- remove lemma subsumed by mathcomp 1.11

affeldt-aist deleted the branch sequences_20200726.

affeldt-aist deleted the branch compatibility_coq_8_12.

affeldt-aist deleted the branch integral_draft.

pi8027 submitted PR Review for #242 Insert a structure of uniform space.

pi8027 submitted PR Review for #242 Insert a structure of uniform space.

pi8027 created PR Review Comment on #242 Insert a structure of uniform space:

IIUC, since this (as a function) returns a

`completeType`

instance, the current naming convention is that it should be named`pseudoMetric_completeType`

.

pi8027 created PR Review Comment on #242 Insert a structure of uniform space:

A coercion from

`CompleteNormedModule`

classes to`CompletePseudoMetric`

classes should be declared to get rid of`CompletePseudoMetric.Class`

here.

drouhling pushed 4 commits to branch uniform_spaces.

- Update changelog (e24d851)
- Follow naming convention (4ff7fd3)
- Add missing joins (6e260fa)
- Update uniform_bigO.v (7c96c57)

drouhling updated PR #242 Insert a structure of uniform space from `uniform_spaces`

to `master`

:

This is meant to replace #119.

Some lemmas can be generalised (from pseudometric to uniform) as in #119 but this should be in another PR.

drouhling submitted PR Review for #242 Insert a structure of uniform space.

drouhling created PR Review Comment on #242 Insert a structure of uniform space:

Done.

drouhling submitted PR Review for #242 Insert a structure of uniform space.

drouhling created PR Review Comment on #242 Insert a structure of uniform space:

Done.

pi8027 edited PR Review Comment on #242 Insert a structure of uniform space.

affeldt-aist pushed 2 commits to branch integral_sketch_hb.

CohenCyril submitted PR Review for #242 Insert a structure of uniform space.

CohenCyril created PR Review Comment on #242 Insert a structure of uniform space:

`flim`

prefix has been renamed to`cvg`

as per #193

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?

drouhling pushed 1 commit to branch uniform_spaces.

- Replace flim with cvg (be176e2)

drouhling updated PR #242 Insert a structure of uniform space from `uniform_spaces`

to `master`

:

This is meant to replace #119.

drouhling submitted PR Review for #242 Insert a structure of uniform space.

drouhling created PR Review Comment on #242 Insert a structure of uniform space:

Indeed. I forgot to update my old code. It's done now.

affeldt-aist pushed 1 commit to branch integral_sketch_hb.

- add ring of sets, etc. using hierarchy builder (wip) (1ccf16d)

CohenCyril merged PR #242 Insert a structure of uniform space.

CohenCyril pushed 8 commits to branch master. Commits by drouhling (7) and CohenCyril (1).

- Insert a structure of uniform space (02b0765)
- Update documentation (ceee447)
- Update changelog (e24d851)
- Follow naming convention (4ff7fd3)
- Add missing joins (6e260fa)
- Update uniform_bigO.v (7c96c57)
- Replace flim with cvg (be176e2)
- Merge pull request #242 from math-comp/uniform_spaces (70d5c47)

affeldt-aist pushed 1 commit to branch integral_sketch_hb.

- wip (b871696)

affeldt-aist pushed 1 commit to branch ereal_minor_cleaning.

- minor change to ereal (1e6ac8c)

affeldt-aist updated PR #244 minor change to ereal from `ereal_minor_cleaning`

to `master`

:

again small localized changes:

- renaming
- remove useless uses of notation scopes
- remove lemma subsumed by mathcomp 1.11

affeldt-aist pushed 2 commits to branch measure_minor_cleaning.

affeldt-aist updated PR #243 minor fix, generalizations, cleaning from `measure_minor_cleaning`

to `master`

:

Harmless improvement in preparation for more PRs on the topic. @CohenCyril

affeldt-aist pushed 1 commit to branch supremum_20200720.

- lemmas about supremum and supremums (1404d9e)

affeldt-aist updated PR #237 lemmas about supremum and supremums from `supremum_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

drouhling pushed 2 commits to branch uniform_spaces. Commits by CohenCyril (1) and drouhling (1).

- Merge pull request #242 from math-comp/uniform_spaces (70d5c47)
- Generalise closeness properties to uniform spaces (7daf09c)

drouhling opened PR #245 Generalise closeness properties to uniform spaces from `uniform_spaces`

to `master`

:

As promised in #242 this PR generalises a few lemmas from

`pseudoMetricType`

to`uniformType`

.

drouhling pushed 1 commit to branch uniform_spaces.

- Generalise continuous_withinNx (26417e2)

drouhling updated PR #245 Generalise closeness properties to uniform spaces from `uniform_spaces`

to `master`

:

As promised in #242 this PR generalises a few lemmas from

`pseudoMetricType`

to`uniformType`

.

drouhling edited PR #245 Generalise properties from pseudo metric to uniform spaces from `uniform_spaces`

to `master`

:

As promised in #242 this PR generalises a few lemmas from

`pseudoMetricType`

to`uniformType`

.

drouhling pushed 1 commit to branch clean_real_dep.

- Move stdlib-related code to Rbar/Rstruct (dd0b4e9)

drouhling opened PR #246 Move stdlib-related code to Rbar/Rstruct from `clean_real_dep`

to `master`

:

This PR removes the dependency on stdlib's reals from the main parts of the library.

affeldt-aist pushed 1 commit to branch supremum_20200720.

- lemmas about supremum and supremums (4a752f9)

affeldt-aist updated PR #237 lemmas about supremum and supremums from `supremum_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist pushed 1 commit to branch integral_sketch_hb.

- a few easy admits remaining from work with Cyril (902c0fb)

CohenCyril submitted PR Review for #237 lemmas about supremum and supremums.

CohenCyril created PR Review Comment on #237 lemmas about supremum and supremums:

I'd rather swap the last two arguments:

`E t -> (supremum x0 E >= t)%O`

and use a`contra_notN`

lemma to finish the job.

Maybe we should also envision adding`contra_not_le`

etc lemmas

CohenCyril edited PR Review Comment on #237 lemmas about supremum and supremums.

CohenCyril submitted PR Review for #237 lemmas about supremum and supremums.

CohenCyril created PR Review Comment on #237 lemmas about supremum and supremums:

shouldn't there be the same for "infimum"?

CohenCyril submitted PR Review for #245 Generalise properties from pseudo metric to uniform spaces.

CohenCyril milestoned Issue #244 minor change to ereal:

again small localized changes:

- renaming
- remove useless uses of notation scopes
- remove lemma subsumed by mathcomp 1.11

CohenCyril merged PR #244 minor change to ereal.

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

- minor change to ereal (1e6ac8c)
- Merge pull request #244 from math-comp/ereal_minor_cleaning (bd0a45b)

CohenCyril merged PR #246 Move stdlib-related code to Rbar/Rstruct.

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and drouhling (1).

- Move stdlib-related code to Rbar/Rstruct (dd0b4e9)
- Merge pull request #246 from math-comp/clean_real_dep (8dd824e)

CohenCyril milestoned Issue #246 Move stdlib-related code to Rbar/Rstruct:

This PR removes the dependency on stdlib's reals from the main parts of the library.

CohenCyril milestoned Issue #232 Generalize prod_pseudoMetricNormedZmodType:

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.

CohenCyril merged PR #232 Generalize prod_pseudoMetricNormedZmodType.

CohenCyril pushed 2 commits to branch master. Commits by CohenCyril (1) and pi8027 (1).

- Generalize prod_pseudoMetricNormedZmodType (2b42967)
- Merge pull request #232 from pi8027/prod_pseudoMetricNormedZmodType (d1c38a2)

CohenCyril pushed 2 commits to branch uniform_spaces. Commits by drouhling (2).

- Generalise closeness properties to uniform spaces (d3e4c78)
- Generalise continuous_withinNx (c07d14a)

CohenCyril updated PR #245 Generalise properties from pseudo metric to uniform spaces from `uniform_spaces`

to `master`

:

As promised in #242 this PR generalises a few lemmas from

`pseudoMetricType`

to`uniformType`

.

CohenCyril merged PR #245 Generalise properties from pseudo metric to uniform spaces.

CohenCyril pushed 3 commits to branch master. Commits by drouhling (2) and CohenCyril (1).

- Generalise closeness properties to uniform spaces (d3e4c78)
- Generalise continuous_withinNx (c07d14a)
- Merge pull request #245 from math-comp/uniform_spaces (1b1c6be)

CohenCyril milestoned Issue #245 Generalise properties from pseudo metric to uniform spaces:

As promised in #242 this PR generalises a few lemmas from

`pseudoMetricType`

to`uniformType`

.

CohenCyril pushed 10 commits to branch measure_minor_cleaning. Commits by CohenCyril (5), drouhling (3), affeldt-aist (1) and others (1).

- Generalize prod_pseudoMetricNormedZmodType (2b42967)
- minor change to ereal (1e6ac8c)
- Move stdlib-related code to Rbar/Rstruct (dd0b4e9)
- Merge pull request #244 from math-comp/ereal_minor_cleaning (bd0a45b)
- Merge pull request #246 from math-comp/clean_real_dep (8dd824e)
- Merge pull request #232 from pi8027/prod_pseudoMetricNormedZmodType (d1c38a2)
- Generalise closeness properties to uniform spaces (d3e4c78)
- Generalise continuous_withinNx (c07d14a)
- Merge pull request #245 from math-comp/uniform_spaces (1b1c6be)
- Merge branch 'master' into measure_minor_cleaning (20e6388)

CohenCyril updated PR #243 minor fix, generalizations, cleaning from `measure_minor_cleaning`

to `master`

:

Harmless improvement in preparation for more PRs on the topic. @CohenCyril

CohenCyril milestoned Issue #243 minor fix, generalizations, cleaning:

Harmless improvement in preparation for more PRs on the topic. @CohenCyril

CohenCyril pushed 2 commits to branch measure_minor_cleaning. Commits by affeldt-aist (2).

CohenCyril updated PR #243 minor fix, generalizations, cleaning from `measure_minor_cleaning`

to `master`

:

Harmless improvement in preparation for more PRs on the topic. @CohenCyril

CohenCyril merged PR #243 minor fix, generalizations, cleaning.

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

- minor fix, generalizations, cleaning (ed7d91c)
- update changelog (bc0e4b2)
- Merge pull request #243 from math-comp/measure_minor_cleaning (bfe024c)

CohenCyril closed 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`

CohenCyril demilestoned Issue #206 Add a distrLattice canonical structure to set T.

Hi,

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:

CohenCyril milestoned Issue #206 Add a distrLattice canonical structure to set T.

Hi,

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:

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril created PR Review Comment on #197 contributing file:

`The purpose of this file is to document coding styles to be`

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril created PR Review Comment on #197 contributing file:

`phrasing, as in`

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril created PR Review Comment on #197 contributing file:

`\forall x \near \oo, P x.`

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril created PR Review Comment on #197 contributing file:

`is might be worth using filter combinators, i.e. lemmas such as`

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril created PR Review Comment on #197 contributing file:

`(for `homo`) or the head of the LHS of the equality (for `mono`), as in ```coq Lemma le_contract : {mono contract : x y / (x <= y)%O}.`

`~~~`

CohenCyril edited PR Review Comment on #197 contributing file.

CohenCyril pushed 1 commit to branch contributing_guide.

- Minor fixes (3ea8a27)

CohenCyril 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.

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril created PR Review Comment on #197 contributing file:

`Landau notations can be written in four shapes: - `f =o_F e` (i.e. functional with a simple right member, thus a binary notation) - `f = g +o_F e` (i.e. functional with an additive right member, thus ternary) - `f x =o_(x \near F) (e x)` (i.e. pointwise with a simple right member, thus binary) - `f x = g x +o_(x \near F) (e x)` (i.e. pointwise with an additive right member, thus ternary) The outcome is an expression with the normal Leibniz equality `=` and term `'o_F` which is not parsable. See [this paper](https://doi.org/10.6092/issn.1972-5787/8124) for more explanation and the header of the file [landau.v](https://github.com/math-comp/analysis/blob/master/theories/landau.v).`

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril created PR Review Comment on #197 contributing file:

`## `-->` vs. `cvg` vs. `lim``

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril created PR Review Comment on #197 contributing file:

`F --> x`

means`F`

tends to`x`

. _This is the preferred way of stating a convergence._Lemmas about it use the string`cvg`

.`lim F`

is the limit of`F`

, it makes sense only when`F`

converges and defaults to a distinguished point otherwise. _It should only be used when there is no other expression for the limit._Lemmas about it use the string`lim`

.`cvg F`

is defined as`F --> lim F`

, and is equivalent through`cvgP`

and`cvg_ex`

to the existence of some`x`

such that`F --> x`

. _When the limit is known,`F --> x`

should be preferred._Lemmas about it use the string`is_cvg`

.

CohenCyril edited PR Review Comment on #197 contributing file.

CohenCyril pushed 1 commit to branch contributing_guide.

- a short description for cvg and landau (b74dce4)

CohenCyril 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.

**CohenCyril** has marked PR #197 as ready for review.

CohenCyril submitted PR Review for #197 contributing file.

CohenCyril merged PR #197 contributing file.

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

- 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)
- naming convention about homo/mono lemmas (01e58b8)
- Minor fixes (3ea8a27)
- a short description for cvg and landau (b74dce4)
- Merge pull request #197 from math-comp/contributing_guide (04d7c72)

CohenCyril milestoned Issue #237 lemmas about supremum and supremums:

Lemmas used in the branch

`integral_sketch`

.

CohenCyril demilestoned Issue #237 lemmas about supremum and supremums:

Lemmas used in the branch

`integral_sketch`

.

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#L199Remove the "'the" tag which makes things unreadable

https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L135

...

CohenCyril milestoned Issue #2 Fix 'the_* landau notation to improve readability:

https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L199

https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/landau.v#L135

...

affeldt-aist deleted the branch measure_minor_cleaning.

affeldt-aist deleted the branch ereal_minor_cleaning.

affeldt-aist deleted the branch contributing_guide.

affeldt-aist pushed 2 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (795cae0)
- tentative caratheodory theorem (dcc63af)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

drouhling closed without merge PR #112 WIP / Experiment : Remove the dependency on R.

CohenCyril milestoned Issue #112 WIP / Experiment : Remove the dependency on R:

I need feedback on this branch which:

replaces

`ball`

with`entourages`

as primitive for the definition of`uniformType`

.removes

`absRingType`

and uses`numDomainType`

instead (related to #4).instantiates the hierarchy on mathcomp's algebraic structures (see

`classical_sets.v`

and`hierarchy.v`

).replaces

`R`

from standard library with any`realFieldType`

/`realType`

and`Rbar`

with`realFieldBar`

.moves non norm-related structures to

`topology.v`

.Using entourages tends to lengthen proofs. In particular, I am not very satisfied with the way

`entourages_split`

replaces`ball_split`

but I haven't found any solution yet.

In normed spaces it is less problematic since we can still use the balls defined by the norm.This branch only use a small part of

`Rstruct.v`

, and this part does not depend on`R`

any more. I believe this file should move to`misc/`

, be extended with the structures from our hierarchy, and come with an example file on`R`

containing the compatibility lemmas from Coquelicot about`continuity_pt`

and`derive_pt`

.The file

`derive.v`

also takes a very long time to compile. I mean more than before. I don't know why yet. In particular Coq takes a long time to go through the proof script of`diffM`

. I looked at the debug script for typeclasses and it seems that Coq is stuckaftertypeclass inference finds how to close all generated subgoals.TODO-list:

[x] Generalize

`ereal`

and merge with`realFieldBar`

(related to #3).

`ereal`

is now generalized to any`numDomainType`

and used everywhere. The`+oo`

and`-oo`

notations replace`\+inf`

and`\-inf`

.

I suggest to delete`Rbar.v`

but first we need to finish the discussion in #3: does there remain any part of the arithmetic in`Rbar.v`

we want to port to`ereal`

?[x] Move

`bigmaxr`

theory out of`Rstruct.v`

? Or reimplement using`bigop`

, generalizing and extending`bigRmax`

theory ?A theory of min/max using

`bigop`

is now in`hierarchy.v`

. This is probably not perfect and should be extended (see discussion in #114), but it is sufficient for the purpose of this PR.[x] Move

`Rstruct.v`

to`misc/`

and extend it with our structures.[x] Reintroduce commented out lemmas about

`R`

and`Rbar`

, either translating them to`realFieldType`

/`realType`

/`realFieldBar`

or putting them in an example file in`misc/`

.[ ] Investigate

`derive.v`

's compilation issue.[ ] Clean up.

[x] Be consistent with names (sometimes

`entourages`

is used, sometimes it is`entourage`

).[x] Rework the existing documentation.

[ ] Rename

`hierarchy.v`

(and`topology.v`

?) to reflect the new organization.[x] Make sure each lemma is in the right file and no lemma has been dropped.

affeldt-aist pushed 1 commit to branch master.

- changelog for version 0.3.2 (91cd60b)

affeldt-aist pushed 1 commit to branch master.

- update opam file (376246c)

affeldt-aist:

- edited HOWTORELEASE

CohenCyril pushed 1 commit to branch fix-changelog.

- fix changelog (0197503)

CohenCyril opened PR #247 fix changelog from `fix-changelog`

to `master`

.

CohenCyril pushed 1 commit to branch fix-changelog.

- Update CHANGELOG.md (b369f36)

CohenCyril updated PR #247 fix changelog from `fix-changelog`

to `master`

.

affeldt-aist merged PR #247 fix changelog.

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

- fix changelog (#247) (ae360cd)

affeldt-aist created release MathComp Analysis 0.3.2 for tag 0.3.2.

affeldt-aist released release MathComp Analysis 0.3.2 for tag 0.3.2.

affeldt-aist published release MathComp Analysis 0.3.2 for tag 0.3.2.

affeldt-aist pushed tag 0.3.2.

affeldt-aist:

- edited HOWTORELEASE

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch fix_installmd_20200811.

- update/fix INSTALL.md (26d936d)

affeldt-aist opened PR #248 update/fix INSTALL.md from `fix_installmd_20200811`

to `master`

:

Fix a typo in

`INSTALL.md`

and updat version numbers.

affeldt-aist:

- edited HOWTORELEASE

affeldt-aist pushed 1 commit to branch bigcup_set1_fix.

- minor generalization (d380da6)

affeldt-aist opened PR #249 minor generalization from `bigcup_set1_fix`

to `master`

:

minor generalization that we happen to rely on in infotheo

CohenCyril pushed 1 commit to branch union-merge-changelog.

- merging changelog unreleased with "union" merge driver. (66b43dd)

CohenCyril opened PR #250 merging changelog unreleased with "union" merge driver. from `union-merge-changelog`

to `master`

.

CohenCyril milestoned Issue #249 minor generalization:

minor generalization that we happen to rely on in infotheo

CohenCyril merged PR #249 minor generalization.

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

CohenCyril merged PR #250 merging changelog unreleased with "union" merge driver.

CohenCyril pushed 2 commits to branch master.

- merging changelog unreleased with "union" merge driver. (66b43dd)
- Merge pull request #250 from math-comp/union-merge-changelog (e7a4014)

CohenCyril merged PR #248 update/fix INSTALL.md.

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

- update/fix INSTALL.md (26d936d)
- Merge pull request #248 from math-comp/fix_installmd_20200811 (26729f9)

CohenCyril deleted the branch union-merge-changelog.

affeldt-aist deleted the branch bigcup_set1_fix.

affeldt-aist deleted the branch fix_installmd_20200811.

affeldt-aist deleted the branch fix-changelog.

affeldt-aist deleted the branch uniform_spaces.

affeldt-aist deleted the branch clean_real_dep.

affeldt-aist pushed 2 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (e7105ae)
- tentative caratheodory theorem (3e7d411)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch warnings_20200814.

- removing a few warnings (01a4bf3)

affeldt-aist opened PR #251 removing a few warnings from `warnings_20200814`

to `master`

:

- duplicate-clear, implicit-core-hint-db, and non-recursive

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

CohenCyril milestoned Issue #251 removing a few warnings:

- duplicate-clear, implicit-core-hint-db, and non-recursive

CohenCyril merged PR #251 removing a few warnings.

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

- removing a few warnings (01a4bf3)
- Merge pull request #251 from math-comp/warnings_20200814 (9e270bd)

affeldt-aist:

- edited Home

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

affeldt-aist pushed 1 commit to branch classical_sets_20200824.

- addition of technical lemmas (6a1a9ea)

affeldt-aist opened PR #252 addition of technical lemmas from `classical_sets_20200824`

to `master`

:

Mostly

`classical_sets`

lemmas. Naming follows`finset.v`

. I have renamed`setIDl`

,`setUDr`

,`setUDl`

,`setIDr`

with a`U`

instead of a`D`

like it is in`finset.v`

. I guess this is because`D`

is put at better use for lemmas with the`\`

operator.

affeldt-aist deleted the branch warnings_20200814.

CohenCyril merged PR #252 addition of technical lemmas.

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

- addition of technical lemmas (6a1a9ea)
- Merge pull request #252 from math-comp/classical_sets_20200824 (6d6fb39)

CohenCyril milestoned Issue #252 addition of technical lemmas:

Mostly

`classical_sets`

lemmas. Naming follows`finset.v`

. I have renamed`setIDl`

,`setUDr`

,`setUDl`

,`setIDr`

with a`U`

instead of a`D`

like it is in`finset.v`

. I guess this is because`D`

is put at better use for lemmas with the`\`

operator.

CohenCyril submitted PR Review for #206 Add a distrLattice canonical structure to set T.

CohenCyril created PR Review Comment on #206 Add a distrLattice canonical structure to set T.

These three last lines should be regrouped in one single line.

CohenCyril updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

affeldt-aist updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

affeldt-aist pushed 2 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (d42f8d2)
- tentative caratheodory theorem (1ef63ff)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist deleted the branch classical_sets_20200824.

affeldt-aist pushed 6 commits to branch integral_sketch_hb.

- tentative caratheodory theorem (68d0495)
- wip (0721897)
- trying to use hb (3a72c43)
- add ring of sets, etc. using hierarchy builder (wip) (0e7a373)
- a few easy admits remaining from work with Cyril (d76e641)
- tentative definition of enumeration with a bit of naive set theory (886d961)

affeldt-aist opened PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Is there an interest for naive set theory like in the file

`cardinality.v`

?

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

affeldt-aist:

- edited Home

Next meeting schedule: https://github.com/math-comp/analysis/wiki (** 2020-09-04 Fri**).

affeldt-aist pushed 1 commit to branch integral_sketch_hb.

- a few more lemmas about cardinality (1a23f16)

affeldt-aist updated PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Is there an interest for naive set theory like in the file

`cardinality.v`

?

affeldt-aist pushed 2 commits to branch integral_sketch_hb.

- the cartesian product of the set of natural numbers is countably (277b424)
- sketch the last step of the proof that mu_ext is sigma_additive (0dc9a6a)

affeldt-aist updated PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Is there an interest for naive set theory like in the file

`cardinality.v`

?

affeldt-aist pushed 1 commit to branch classical_sets_20200902.

- simple lemmas added about classical sets (a281fed)

affeldt-aist opened PR #254 simple lemmas added about classical sets from `classical_sets_20200902`

to `master`

:

again a few easy lemmas I found were lacking when developing lemmas about measure theory

affeldt-aist pushed 1 commit to branch supremum_20200720.

- minor additions to the theory of supremums (62b155c)

affeldt-aist updated PR #237 lemmas about supremum and supremums from `supremum_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist submitted PR Review for #237 lemmas about supremum and supremums.

affeldt-aist created PR Review Comment on #237 lemmas about supremum and supremums:

I recorded the idea as a draft PR to mathcomp (https://github.com/math-comp/math-comp/pull/576).

affeldt-aist pushed 2 commits to branch integral_sketch_hb.

affeldt-aist updated PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Is there an interest for naive set theory like in the file

`cardinality.v`

?

affeldt-aist opened Issue #255 Redundancies between `realseq.v`

and `sequences.v`

There are redundancies between

`altreals/realseq.v`

(which predates MathComp-Analysis) and the newer`sequences.v`

. How should we factorize?

affeldt-aist labeled Issue #255 Redundancies between `realseq.v`

and `sequences.v`

There are redundancies between

`altreals/realseq.v`

(which predates MathComp-Analysis) and the newer`sequences.v`

. How should we factorize?

affeldt-aist labeled Issue #255 Redundancies between `realseq.v`

and `sequences.v`

There are redundancies between

`altreals/realseq.v`

(which predates MathComp-Analysis) and the newer`sequences.v`

. How should we factorize?

affeldt-aist labeled Issue #255 Redundancies between `realseq.v`

and `sequences.v`

`altreals/realseq.v`

(which predates MathComp-Analysis) and the newer`sequences.v`

. How should we factorize?

affeldt-aist milestoned Issue #255 Redundancies between `realseq.v`

and `sequences.v`

`altreals/realseq.v`

(which predates MathComp-Analysis) and the newer`sequences.v`

. How should we factorize?

affeldt-aist milestoned Issue #254 simple lemmas added about classical sets:

again a few easy lemmas I found were lacking when developing lemmas about measure theory

affeldt-aist:

- created 2020 09 04 Meeting

affeldt-aist:

- edited Home

affeldt-aist:

- edited 2020 09 04 Meeting

affeldt-aist:

- edited 2020 09 04 Meeting

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch integral_sketch_hb.

- progress in proving lemmas about summation over countable sets (d2168bb)

affeldt-aist updated PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Is there an interest for naive set theory like in the file

`cardinality.v`

?

affeldt-aist pushed 1 commit to branch contra_20200909.

- rename/remove contra lemmas (3d861b0)

affeldt-aist milestoned Issue #256 rename/remove contra lemmas:

Rename

`contra`

lemmas following the notation scheme adopted in MathComp and remove duplicate definitions of contra lemmas.

affeldt-aist opened PR #256 rename/remove contra lemmas from `contra_20200909`

to `master`

:

Rename

`contra`

lemmas following the notation scheme adopted in MathComp and remove duplicate definitions of contra lemmas.

CohenCyril submitted PR Review for #256 rename/remove contra lemmas.

CohenCyril created PR Review Comment on #256 rename/remove contra lemmas:

It is

`contra_not`

(https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrbool.v#L215)

affeldt-aist pushed 1 commit to branch contra_20200909.

- rename/remove contra lemmas (d8c7a1b)

affeldt-aist updated PR #256 rename/remove contra lemmas from `contra_20200909`

to `master`

:

Rename

`contra`

lemmas following the notation scheme adopted in MathComp and remove duplicate definitions of contra lemmas.

affeldt-aist submitted PR Review for #256 rename/remove contra lemmas.

affeldt-aist created PR Review Comment on #256 rename/remove contra lemmas:

Then I guess we'll need to make an issue to later remove

`contra_not`

(when MathComp's new master is released).

CohenCyril submitted PR Review for #256 rename/remove contra lemmas.

CohenCyril created PR Review Comment on #256 rename/remove contra lemmas:

This looks like unneeded changelog duplication, doesn't it?

CohenCyril submitted PR Review for #256 rename/remove contra lemmas.

CohenCyril created PR Review Comment on #256 rename/remove contra lemmas:

yes indeed

affeldt-aist pushed 1 commit to branch contra_20200909.

- rename/remove contra lemmas (e219482)

affeldt-aist updated PR #256 rename/remove contra lemmas from `contra_20200909`

to `master`

:

`contra`

lemmas following the notation scheme adopted in MathComp and remove duplicate definitions of contra lemmas.

affeldt-aist edited PR #256 rename/remove contra lemmas from `contra_20200909`

to `master`

:

`contra`

lemmas following the notation scheme adopted in MathComp and remove duplicate definitions of contra lemmas.TODO when merging: add an issue to remove

`contra_not`

when it is available with a future release of MathComp

affeldt-aist assigned PR #237 lemmas about supremum and supremums to CohenCyril.

affeldt-aist pushed 1 commit to branch duplicate_20200911.

- remove duplicate lemmas (0276041)

affeldt-aist opened PR #257 remove duplicate lemmas from `duplicate_20200911`

to `master`

:

Just removed three lemmas that made their way into

`boolp.v`

(with a different name).

pi8027 submitted PR Review for #257 remove duplicate lemmas.

pi8027 created PR Review Comment on #257 remove duplicate lemmas:

I guess

`eqNN`

should be named`notK`

.

pi8027 edited PR Review Comment on #257 remove duplicate lemmas.

affeldt-aist pushed 1 commit to branch integral_sketch_hb.

- outer measures and Cartheodory's theorem (a401d81)

affeldt-aist updated PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Is there an interest for naive set theory like in the file

`cardinality.v`

?

affeldt-aist edited PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Needs to be cleaned and factored out into PRs/commits.

affeldt-aist pushed 1 commit to branch duplicate_20200911.

- remove duplicate lemmas (0e9a0f9)

affeldt-aist updated PR #257 remove duplicate lemmas from `duplicate_20200911`

to `master`

:

Just removed three lemmas that made their way into

`boolp.v`

(with a different name).

affeldt-aist pushed 1 commit to branch integral_sketch_hb.

- test (4dd5432)

affeldt-aist updated PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Needs to be cleaned and factored out into PRs/commits.

affeldt-aist pushed 1 commit to branch integral_sketch_hb.

- outer measures and Cartheodory's theorem (7af3e19)

affeldt-aist updated PR #253 Integral sketch hb from `integral_sketch_hb`

to `integral_sketch`

:

Needs to be cleaned and factored out into PRs/commits.

affeldt-aist pushed 1 commit to branch integral_sketch.

- outer measures and Cartheodory's theorem (7af3e19)

affeldt-aist merged PR #253 Integral sketch hb.

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch integral_sketch.

- outer measures and Cartheodory's theorem (a7ee9dc)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch closed_sets_ereal_20200912.v.

- two lemmas about closed sets of extended reals (797c475)

affeldt-aist opened PR #258 two lemmas about closed sets of extended reals from `closed_sets_ereal_20200912.v`

to `master`

:

used in the development of measure theory

affeldt-aist opened Issue #259 Remove code PRed to MathComp:

Remove when PR https://github.com/math-comp/math-comp/pull/593 is merged with MathComp's master and released.

affeldt-aist labeled Issue #259 Remove code PRed to MathComp:

Remove when PR https://github.com/math-comp/math-comp/pull/593 is merged with MathComp's master and released.

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

affeldt-aist pushed 1 commit to branch ereal_normedtype_20200913.

- simple lemmas about extended reals (1b2c164)

affeldt-aist opened PR #260 simple lemmas about extended reals from `ereal_normedtype_20200913`

to `master`

:

- used to develop the theory of sequences of extended reals in another branch

affeldt-aist milestoned Issue #260 simple lemmas about extended reals:

- used to develop the theory of sequences of extended reals in another branch

affeldt-aist milestoned Issue #257 remove duplicate lemmas:

Just removed three lemmas that made their way into

`boolp.v`

(with a different name).

affeldt-aist milestoned Issue #258 two lemmas about closed sets of extended reals:

used in the development of measure theory

affeldt-aist opened Issue #261 move contents out of `normedtype.v`

I suspect that much contents about extended reals could/should be moved from

`normedtype.v`

to`topology.v`

. However, it might not be wise to provide a PR right now because it might conflict with other on-going PRs (I am thinking about PR #205 , PR #183 , PR #180).

affeldt-aist labeled Issue #261 move contents out of `normedtype.v`

I suspect that much contents about extended reals could/should be moved from

`normedtype.v`

to`topology.v`

. However, it might not be wise to provide a PR right now because it might conflict with other on-going PRs (I am thinking about PR #205 , PR #183 , PR #180).

affeldt-aist milestoned Issue #261 move contents out of `normedtype.v`

I suspect that much contents about extended reals could/should be moved from

`normedtype.v`

to`topology.v`

. However, it might not be wise to provide a PR right now because it might conflict with other on-going PRs (I am thinking about PR #205 , PR #183 , PR #180).

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 2 commits to branch integral_sketch.

- lemmas used when developping measure theory (bb46b0a)
- outer measures and Cartheodory's theorem … (b0c79c7)

affeldt-aist pushed 1 commit to branch integral_sketch.

- outer measures and Cartheodory's theorem (69b7c17)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist:

- edited Home

affeldt-aist pushed 1 commit to branch duplicate_20200911.

- remove duplicate and move/rename lemmas (38512dd)

affeldt-aist updated PR #257 remove duplicate lemmas from `duplicate_20200911`

to `master`

:

Just removed three lemmas that made their way into

`boolp.v`

(with a different name).

CohenCyril submitted PR Review for #258 two lemmas about closed sets of extended reals.

CohenCyril created PR Review Comment on #258 two lemmas about closed sets of extended reals:

`Lemma closed_ereal_le_ereal y : closed [set x | (y <= x)%E].`

CohenCyril submitted PR Review for #258 two lemmas about closed sets of extended reals.

CohenCyril created PR Review Comment on #258 two lemmas about closed sets of extended reals:

`Lemma closed_ereal_ge_ereal y : closed [set x | (y >= x)%E].`

affeldt-aist pushed 1 commit to branch closed_sets_ereal_20200912.v.

- two lemmas about closed sets of extended reals (6ccefee)

affeldt-aist updated PR #258 two lemmas about closed sets of extended reals from `closed_sets_ereal_20200912.v`

to `master`

:

used in the development of measure theory

affeldt-aist pushed 1 commit to branch integral_sketch.

- outer measures and Cartheodory's theorem (57be898)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

CohenCyril merged PR #258 two lemmas about closed sets of extended reals.

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

- two lemmas about closed sets of extended reals (6ccefee)
- Merge pull request #258 from math-comp/closed_sets_ereal_20200912.v (3de1f28)

affeldt-aist deleted the branch closed_sets_ereal_20200912.v.

affeldt-aist pushed 1 commit to branch ereal_normedtype_20200913.

- simple lemmas about extended reals (2df10cc)

affeldt-aist updated PR #260 simple lemmas about extended reals from `ereal_normedtype_20200913`

to `master`

:

- used to develop the theory of sequences of extended reals in another branch

affeldt-aist pushed 1 commit to branch classical_sets_20200902.

- simple lemmas added about classical sets (ffd577f)

affeldt-aist updated PR #254 simple lemmas added about classical sets from `classical_sets_20200902`

to `master`

:

again a few easy lemmas I found were lacking when developing lemmas about measure theory

affeldt-aist pushed 1 commit to branch supremum_20200720.

- minor additions to the theory of supremums (d0c6703)

affeldt-aist updated PR #237 lemmas about supremum and supremums (assigned to CohenCyril) from `supremum_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

mkerjean pushed 4 commits to branch mathcomp_master_hahnbanach. Commits by mkerjean (3) and affeldt-aist (1).

- Hahn-Banach adapted to PR#270 (64089df)
- various generalizations (1bd6616)
- fix wrt PR193 (6fe47bf)
- renaming locally to nbhs (3cc6fe4)

mkerjean updated PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independant from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries. It also contains lemmas proving the equivalence of boundedness and continuity of linear functions on normed vector spaces.

mkerjean:

- edited Home

mkerjean pushed 2 commits to branch mathcomp_master_hahnbanach.

mkerjean updated PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independant from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries. It also contains lemmas proving the equivalence of boundedness and continuity of linear functions on normed vector spaces.

mkerjean pushed 1 commit to branch mathcomp_master_hahnbanach.

- wip entourage (6ba634b)

mkerjean updated PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independant from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries. It also contains lemmas proving the equivalence of boundedness and continuity of linear functions on normed vector spaces.

mkerjean pushed 1 commit to branch mathcomp_master_hahnbanach.

- wip entourage (7b13796)

mkerjean updated PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independant from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries. It also contains lemmas proving the equivalence of boundedness and continuity of linear functions on normed vector spaces.

mkerjean pushed 1 commit to branch mathcomp_master_hahnbanach.

- wip bounded (db1ed75)

mkerjean updated PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independant from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries. It also contains lemmas proving the equivalence of boundedness and continuity of linear functions on normed vector spaces.

affeldt-aist:

- edited Home

mkerjean pushed 1 commit to branch mathcomp_master_hahnbanach.

- lincont bounded (2665e17)

mkerjean updated PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independant from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries. It also contains lemmas proving the equivalence of boundedness and continuity of linear functions on normed vector spaces.

mkerjean pushed 5 commits to branch mathcomp_master_linearcontinuousbounded. Commits by affeldt-aist (3) and mkerjean (2).

- LinearContinuousBounded (1d79a03)
- continuous_at -> for _, continuous (f11bb80)
- format lemmas in section LinearContinuousBounded (e1f6a94)
- Update theories/normedtype.v (0287de6)
- fix (3440a94)

mkerjean updated PR #183 LinearContinuousBounded from `mathcomp_master_linearcontinuousbounded`

to `master`

:

These lemmas should maybe be rephrased using landau notations.

mkerjean pushed 1 commit to branch mathcomp_master_linearcontinuousbounded.

- bounded functions (c46a186)

mkerjean updated PR #183 LinearContinuousBounded from `mathcomp_master_linearcontinuousbounded`

to `master`

:

These lemmas should maybe be rephrased using landau notations.

mkerjean updated PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independant from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries. It also contains lemmas proving the equivalence of boundedness and continuity of linear functions on normed vector spaces.

mkerjean pushed 113 commits to branch mathcomp_master_hahnbanach. Commits by affeldt-aist (66), CohenCyril (20), mkerjean (13) and others (14).

- LinearContinuousBounded (024ce1c)
- continuous_at -> for _, continuous (ef1ab98)
- format lemmas in section LinearContinuousBounded (a584b4e)
- Update theories/normedtype.v (559e0ee)
- fix (382699d)
- renaming: is_prop -> is_subset1 (issue 24) (ebf9243)
- tentative definitions of T2separated and closeness (12e8780)
- ported closness to topological spaces and link with hausdorff (45bdd2f)
- topological type mixin for ereal (4bd41af)
- add lemmas and perform generalizations (00bc11b)
- fix the definition of le_ereal, lt_ereal (33274cf)
- cleanup (wip) (c5f1bf3)
- fix lee_pinfty and lee_ninfty (8cb51a1)
- small renamings and left a comment for later on (cad3226)
- Big refactoring about naming conventions (a475f37)
- Various renamings (4090b4d)
- make travis not run twice! (80d83c8)
- Generic domination, boundedness and lipschitz (325e74a)
- in_setE/in_fsetE -> inE (3a4ec11)
- use mathcomp's subrKA instead of sub_trans (d6aa203)

[and 93 more commit(s)]

mkerjean pushed 1 commit to branch mathcomp_master_hahnbanach.

- fix (02a41de)

mkerjean updated PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independant from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries. It also contains lemmas proving the equivalence of boundedness and continuity of linear functions on normed vector spaces.

mkerjean edited PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `master`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independent from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries.This PR depends on PR#183

mkerjean pushed 1 commit to branch mathcomp_master_linearcontinuousbounded.

- closed balls (8d315cb)

mkerjean updated PR #183 LinearContinuousBounded from `mathcomp_master_linearcontinuousbounded`

to `master`

:

These lemmas should maybe be rephrased using landau notations.

mkerjean:

- edited Home

CohenCyril:

- edited Home

mkerjean pushed 1 commit to branch mathcomp_master_linearcontinuousbounded.

- wip closure closed_ball (a38f85a)

`mathcomp_master_linearcontinuousbounded`

to `master`

:

These lemmas should maybe be rephrased using landau notations.

mkerjean pushed 1 commit to branch mathcomp_master_linearcontinuousbounded.

- wip closure closed_ball (114842c)

`mathcomp_master_linearcontinuousbounded`

to `master`

:

These lemmas should maybe be rephrased using landau notations.

mkerjean pushed 1 commit to branch mathcomp_master_linearcontinuousbounded.

- changes (ddb5fcf)

`mathcomp_master_linearcontinuousbounded`

to `master`

:

These lemmas should maybe be rephrased using landau notations.

mkerjean pushed 1 commit to branch banach_steinhaus.

- init (d230825)

mkerjean opened PR #262 init from `banach_steinhaus`

to `mathcomp_master_linearcontinuousbounded`

:

Banach-Steinhaus Theorem, through Baire's Theorem.

This PR depends on PR#183 (linearcontinuousbounded)

mkerjean pushed 1 commit to branch mathcomp_master_linearcontinuousbounded.

- nbhs_ballrP (022f17f)

`mathcomp_master_linearcontinuousbounded`

to `master`

:

These lemmas should maybe be rephrased using landau notations.

mkerjean pushed 1 commit to branch mathcomp_master_linearcontinuousbounded.

- nbhs_ballrP (ce21e70)

`mathcomp_master_linearcontinuousbounded`

to `master`

:

These lemmas should maybe be rephrased using landau notations.

mkerjean pushed 1 commit to branch banach_steinhaus.

- wip baire (400f497)

mkerjean updated PR #262 init from `banach_steinhaus`

to `mathcomp_master_linearcontinuousbounded`

:

Banach-Steinhaus Theorem, through Baire's Theorem.

This PR depends on PR#183 (linearcontinuousbounded)

mkerjean pushed 2 commits to branch banach_steinhaus.

mkerjean updated PR #262 init from `banach_steinhaus`

to `mathcomp_master_linearcontinuousbounded`

:

Banach-Steinhaus Theorem, through Baire's Theorem.

This PR depends on PR#183 (linearcontinuousbounded)

mkerjean pushed 1 commit to branch banach_steinhaus.

- wip baire (21298d2)

mkerjean updated PR #262 init from `banach_steinhaus`

to `mathcomp_master_linearcontinuousbounded`

:

Banach-Steinhaus Theorem, through Baire's Theorem.

This PR depends on PR#183 (linearcontinuousbounded)

CohenCyril merged PR #254 simple lemmas added about classical sets.

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

- simple lemmas added about classical sets (ffd577f)
- Merge pull request #254 from math-comp/classical_sets_20200902 (0a048bb)

CohenCyril merged PR #256 rename/remove contra lemmas.

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

- rename/remove contra lemmas (e219482)
- Merge pull request #256 from math-comp/contra_20200909 (f32b0c9)

CohenCyril submitted PR Review for #257 remove duplicate lemmas.

CohenCyril submitted PR Review for #260 simple lemmas about extended reals.

CohenCyril submitted PR Review for #237 lemmas about supremum and supremums.

CohenCyril submitted PR Review for #206 Add a distrLattice canonical structure to set T.

affeldt-aist deleted the branch classical_sets_20200902.

affeldt-aist deleted the branch contra_20200909.

affeldt-aist pushed 1 commit to branch duplicate_20200911.

- remove duplicate and move/rename lemmas (2faf13c)

affeldt-aist updated PR #257 remove duplicate lemmas from `duplicate_20200911`

to `master`

:

Just removed three lemmas that made their way into

`boolp.v`

(with a different name).

affeldt-aist pushed 1 commit to branch supremum_20200720.

- minor additions to the theory of supremums (e296c1b)

affeldt-aist updated PR #237 lemmas about supremum and supremums (assigned to CohenCyril) from `supremum_20200720`

to `master`

:

Lemmas used in the branch

`integral_sketch`

.

affeldt-aist pushed 1 commit to branch ereal_normedtype_20200913.

- simple lemmas about extended reals (5d83e71)

affeldt-aist updated PR #260 simple lemmas about extended reals from `ereal_normedtype_20200913`

to `master`

:

- used to develop the theory of sequences of extended reals in another branch

CohenCyril merged PR #257 remove duplicate lemmas.

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

- remove duplicate and move/rename lemmas (2faf13c)
- Merge pull request #257 from math-comp/duplicate_20200911 (995293e)

CohenCyril merged PR #237 lemmas about supremum and supremums.

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

- minor additions to the theory of supremums (e296c1b)
- Merge pull request #237 from math-comp/supremum_20200720 (efba06d)

CohenCyril milestoned Issue #242 Insert a structure of uniform space:

This is meant to replace #119.

affeldt-aist pushed 1 commit to branch ereal_normedtype_20200913.

- simple lemmas about extended reals (e3a686e)

affeldt-aist updated PR #260 simple lemmas about extended reals from `ereal_normedtype_20200913`

to `master`

:

- used to develop the theory of sequences of extended reals in another branch

affeldt-aist pushed 3 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (9976b48)
- outer measures and Cartheodory's theorem (28d9bc9)
- rebase (855902d)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist:

- edited Home

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

CohenCyril submitted PR Review for #206 Add a distrLattice canonical structure to set T.

CohenCyril created PR Review Comment on #206 Add a distrLattice canonical structure to set T.

`+ Canonical `porderType`, `latticeType`, `distrLatticeType`, `blatticeType`, `tblatticeType`, `bDistrLatticeType`, `tbDistrLatticeType`, `cbDistrLatticeType`, `ctbDistrLatticeType` on classical `set``

CohenCyril submitted PR Review for #206 Add a distrLattice canonical structure to set T.

CohenCyril created PR Review Comment on #206 Add a distrLattice canonical structure to set T.

`Definition proper_subset {A} (X Y : set A) := (Y != X) /\ X `<=` Y.`

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

CohenCyril submitted PR Review for #206 Add a distrLattice canonical structure to set T.

CohenCyril created PR Review Comment on #206 Add a distrLattice canonical structure to set T.

Actually, on second thoughts, this definition would be even more usable like this:

`Definition proper_subset {A} (X Y : set A) := (X `<=` Y) /\ (exists2 a, Y a & ~ X a).`

With lemma

`proper_neqAsubset : (X `<` Y) = (X `!=` Y) /\ (X `<=` Y)`

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

affeldt-aist merged PR #260 simple lemmas about extended reals.

affeldt-aist pushed 1 commit to branch master.

- simple lemmas about extended reals (#260) (41b3e54)

affeldt-aist:

- created FAQ

affeldt-aist:

- edited Home

affeldt-aist pushed 2 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (ed6b7e3)
- outer measures and Cartheodory's theorem (2b63076)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch ereal_20200928.

- minor changes and additions to ereal.v used to develop measure theory (b79c4cf)

affeldt-aist opened PR #263 minor changes and additions to ereal.v from `ereal_20200928`

to `master`

:

used to develop the theory of sequences of extended real numbers

affeldt-aist pushed 1 commit to branch sequences_20200928.

- more lemmas about sequences of extended real numbers (6f81356)

affeldt-aist opened PR #264 more lemmas about sequences of extended real numbers from `sequences_20200928`

to `ereal_20200928`

:

- used to develop measure theory
- based on PR #263

affeldt-aist:

- edited Home

affeldt-aist pushed 2 commits to branch integral_sketch.

- integral.v file written with all members during mathcomp-analysis-dev meeting (2c2166b)
- outer measures and Cartheodory's theorem (d2850ab)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

affeldt-aist pushed 1 commit to branch integral_sketch.

- outer measures and Cartheodory's theorem (91784b8)

affeldt-aist updated PR #224 Integral sketch from `integral_sketch`

to `master`

:

Depends on #223 (EDIT by Cyril) which has been merged in master

CohenCyril submitted PR Review for #263 minor changes and additions to ereal.v.

CohenCyril created PR Review Comment on #263 minor changes and additions to ereal.v:

`Lemma gee0P (R : realDomainType) (x : {ereal R}) : 0%:E <= x <-> x = +oo \/ exists2 r, r >= 0 & x = r%:E.`

CohenCyril submitted PR Review for #263 minor changes and additions to ereal.v.

CohenCyril created PR Review Comment on #263 minor changes and additions to ereal.v:

`Lemma lee_sum I (f g : I -> {ereal R}) s (P : pred I) : (forall i, P i -> f i <= g i) -> \sum_(i <- s | P i) f i <= \sum_(i <- s | p i) g i.`

CohenCyril edited PR Review Comment on #263 minor changes and additions to ereal.v.

CohenCyril submitted PR Review for #263 minor changes and additions to ereal.v.

CohenCyril created PR Review Comment on #263 minor changes and additions to ereal.v:

Depending on where/how it is used, I would rather have the following:

`Lemma lee_sum_nneg I (s : seq I) (P Q : pred I) (f : I -> {ereal R}) : (forall i, P i -> Q i -> 0%:E <= f i) -> \sum_(i <- s | P i && Q i) f i <= \sum_(t <- s | P i) f i.`

But I wonder how much all of this is would be subsumed by systematically duplicating ssrnum in ereal?

CohenCyril edited PR Review Comment on #263 minor changes and additions to ereal.v.

mkerjean edited PR #262 Banach-Steinhaus from `banach_steinhaus`

to `mathcomp_master_linearcontinuousbounded`

:

Banach-Steinhaus Theorem, through Baire's Theorem.

This PR depends on PR#183 (linearcontinuousbounded)

mkerjean edited PR #179 Mathcomp master hahnbanach from `mathcomp_master_hahnbanach`

to `mathcomp_master_linearcontinuousbounded`

:

This contains two files:

`hahn_banach.v`

contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to Excluding middle, as well as a proof of Hahn_Banach theorem in its analytical form. This file is independent from MathComp Analysis libraries.

`hahn_banach_applications.v`

contains a formalization of Hahn Banach's theorem on normed vector spaces, using the Mathematical Components libraries.This PR depends on PR#183

mkerjean pushed 2 commits to branch banach_steinhaus.

mkerjean updated PR #262 Banach-Steinhaus from `banach_steinhaus`

to `mathcomp_master_linearcontinuousbounded`

:

Banach-Steinhaus Theorem, through Baire's Theorem.

This PR depends on PR#183 (linearcontinuousbounded)

affeldt-aist:

- created 2020 09 28 Meeting

affeldt-aist:

- edited Home

affeldt-aist:

- edited 2020 09 28 Meeting

affeldt-aist:

- edited Home

affeldt-aist:

- edited 2020 09 28 Meeting

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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:

vlj updated PR #206 Add a distrLattice canonical structure to set T. from `subset-lattice`

to `master`

:

Hi,

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 unif