[Merged by Bors] - feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) by xroblot · Pull Request #20661 · leanprover-community/mathlib4

xroblot · 2025-01-11T16:26:35Z

We prove several results involving partial sums of coefficients (or norm of coefficients) of L-series.

The two main results of this PR are:

LSeriesSummable_of_sum_norm_bigO: for f : ℕ → ℂ, if the partial sums ∑ k ∈ Icc 1 n, ‖f k‖ are O(n ^ r) for some real 0 ≤ r, then the L-series Lseries f converges at s : ℂ for all s such that r < s.re.
LSeries_eq_mul_integral : for f : ℕ → ℂ, if the partial sums ∑ k ∈ Icc 1 n, f k are O(n ^ r) for some real 0 ≤ r and the L-series LSeries f converges at s : ℂ with r < s.re, then LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (- (s + 1)).

More results will be proved in #20660

depends on: [Merged by Bors] - feat(Analysis/Pow/Deriv): add some results about differentiability of cpow #19944

github-actions · 2025-01-11T16:27:25Z

PR summary a49515e3d9

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Asymptotics.SpecificAsymptotics	1358	1380	+22 (+1.62%)

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Polynomial.Basic`	19
`Mathlib.Analysis.Asymptotics.SpecificAsymptotics`	22
`Mathlib.NumberTheory.LSeries.SumCoeff` (new file)	2148

Declarations diff

+ Asymptotics.isEquivalent_nat_ceil
+ Asymptotics.isEquivalent_nat_floor
+ IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow
+ IsBigO.mul_atTop_rpow_of_isBigO_rpow
+ LSeriesSummable_of_sum_norm_bigO
+ LSeriesSummable_of_sum_norm_bigO_and_nonneg
+ LSeries_eq_mul_integral
+ LSeries_eq_mul_integral'
+ LSeries_eq_mul_integral_of_nonneg
+ _root_.integrableOn_mul_sum_Icc
+ cpow_ne_zero_iff
+ cpow_ne_zero_iff_of_exponent_ne_zero
+ deriv_norm_ofReal_cpow
+ integrableAtFilter_rpow_atTop_iff
+ integrableOn_Ioi_deriv_norm_ofReal_cpow
+ integrableOn_Ioi_deriv_ofReal_cpow
+ locallyIntegrableOn_mul_sum_Icc
+ ne_zero_of_re_pos
+ norm_ofReal_cpow_eventually_eq_atTop
+ range_succ_eq_Icc_zero
+ re_neg_ne_zero_of_re_pos
+ term_def₀

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 · 2025-01-20T17:20:24Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Analysis/Pow/Deriv): add some results about differentiability of cpow #19944~~
By Dependent Issues (🤖). Happy coding!

loefflerd

Here's some feedback on all the files except the new one (will look at the new one later). All looks very good so far!

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean

Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean

Mathlib/NumberTheory/AbelSummation.lean

loefflerd

I am not sure it is a good idea to have so many private declarations. When I first started contributing to mathlib, I was told that private was banned entirely; the rules have been relaxed somewhat, but I think indiscriminate use of private is still discouraged.

Many of these lemmas (not all, I admit) could potentially be useful elsewhere. Maybe they're not terribly interesting, but mathlib is full of dull-but-useful lemmas. Others have one-line proofs and are only used once in the file; so they can just be in-lined where used.

Mathlib/NumberTheory/LSeries/SumCoeff.lean

xroblot · 2025-01-23T12:49:59Z

I am not sure it is a good idea to have so many private declarations. When I first started contributing to mathlib, I was told that private was banned entirely; the rules have been relaxed somewhat, but I think indiscriminate use of private is still discouraged.

Many of these lemmas (not all, I admit) could potentially be useful elsewhere. Maybe they're not terribly interesting, but mathlib is full of dull-but-useful lemmas. Others have one-line proofs and are only used once in the file; so they can just be in-lined where used.

Yes, I know there are a lot of private results. I tried to keep the proof short (well, not too long) and thus added a lot of partial results (and it's even worse in the second PR). I'll try to clean it up a bit as you suggested by making some of them public and incorporating others in the proof.

xroblot · 2025-01-25T18:06:19Z

@loefflerd, I got rid of almost all the private results. The easy ones are now proved where they are needed and I generalized (or tried to) the other ones and move them where they belong. It is possible that the PR is now more difficult to review. I can split it into several smaller PR if needed, just let me know.

loefflerd

Thanks for all the work you've put into this! I've suggested a bunch of changes, but almost all of them are entirely cosmetic – the only ones with any content are occasionally replacing explicit rewrites with automatic tactics (linarith, ring etc) for maintainability.

maintainer delegate

Mathlib/NumberTheory/LSeries/SumCoeff.lean

github-actions · 2025-01-26T10:45:52Z

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

Mathlib/NumberTheory/LSeries/SumCoeff.lean

xroblot · 2025-01-26T16:25:56Z

Thanks a lot for the reviews!

Mathlib/NumberTheory/LSeries/SumCoeff.lean

riccardobrasca · 2025-01-27T09:59:18Z

Thanks!

bors d+

mathlib-bors · 2025-01-27T09:59:22Z

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

xroblot · 2025-01-27T10:18:04Z

bors r+

…ients (part 1) (#20661) We prove several results involving partial sums of coefficients (or norm of coefficients) of L-series. The two main results of this PR are: - `LSeriesSummable_of_sum_norm_bigO`: for `f : ℕ → ℂ`, if the partial sums `∑ k ∈ Icc 1 n, ‖f k‖` are `O(n ^ r)` for some real `0 ≤ r`, then the L-series `Lseries f` converges at `s : ℂ` for all `s` such that `r < s.re`. - `LSeries_eq_mul_integral` : for `f : ℕ → ℂ`, if the partial sums `∑ k ∈ Icc 1 n, f k` are `O(n ^ r)` for some real `0 ≤ r` and the L-series `LSeries f` converges at `s : ℂ` with `r < s.re`, then `LSeries f s = s * ∫ t in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * t ^ (- (s + 1))`. More results will be proved in #20660

mathlib-bors · 2025-01-27T10:51:28Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (294 commits) feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) feat(RingTheory/Artinian): `IsUnit a` iff `a ∈ R⁰` for an artinian ring `R` (#21084) feat: separating set in the category of ind-objects (#21082) feat: derivWithin lemmas (#21092) chore(Fintype): golf a proof (#21113) chore: golf using `funext₂` (#21106) chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) doc(Algebra/BigOperators/Fin): change 'product' to 'sum' in doc-string of additivised declarations (#21101) doc(ComputeDegree): typos (#21095) ...

* polynomial-sequences: (308 commits) Use the lemma we already added. Minor reordering. This is true even for the trivial ring. Also add the lt versions and the other inj lemma. Also add the basis ne versions. This seems also like it should be simp. Back to sorry free. And the natDegree version. feat: equalizers and coequalizers in the category of ind-objects (#21139) doc: turn more links to Stacks into `@[stacks]` tags (#21135) feat(Asymptotics): prove `IsLittleOTVS.add` (#20578) feat(Algebra/Polynomial): `Polynomial.aeval` for product algebras (#21062) chore: import Std in Mathlib.lean (#21126) feat(Data/Matroid/Circuit): fundamental circuits and extensionality (#21145) feat(CategoryTheory/Endofunctor): prove the dual form of Lambek's Lemma on terminal coalgebra (#21140) feat(SetTheory/Game/PGame): rewrite left moves of `-x` as right moves of `x` under binders (#21109) feat(RingTheory/Localization/Pi): localization of a finite direct product is a product of localizations (#19042) doc: fixed notation error in customizing category composition (#21132) feat(Matrix): more lemmas for `PEquiv.toMatrix` (#21143) chore(SupIndep): speedup the `Decidable` instance (#21114) fix(CI): use `Elab.async=false` for late importers workflow (#21147) feat(Topology/Algebra/Indicator): indicator of a clopen is continuous (#20687) feat(Data/Matroid/Rank/Cardinal): Cardinality-valued rank function (#20921) feat(Algebra): `Pi.single_induction` (#21141) chore(BigOperators/Fin): golf a proof (#21131) feat: generalize tangent cone lemmas to TVS (#20859) feat(CategoryTheory): `Comma.snd L R` is final if `R` is final and domains are filtered (#21136) refactor: unapply matrix lemmas (#21091) chore(Algebra/Category): `erw` -> `rw` (#21130) feat(CategoryTheory): filteredness of Comma catgories given finality of one of the functors (#21128) feat(Algebra/Category): `ConcreteCategory` instance for `ModuleCat` (#21125) feat: PSum of finite sorts is finite (#20285) feat: inequality on the integral of a convex function of a RN derivative (#21093) feat: `(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t` (#21058) chore: rename the fact that `(∀ a < a₁, a ≤ a₂) ↔ a₁ ≤ a₂` in a dense order (#20317) feat: a `RelHom` preserves directedness (#20080) feat(Combinatorics/SimpleGraph): add definitions and theorems about the coloring of sum graphs (#18677) chore(Data/Matrix/PEquiv): clean up names (#21108) feat(Algebra/Category): `ConcreteCategory` instances for rings (#20815) feat: define Descriptive.Tree (#18763) chore(Data/Complex/Exponential): split trig functions to new file (#21075) feat(Logic/IsEmpty/Relator): empty on sides (#20319) feat(Algebra/Category): `ConcreteCategory` instance for `AlgebraCat` (#21121) feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) (#20661) feat(RingTheory/LaurentSeries): add algebraEquiv (#21004) chore(SetTheory/Game/Impartial): golf two proofs (#21074) feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves (#21047) feat(RingTheory/IntegralClosure): `Algebra.IsIntegral` transfers via surjective homomorphisms (#21023) feat(`InformationTheory/Hamming`): Add AddGroup instances (#20994) feat(RingTheory/IntegralClosure): prove `Module.Finite R (adjoin R S)` for finite set `S` of integral elements (#20970) ...

xroblot added 5 commits January 11, 2025 16:11

1st commit

f86eaba

Change name

1287199

Better version

e4e2395

Docstring

90d7c92

1st part

d81b916

xroblot mentioned this pull request Jan 11, 2025

[Merged by Bors] - feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 2) #20660

Closed

2 tasks

xroblot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Jan 11, 2025

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 11, 2025

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 Jan 18, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 20, 2025

xroblot added 2 commits January 21, 2025 08:04

Merge remote-tracking branch 'origin/master' into xfr_lseries-sumcoeff1

36e7cec

clean up + docstrings

bdf4aa8

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 Jan 21, 2025

xroblot requested a review from loefflerd January 21, 2025 09:16

loefflerd reviewed Jan 22, 2025

View reviewed changes

Mathlib/NumberTheory/LSeries/SumCoeff.lean Outdated Show resolved Hide resolved

Mathlib/NumberTheory/LSeries/SumCoeff.lean Outdated Show resolved Hide resolved

Mathlib/NumberTheory/LSeries/SumCoeff.lean Outdated Show resolved Hide resolved

xroblot added 2 commits January 24, 2025 08:27

Review

9d4a621

Not a simp

a718bfe

xroblot added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 24, 2025

xroblot added 5 commits January 25, 2025 17:28

(almost) no more private

49fb178

fix docstrings

55e2e3c

Merge remote-tracking branch 'origin/master' into xfr_lseries-sumcoeff1

5234e3c

Fix name

0f330d5

Change name

6df822d

xroblot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 25, 2025

loefflerd approved these changes Jan 26, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 26, 2025

MichaelStollBayreuth reviewed Jan 26, 2025

View reviewed changes

Mathlib/NumberTheory/LSeries/SumCoeff.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth reviewed Jan 26, 2025

View reviewed changes

Mathlib/NumberTheory/LSeries/SumCoeff.lean Outdated Show resolved Hide resolved

xroblot added 2 commits January 26, 2025 17:19

Review (1)

16a5245

Review (2)

9393259

loefflerd reviewed Jan 26, 2025

View reviewed changes

Mathlib/NumberTheory/LSeries/SumCoeff.lean Outdated Show resolved Hide resolved

Unsqueeze

a49515e

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jan 27, 2025

mathlib-bors bot changed the title ~~feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1)~~ [Merged by Bors] - feat(NumberTheory/LSeries): results involving partial sums of coefficients (part 1) Jan 27, 2025

mathlib-bors bot closed this Jan 27, 2025

mathlib-bors bot deleted the xfr_lseries-sumcoeff1 branch January 27, 2025 10:51

Conversation

xroblot commented Jan 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary a49515e3d9

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jan 20, 2025

Uh oh!

loefflerd left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

loefflerd left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

xroblot commented Jan 23, 2025

Uh oh!

xroblot commented Jan 25, 2025

Uh oh!

loefflerd left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Jan 26, 2025

Uh oh!

Uh oh!

Uh oh!

xroblot commented Jan 26, 2025

Uh oh!

Uh oh!

riccardobrasca commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

xroblot commented Jan 27, 2025

Uh oh!

mathlib-bors bot commented Jan 27, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

xroblot commented Jan 11, 2025 •

edited

Loading

github-actions bot commented Jan 11, 2025 •

edited

Loading