[Merged by Bors] - feat: Infinite products #11733
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
YaelDillies
reviewed
Mar 28, 2024
|
Thank you for the review. I have taken into account your comments. |
YaelDillies
reviewed
Mar 29, 2024
|
Thanks; I've added the docstrings |
YaelDillies
reviewed
Mar 29, 2024
|
Sorry for missing so many of them. |
YaelDillies
approved these changes
Mar 30, 2024
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
sgouezel
reviewed
Mar 30, 2024
|
✌️ trivial1711 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
(Before merging, please take into account Yael's comment on names in the PR description) |
|
(This was already done) |
|
bors r+ |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Mar 30, 2024
Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: leanprover-community/mathlib3#18405. This is the mathlib4 version of that pull request. We define arbitrarily indexed products in a commutative monoid with a topology. This is done by "multiplicativizing" the currently existing definitions and theorems about arbitrarily indexed sums. That is, the existing code is rewritten in the multiplicative setting, and the original definitions and theorems are recovered using `@[to_additive]`. Please see this thread on Zulip for information on why this approach was chosen: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products As YaelDillies wrote in the description of leanprover-community/mathlib3#18405, there are a few small technical issues that arise when directly "multiplicativizing" theorems in this way: - I have renamed `cauchySeq_finset_iff_vanishing` to `cauchySeq_finset_iff_sum_vanishing` to make the name multiplicativizable. This is slightly different from the name `cauchy_seq_finset_sum_iff_vanishing` that YaelDillies used, and it is meant to parallel the existing name `cauchySeq_finset_iff_tsum_vanishing`. - Currently, on master, there is a theorem called `tsum_sum` about taking the `tsum` of a `sum`, and a theorem called `tsum_prod` about taking a `tsum` on a product of two index sets. I have called the multiplicative versions `tprod_of_prod` and `tprod_prod`. This is slightly different from the names `tprod_prod''` and `tprod_prod` that YaelDillies used. eric-wieser suggested renaming `tsum_prod` to `tsum_prod_index` to get around this issue, which I can do in a separate pull request.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Louddy
pushed a commit
that referenced
this pull request
Apr 15, 2024
Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: leanprover-community/mathlib3#18405. This is the mathlib4 version of that pull request. We define arbitrarily indexed products in a commutative monoid with a topology. This is done by "multiplicativizing" the currently existing definitions and theorems about arbitrarily indexed sums. That is, the existing code is rewritten in the multiplicative setting, and the original definitions and theorems are recovered using `@[to_additive]`. Please see this thread on Zulip for information on why this approach was chosen: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products As YaelDillies wrote in the description of leanprover-community/mathlib3#18405, there are a few small technical issues that arise when directly "multiplicativizing" theorems in this way: - I have renamed `cauchySeq_finset_iff_vanishing` to `cauchySeq_finset_iff_sum_vanishing` to make the name multiplicativizable. This is slightly different from the name `cauchy_seq_finset_sum_iff_vanishing` that YaelDillies used, and it is meant to parallel the existing name `cauchySeq_finset_iff_tsum_vanishing`. - Currently, on master, there is a theorem called `tsum_sum` about taking the `tsum` of a `sum`, and a theorem called `tsum_prod` about taking a `tsum` on a product of two index sets. I have called the multiplicative versions `tprod_of_prod` and `tprod_prod`. This is slightly different from the names `tprod_prod''` and `tprod_prod` that YaelDillies used. eric-wieser suggested renaming `tsum_prod` to `tsum_prod_index` to get around this issue, which I can do in a separate pull request.
atarnoam
pushed a commit
that referenced
this pull request
Apr 16, 2024
Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: leanprover-community/mathlib3#18405. This is the mathlib4 version of that pull request. We define arbitrarily indexed products in a commutative monoid with a topology. This is done by "multiplicativizing" the currently existing definitions and theorems about arbitrarily indexed sums. That is, the existing code is rewritten in the multiplicative setting, and the original definitions and theorems are recovered using `@[to_additive]`. Please see this thread on Zulip for information on why this approach was chosen: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products As YaelDillies wrote in the description of leanprover-community/mathlib3#18405, there are a few small technical issues that arise when directly "multiplicativizing" theorems in this way: - I have renamed `cauchySeq_finset_iff_vanishing` to `cauchySeq_finset_iff_sum_vanishing` to make the name multiplicativizable. This is slightly different from the name `cauchy_seq_finset_sum_iff_vanishing` that YaelDillies used, and it is meant to parallel the existing name `cauchySeq_finset_iff_tsum_vanishing`. - Currently, on master, there is a theorem called `tsum_sum` about taking the `tsum` of a `sum`, and a theorem called `tsum_prod` about taking a `tsum` on a product of two index sets. I have called the multiplicative versions `tprod_of_prod` and `tprod_prod`. This is slightly different from the names `tprod_prod''` and `tprod_prod` that YaelDillies used. eric-wieser suggested renaming `tsum_prod` to `tsum_prod_index` to get around this issue, which I can do in a separate pull request.
uniwuni
pushed a commit
that referenced
this pull request
Apr 19, 2024
Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: leanprover-community/mathlib3#18405. This is the mathlib4 version of that pull request. We define arbitrarily indexed products in a commutative monoid with a topology. This is done by "multiplicativizing" the currently existing definitions and theorems about arbitrarily indexed sums. That is, the existing code is rewritten in the multiplicative setting, and the original definitions and theorems are recovered using `@[to_additive]`. Please see this thread on Zulip for information on why this approach was chosen: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products As YaelDillies wrote in the description of leanprover-community/mathlib3#18405, there are a few small technical issues that arise when directly "multiplicativizing" theorems in this way: - I have renamed `cauchySeq_finset_iff_vanishing` to `cauchySeq_finset_iff_sum_vanishing` to make the name multiplicativizable. This is slightly different from the name `cauchy_seq_finset_sum_iff_vanishing` that YaelDillies used, and it is meant to parallel the existing name `cauchySeq_finset_iff_tsum_vanishing`. - Currently, on master, there is a theorem called `tsum_sum` about taking the `tsum` of a `sum`, and a theorem called `tsum_prod` about taking a `tsum` on a product of two index sets. I have called the multiplicative versions `tprod_of_prod` and `tprod_prod`. This is slightly different from the names `tprod_prod''` and `tprod_prod` that YaelDillies used. eric-wieser suggested renaming `tsum_prod` to `tsum_prod_index` to get around this issue, which I can do in a separate pull request.
callesonne
pushed a commit
that referenced
this pull request
Apr 22, 2024
Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: leanprover-community/mathlib3#18405. This is the mathlib4 version of that pull request. We define arbitrarily indexed products in a commutative monoid with a topology. This is done by "multiplicativizing" the currently existing definitions and theorems about arbitrarily indexed sums. That is, the existing code is rewritten in the multiplicative setting, and the original definitions and theorems are recovered using `@[to_additive]`. Please see this thread on Zulip for information on why this approach was chosen: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products As YaelDillies wrote in the description of leanprover-community/mathlib3#18405, there are a few small technical issues that arise when directly "multiplicativizing" theorems in this way: - I have renamed `cauchySeq_finset_iff_vanishing` to `cauchySeq_finset_iff_sum_vanishing` to make the name multiplicativizable. This is slightly different from the name `cauchy_seq_finset_sum_iff_vanishing` that YaelDillies used, and it is meant to parallel the existing name `cauchySeq_finset_iff_tsum_vanishing`. - Currently, on master, there is a theorem called `tsum_sum` about taking the `tsum` of a `sum`, and a theorem called `tsum_prod` about taking a `tsum` on a product of two index sets. I have called the multiplicative versions `tprod_of_prod` and `tprod_prod`. This is slightly different from the names `tprod_prod''` and `tprod_prod` that YaelDillies used. eric-wieser suggested renaming `tsum_prod` to `tsum_prod_index` to get around this issue, which I can do in a separate pull request.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: leanprover-community/mathlib3#18405. This is the mathlib4 version of that pull request.
We define arbitrarily indexed products in a commutative monoid with a topology. This is done by "multiplicativizing" the currently existing definitions and theorems about arbitrarily indexed sums. That is, the existing code is rewritten in the multiplicative setting, and the original definitions and theorems are recovered using
@[to_additive]. Please see this thread on Zulip for information on why this approach was chosen: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20productsAs YaelDillies wrote in the description of leanprover-community/mathlib3#18405, there are a few small technical issues that arise when directly "multiplicativizing" theorems in this way:
cauchySeq_finset_iff_vanishingtocauchySeq_finset_iff_sum_vanishingto make the name multiplicativizable. This is slightly different from the namecauchy_seq_finset_sum_iff_vanishingthat YaelDillies used, and it is meant to parallel the existing namecauchySeq_finset_iff_tsum_vanishing.tsum_sumabout taking thetsumof asum, and a theorem calledtsum_prodabout taking atsumon a product of two index sets. I have called the multiplicative versionstprod_of_prodandtprod_prod. This is slightly different from the namestprod_prod''andtprod_prodthat YaelDillies used. eric-wieser suggested renamingtsum_prodtotsum_prod_indexto get around this issue, which I can do in a separate pull request.