refactor: golf CStarAlgebra/Unitization, Complex/Trigonometric, Asymptotics/SpecificAsymptotics

[yuanyi-350]

This PR extracts three file-level refactors from #37968 into a standalone branch:

• Mathlib/Analysis/CStarAlgebra/Unitization.lean
• Mathlib/Analysis/Complex/Trigonometric.lean
• Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

The goal is to make these simplifications reviewable independently of the larger batch PR.

[github-actions]

PR summary 14ec76b5f0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[themathqueen]

!radar

[leanprover-radar]

Benchmark results for 2850e01 against 14ec76b are in. There are significant results. @themathqueen

• 🟥 build//instructions: +5.0G (+0.00%)

Large changes (1🟥)

• 🟥 build/module/Mathlib.Analysis.CStarAlgebra.Unitization//instructions: +8.2G (+20.57%)

Small changes (1✅, 1🟥)

• ✅ build/module/Mathlib.Analysis.Asymptotics.SpecificAsymptotics//instructions: -1.8G (-10.94%)
• 🟥 build/module/Mathlib.CategoryTheory.Limits.Shapes.IsTerminal//instructions: +771.9M (+3.58%)

[yuanyi-350]

I ran a profiler comparison for the changed declarations in this PR.

Results (seconds):

• Asymptotics.isLittleO_pow_pow_cobounded_of_lt: 0.346176 -> 0.060680 (-82.5%)
• Unitization.instCStarRing: 1.152755 -> 2.749847 (+138.5%)
• Complex.cos_three_mul: 0.054808 -> 0.006588 (-88.0%)
• Complex.sin_three_mul: 0.058487 -> 0.376893 (+544.4%)

Overall:

• Asymptotics.isLittleO_pow_pow_cobounded_of_lt and Complex.cos_three_mul got faster.
• Unitization.instCStarRing and especially Complex.sin_three_mul got slower.

Caveat:

• These are single-run trace.profiler measurements of the Elab.definition.value entries after lake -R exe cache get.
• I used the PR merge-base 14ec76b5f0 for before and PR head 2850e0138e for after.
• I set trace.profiler.threshold := 0 for the Complex declarations so the sub-10ms entries would be reported.

[yuanyi-350]

I have updated the PR. I removed Unitization.instCStarRing and Complex.sin_three_mul, which were severely hurting performance. Now only Asymptotics.isLittleO_pow_pow_cobounded_of_lt and Complex.cos_three_mul remain.

[themathqueen]

I wouldn't revert yet. Let's see what others say about it?

[themathqueen]

Can you add a comment in Unitization.instCStarRing that says something like "grind works here but is slow"?

[yuanyi-350]

Can you add a comment in Unitization.instCStarRing that says something like "grind works here but is slow"?

Done.

[themathqueen]

This seems fine. I'm not too familiar with the Asymptotic files, so I'm not entirely sure for that (but it looks fine?).

If you want you can move it to a different PR along with other similar files?

[Parcly-Taxel]

No need to add this comment.

[themathqueen]

I don't know, might be okay. Maybe it'll be faster in the future, and then we can use it? I'll leave this for other reviewers:

Suggested change

-- `grind` works here but is much slower

[grunweg]

Please follow the requests made in the comments here and here, if still necessary. (You should still update the PR description, for instance.) Thanks!