[Merged by Bors] - feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered by wwylele · Pull Request #30436 · leanprover-community/mathlib4

wwylele · 2025-10-11T12:34:42Z

This extends the existing Finset.prod_one_sub_ordered to infinite sum/product, and also adds the more natural add version.

Together with some previous PRs about infinite sum/prod and powerseries, this is part of my effort of upstreaming useful stuff from https://github.com/wwylele/PentagonalNumberTheorem. It starts getting into niche lemma, so suggestions such that not wanting this in mathlib, or it should be stated in a different form, are all welcomed.

github-actions · 2025-10-11T12:35:56Z

PR summary 412e7b8df3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ prod_one_add_ordered
+ tprod_one_add_ordered
+ tprod_one_sub_ordered

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

kckennylau · 2025-11-21T21:10:44Z

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

+theorem tprod_one_add_ordererd [ContinuousAdd α]
+    (hsum : Summable fun i ↦ f i * ∏ j ∈ Iio i, (1 + f j))
+    (hprod : Multipliable (1 + f ·)) :
+    ∏' i, (1 + f i) = 1 + ∑' i, f i * ∏ j ∈ Iio i, (1 + f j) := by


Recently there was a huge topological summation/product refactor, where we now add a filter to the inputs of every summartion/product.

Since this is about the ordered product, I would assume that we're concerned about conditional convergence (i.e. limit of partial products using Iic/Iio), so maybe we can use that? (It's called SummationFilter.conditional.)

And if you use that, then maybe you can look at the code above you and start with the corresponding analogue of hasProd_one_add_of_hasSum_prod above, but using the conditional filter, and then you should only require the hsum assumption and not hprod?

I tried to write some code myself and this was the result.

For my own usage, I am concerned about absolute convergence, but I can look into how I can generalize this to other summation filters

Sorry, it took me a while to get back to this, but after trying for a while, I couldn't generalize this to more summation filters. I suspect this isn't correct for general (NeBot, LeAtTop) filters.

This is also very different from hasProd_one_add_of_hasSum_prod (see how the summation here has a prod inside!),. The summability can't translate.

I am honestly not very motivated to do the generalization. Perhaps, do you have a statement about general filter that you think is definitely true, so I focus on proving it without doubting its correctness?

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

grunweg · 2025-12-24T09:35:09Z

Thanks for the PR! This looks good to me, but I'd like to have another pair of eyes:
maintainer merge

github-actions · 2025-12-24T09:35:21Z

🚀 Pull request has been placed on the maintainer queue by grunweg.

JovanGerb · 2025-12-24T11:30:33Z

Will you also add the dual version of the theorem? I.e. with the order relation i < j reversed?

JovanGerb · 2025-12-24T11:32:14Z

I don't know how long it will take to tag all of the dependencies, but we will eventually use @[to_dual] to generate the dual version automatically. But it's not clear to me what the name of the dual version should be.

wwylele · 2025-12-24T13:23:12Z

The dependencies to tag is fortunately only about 6 lemmas. I can do it but I'd like to do it in another PR, given the potential debate on the naming. I don't have good idea on the name either...

JovanGerb · 2025-12-24T19:39:41Z

Hmm, I don't have a good idea for the lemma names either, though it would be nice to have a more descriptive lemma name, so that you can tell the direction based on the lemma name. Maybe something like prod_add_eq_sum_prod_lt...

jcommelin

Thanks 🎉

bors merge

Let's discuss dualizing and naming in the follow up PR.

This extends the existing `Finset.prod_one_sub_ordered` to infinite sum/product, and also adds the more natural `add` version. Together with some previous PRs about infinite sum/prod and powerseries, this is part of my effort of upstreaming useful stuff from https://github.com/wwylele/PentagonalNumberTheorem. It starts getting into niche lemma, so suggestions such that not wanting this in mathlib, or it should be stated in a different form, are all welcomed.

mathlib-bors · 2025-12-26T17:05:39Z

Build failed (retrying...):

Post-Build Step

This extends the existing `Finset.prod_one_sub_ordered` to infinite sum/product, and also adds the more natural `add` version. Together with some previous PRs about infinite sum/prod and powerseries, this is part of my effort of upstreaming useful stuff from https://github.com/wwylele/PentagonalNumberTheorem. It starts getting into niche lemma, so suggestions such that not wanting this in mathlib, or it should be stated in a different form, are all welcomed.

mathlib-bors · 2025-12-26T18:30:19Z

Pull request successfully merged into master.

Build succeeded:

wwylele · 2025-12-27T00:11:44Z

The dependencies to tag is fortunately only about 6 lemmas.

So it turned out I underestimated the amount of dependencies to tag. There is a whole chain of lemmas from Filter to tag. I am trying to work on it but it will probably take a while

…ommunity#30436) This extends the existing `Finset.prod_one_sub_ordered` to infinite sum/product, and also adds the more natural `add` version. Together with some previous PRs about infinite sum/prod and powerseries, this is part of my effort of upstreaming useful stuff from https://github.com/wwylele/PentagonalNumberTheorem. It starts getting into niche lemma, so suggestions such that not wanting this in mathlib, or it should be stated in a different form, are all welcomed.

wwylele added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Oct 18, 2025

leanprover-community-bot-assistant assigned grunweg Oct 26, 2025

kckennylau suggested changes Nov 21, 2025

View reviewed changes

kckennylau added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 21, 2025

kckennylau reviewed Nov 21, 2025

View reviewed changes

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean Outdated Show resolved Hide resolved

wwylele commented Nov 21, 2025

View reviewed changes

Mathlib/Topology/Algebra/InfiniteSum/Ring.lean Outdated Show resolved Hide resolved

feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered

2c7f8fd

wwylele force-pushed the prod-one-sub branch from d7c58e6 to 2c7f8fd Compare December 7, 2025 15:31

grind

b59af7a

wwylele removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 7, 2025

wwylele mentioned this pull request Dec 20, 2025

feat(PowerSeries): pentagonal number theorem #33143

Open

1 task

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 24, 2025

jcommelin reviewed Dec 26, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Dec 26, 2025

mathlib-bors bot changed the title ~~feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered~~ [Merged by Bors] - feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered Dec 26, 2025

mathlib-bors bot closed this Dec 26, 2025

wwylele deleted the prod-one-sub branch December 26, 2025 19:02

Conversation

wwylele commented Oct 11, 2025

Uh oh!

github-actions bot commented Oct 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 412e7b8df3

Import changes for modified files

Declarations diff

Uh oh!

kckennylau Nov 21, 2025

Choose a reason for hiding this comment

Uh oh!

wwylele Nov 21, 2025

Choose a reason for hiding this comment

Uh oh!

wwylele Dec 7, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

grunweg commented Dec 24, 2025

Uh oh!

github-actions bot commented Dec 24, 2025

Uh oh!

JovanGerb commented Dec 24, 2025

Uh oh!

JovanGerb commented Dec 24, 2025

Uh oh!

wwylele commented Dec 24, 2025

Uh oh!

JovanGerb commented Dec 24, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Dec 26, 2025

Uh oh!

mathlib-bors bot commented Dec 26, 2025

Uh oh!

wwylele commented Dec 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented Oct 11, 2025 •

edited

Loading

wwylele commented Dec 27, 2025 •

edited

Loading