[Merged by Bors] - feat(Analysis/SpecialFunctions): iterated derivative of cotangent

[CBirkbeck]

---

• depends on: [Merged by Bors] - feat: iteratedDerivWithin version of zpow lemmas #27209
• depends on: [Merged by Bors] - Iterated derivatives of tsum's within some open set. #26016
• depends on: [Merged by Bors] - feat(NumberTheory/ModularForms): the Dedekind Eta function #28400

[github-actions]

PR summary 0ad288bf4a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent	2496	2498	+2 (+0.08%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent	2

---

Declarations diff

+ abs_norm_eq_max_natAbs
+ abs_norm_eq_max_natAbs_neg
+ cot_pi_mul_contDiffWithinAt
+ differentiableOn_iteratedDerivWithin_cotTerm
+ eqOn_iteratedDerivWithin_cotTerm_integerComplement
+ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet
+ eqOn_iteratedDeriv_cotTerm
+ iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow
+ iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow
+ iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum
+ sin_pi_mul_ne_zero
+ summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm
+ upperHalfPlane_inter_integerComplement
- sin_pi_z_ne_zero

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

[CBirkbeck]

Can you try to be more consistent regarding lemma vs. theorem? I think the idea is that theorems are the more interesting statments (and should have docstrings), whereas lemma is for the auxiliary and less interesting or boring stuff. (mathport turned all lemmas into theorems, so this is not very consistent in current Mathlib, but I think it makes sense to do that for new stuff.)

Sorry I was still under the impression that lemma and theorem were treated the same in mathlib. These were named theorems either from the mathport, but also extract_goal automatically calls them theorems and I never changed that bit. But I think it would be nice to have it as you say so I'll do that going forward thanks!

[MichaelStollBayreuth]

Instead of fun x ↦ π * Complex.cot (π * x) you could write fun x : ℂ ↦ π * cot (π * x) (the Complex namespace is open, and specifying the type of x resolves the ambiguity), but this is a matter of taste.

[MichaelStollBayreuth]

LGTM now.

maintainer merge

[github-actions]

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

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success