[Merged by Bors] - feat(NumberTheory/Divisors): divisors antidiagonal tsum

[CBirkbeck]

---

• depends on: [Merged by Bors] - feat(NumberTheory/Divisors): add divisorAntidiagonal equivalence. #27837

[github-actions]

PR summary 8bd4d3ea3d

Import changes exceeding 2%

%	File
+119.28%	Mathlib.NumberTheory.TsumDivsorsAntidiagonal

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.TsumDivsorsAntidiagonal	726	1592	+866 (+119.28%)

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.TsumDivsorsAntidiagonal	866

---

Declarations diff

+ Summable.mul_tendsto_const
+ norm_natCast
+ sigma_eq_sum_div
+ summable_norm_pow_mul_geometric_div_one_sub
+ summable_prod_mul_pow
+ tprod_congr₂
+ tsum_pow_div_one_sub_eq_tsum_sigma
+ tsum_prod_pow_eq_tsum_sigma

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]

This PR/issue depends on:

• [Merged by Bors] - feat(NumberTheory/Divisors): add divisorAntidiagonal equivalence. #27837
  By Dependent Issues (🤖). Happy coding!

[CBirkbeck]

I think I was talking rubbish earlier about the norm_natCast simp lemmas. I think you can just revert the changes in Mathlib/Analysis/Complex/Exponential.lean, Mathlib/Analysis/Complex/Norm.lean, Mathlib/Analysis/RCLike/Basic.lean and Mathlib/Analysis/Normed/Group/Basic.lean. I was mistaken in thinking this would somehow conflict with the general simp lemma you're adding in Mathlib/Analysis/Normed/Module/Basic.lean. (What I missed is that when the specific norm_natCast lemmas for ℝ, ℂ and an RCLike are stated, mathlib doesn't yet know that these types have an [NormSMulClass ℤ -] instance, because it is only created later using precisely these lemmas!)

So that was a complete distraction from the actual content of this PR. I hope to have some time to look at this properly either tomorrow, or early next week.

Hmm well the build was failing at the RCLike file, so that one does need changing. I think it does break at the other places as well, but I'll see if it builds first before changing them. Edit: Yep it breaks without this.

[loefflerd]

Hmm well the build was failing at the RCLike file, so that one does need changing. I think it does break at the other places as well, but I'll see if it builds first before changing them. Edit: Yep it breaks without this.

I'm surprised. I made #29386, which is a fork of this PR, so I can play around with the simp-tagging changes. I will experiment & get back to you.

[loefflerd]

... and it genuinely doesn't work. Looks like I was actually correct first time around in guessing that the simp lemmas would need corrective action downstream. OK, I believe now that the current state of this PR is the Right Thing.

[loefflerd]

I think this is pretty much ready now. Some of the lemmas maybe don't look "natural" in their statements but this is probably inevitable for an early stage of a large multi-PR project.

maintainer delegate

[github-actions]

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

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ 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.

[CBirkbeck]

bors r+

[mathlib-bors]

Build failed (retrying...):

• CI Success

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success