[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems #16544

CBirkbeck · 2024-09-06T17:40:19Z

Add some basic results about tsums indexed by pnat.

depends on: [Merged by Bors] - feat(Analysis/NormedSpace/FunctionSeries): add eventually versions #16543

github-actions · 2024-09-06T17:41:00Z

PR summary 59bdaf8b48

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ pnat_multipliable_iff_multipliable_succ
+ tprod_pnat_eq_tprod_succ

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

mathlib4-dependent-issues-bot · 2024-11-28T15:23:19Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Analysis/NormedSpace/FunctionSeries): add eventually versions #16543~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

Thanks! 🚀

maintainer merge

Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

github-actions · 2025-01-04T21:57:28Z

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

kim-em · 2025-01-05T00:09:05Z

Please act on Yael's suggestions before merging.

bors d+

mathlib-bors · 2025-01-05T00:09:07Z

✌️ CBirkbeck can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Yaël Dillies <[email protected]>

CBirkbeck · 2025-01-06T09:13:55Z

bors r+

Add some basic results about tsums indexed by pnat. Co-authored-by: Chris Birkbeck <[email protected]>

mathlib-bors · 2025-01-06T09:34:47Z

Build failed:

Build

CBirkbeck · 2025-01-06T11:54:54Z

bors r+

Add some basic results about tsums indexed by pnat. Co-authored-by: Chris Birkbeck <[email protected]>

mathlib-bors · 2025-01-06T12:15:33Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (189 commits) chore(Algebra): make more names consistent (#20449) feat: Polynomial FLT (#18882) feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457) fix: linkfix in 100.yaml (#20517) feat(1000): fill in more entries (#20470) feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769) feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462) feat(RingTheory): classification of etale algebras over fields (#20324) fix: Allow multiple builds on staging branch (#20515) feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337) chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863) chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514) refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474) feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544) chore(RingTheory/Finiteness): rename Module.Finite.out (#20506) refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508) feat(CategoryTheory): products in the category of Ind-objects (#20507) chore: remove >9 month old deprecations (#20505) chore(FieldTheory/Galois): small cleanup (#20217) chore(LinearIndependent): generalize to semirings (#20480) chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) chore: replace `aesop` with `simp` where possible (#20483) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) ...

CBirkbeck added 2 commits September 6, 2024 18:34

feat(Analysis/NormedSpace/FunctionSeries): add eventually versions

94cc501

feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems

120118d

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Sep 6, 2024

joneugster added t-topology Topological spaces, uniform spaces, metric spaces, filters t-analysis Analysis (normed *, calculus) labels Sep 12, 2024

CBirkbeck mentioned this pull request Oct 5, 2024

Cot mittag leffler #16547

Open

5 tasks

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Nov 28, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 28, 2024

CBirkbeck added the WIP Work in progress label Dec 4, 2024

CBirkbeck added 2 commits December 4, 2024 10:24

Merge remote-tracking branch 'origin/master' into pnat_tsum

6fe5626

make mult version

e82f6db

CBirkbeck removed the WIP Work in progress label Dec 4, 2024

update names

d9b74d6

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 4, 2024

fix name

9f1fbd8

YaelDillies approved these changes Jan 4, 2025

View reviewed changes

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

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

github-actions bot added the maintainer-merge label Jan 4, 2025

leanprover-community-mathlib4-bot added the delegated label Jan 5, 2025

CBirkbeck and others added 2 commits January 6, 2025 09:12

Update Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

3497dcd

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

ae06199

Co-authored-by: Yaël Dillies <[email protected]>

mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2025

feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544)

54effda

Add some basic results about tsums indexed by pnat. Co-authored-by: Chris Birkbeck <[email protected]>

fix lint

59bdaf8

mathlib-bors bot pushed a commit that referenced this pull request Jan 6, 2025

feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544)

ae4ed02

Add some basic results about tsums indexed by pnat. Co-authored-by: Chris Birkbeck <[email protected]>

mathlib-bors bot changed the title ~~feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems~~ [Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems Jan 6, 2025

mathlib-bors bot closed this Jan 6, 2025

mathlib-bors bot deleted the pnat_tsum branch January 6, 2025 12:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems #16544

[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems #16544

CBirkbeck commented Sep 6, 2024 •

edited by YaelDillies

Loading

github-actions bot commented Sep 6, 2024 •

edited

Loading

mathlib4-dependent-issues-bot commented Nov 28, 2024

YaelDillies left a comment

github-actions bot commented Jan 4, 2025

kim-em commented Jan 5, 2025

mathlib-bors bot commented Jan 5, 2025

CBirkbeck commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

CBirkbeck commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems #16544

[Merged by Bors] - feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems #16544

Conversation

CBirkbeck commented Sep 6, 2024 • edited by YaelDillies Loading

github-actions bot commented Sep 6, 2024 • edited Loading

PR summary 59bdaf8b48

Import changes for modified files

Declarations diff

mathlib4-dependent-issues-bot commented Nov 28, 2024

YaelDillies left a comment

Choose a reason for hiding this comment

github-actions bot commented Jan 4, 2025

kim-em commented Jan 5, 2025

mathlib-bors bot commented Jan 5, 2025

CBirkbeck commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

CBirkbeck commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

CBirkbeck commented Sep 6, 2024 •

edited by YaelDillies

Loading

github-actions bot commented Sep 6, 2024 •

edited

Loading