This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
feat(topology/algebra/infinite_sum): Multiplicativise #18405
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
added
awaiting-review
Another way out would be to rename the existing |
eric-wieser
reviewed
Feb 9, 2023
There was a problem hiding this comment.
Please edit the mathlib4 porting comments to indicate that porting this file is blocked by this refactor; that way we don't end up wasting work porting the old version.
If this becomes on the critical part for porting, it's possible we won't wait for this refactor; but if the comment is in the yaml file then that certainly shouldn't happen without a Zulip discussion.
|
You say that "The manually additivized lemma names |
YaelDillies
added
the
blocked-by-other-PR
bors bot
pushed a commit
that referenced
this pull request
Feb 15, 2023
Over the past five years, `topology.algebra.infinite_sum` has grown pretty big. This PR splits off a third of it to three new files. Precisely, split `topology.algebra.infinite_sum` into: * `topology.algebra.infinite_sum.basic`: Definitions and theory in monoids. All this will be multiplicativised in #18405. * `topology.algebra.infinite_sum.ring`: Interaction of infinite sums and (scalar) multiplication. This mostly cannot be multiplicativised. * `topology.algebra.infinite_sum.order`: Interaction of infinite sums and order. Most of this will be multiplicativised in #18405. Incidentally, this brings down some files' imports by quite a lot. Also move the `star` and `mul_opposite` material to the end of the file to facilitate multiplicativisation in #18405. Johannes wrote some of all these files, except `topology.algebra.infinite_sum.real` whose first lemma I could trace back as coming from #753, with the others coming from #1739.
bors bot
pushed a commit
that referenced
this pull request
Feb 15, 2023
Over the past five years, `topology.algebra.infinite_sum` has grown pretty big. This PR splits off a third of it to three new files. Precisely, split `topology.algebra.infinite_sum` into: * `topology.algebra.infinite_sum.basic`: Definitions and theory in monoids. All this will be multiplicativised in #18405. * `topology.algebra.infinite_sum.ring`: Interaction of infinite sums and (scalar) multiplication. This mostly cannot be multiplicativised. * `topology.algebra.infinite_sum.order`: Interaction of infinite sums and order. Most of this will be multiplicativised in #18405. Incidentally, this brings down some files' imports by quite a lot. Also move the `star` and `mul_opposite` material to the end of the file to facilitate multiplicativisation in #18405. Johannes wrote some of all these files, except `topology.algebra.infinite_sum.real` whose first lemma I could trace back as coming from #753, with the others coming from #1739.
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
eric-wieser
added
the
merge-conflict
YaelDillies
added
awaiting-CI
|
Can you update the PR description to reflect the file split now having happened already? |
|
Thank you, I forgot. |
|
I don't understand why I am getting all those elaboration timeouts 😢 |
kim-em
added
the
wait-requested-on
github-actions
bot
added
the
modifies-synchronized-file
|
All non-trivial changes in this PR are to files that were ported in early March, so I am removing the |
collares
removed
the
wait-requested-on
|
This will need redoing in Lean 4 and it seems we haven't yet decided what multiplicativising should even look like. |
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
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.
Louddy
pushed a commit
to leanprover-community/mathlib4
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
to leanprover-community/mathlib4
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
to leanprover-community/mathlib4
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
to leanprover-community/mathlib4
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 subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
Multiplicativise
has_sum,summable,tsumand their API to gethas_prod,prodable,tprod.The diff is mostly additivizing lemmas. However extra attention should be paid to the following:
cauchy_seq_finset_iff_vanishingtocauchy_seq_finset_sum_iff_vanishingas otherwise the name wouldn't be multiplicativisableprodandfinset.prod. Concretely, we have the lemmastsum_sum,tsum_prod,tsum_prod'which want to be multiplicativised totprod_prod,tprod_prod,tprod_prod'. I am instead multiplicativising them totprod_prod'',tprod_prod,tprod_prod'Requested by @pechersky