feat(Analysis): derivative of Weierstrass ℘

[erdOne]

---

[github-actions]

PR summary 97f41d5185

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass	2287	2303	+16 (+0.70%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass	16

---

Declarations diff

+ derivWeierstrassP
+ derivWeierstrassPExcept
+ derivWeierstrassPExcept_add_coe
+ derivWeierstrassPExcept_def
+ derivWeierstrassPExcept_neg
+ derivWeierstrassPExcept_of_notMem
+ derivWeierstrassPExcept_sub
+ derivWeierstrassP_add_coe
+ derivWeierstrassP_coe
+ derivWeierstrassP_neg
+ derivWeierstrassP_sub_coe
+ derivWeierstrassP_zero
+ deriv_weierstrassP
+ differentiableOn_derivWeierstrassP
+ differentiableOn_derivWeierstrassPExcept
+ differentiableOn_weierstrassP
+ differentiableOn_weierstrassPExcept
+ eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept
+ hasSumLocallyUniformly_derivWeierstrassP
+ hasSumLocallyUniformly_derivWeierstrassPExcept
+ hasSumLocallyUniformly_weierstrassP
+ hasSumLocallyUniformly_weierstrassPExcept
+ hasSum_derivWeierstrassP
+ hasSum_derivWeierstrassPExcept
+ hasSum_weierstrassP
+ hasSum_weierstrassPExcept
+ isOpen_compl_lattice_diff
+ not_continuousAt_weierstrassP
+ weierstrassP
+ weierstrassPExcept
+ weierstrassPExcept_add
+ weierstrassPExcept_def
+ weierstrassPExcept_neg
+ weierstrassPExcept_of_notMem
+ weierstrassP_add_coe
+ weierstrassP_bound
+ weierstrassP_coe
+ weierstrassP_neg
+ weierstrassP_sub_coe
+ weierstrassP_zero
- differentiableOn_℘
- differentiableOn_℘Except
- hasSumLocallyUniformly_℘
- hasSumLocallyUniformly_℘Except
- hasSum_℘
- hasSum_℘Except
- ℘
- ℘Except
- ℘Except_add
- ℘Except_def
- ℘Except_neg
- ℘Except_of_notMem
- ℘_bound
- ℘_neg

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

[j-loreaux]

This is nice! I only have a few comments, and I probably shouldn't be the one to merge this anyway. Others will have better things to say than me.

[j-loreaux]

I haven't checked how doable this is, but I think it would be much nicer if this were solvable by some have : correct_statement := by fun_prop; simpa using this or something of the sort. I can look into it another time if you don't get to it first. I think it would make it more readable.

[erdOne]

I tried a bit but I don't know how to make it work. In particular ContinuousOn.continuousAt is not fun_prop and probably couldn't be.

[j-loreaux]

I really don't like the use of a prime here (in the declaration name) to refer to the derivative of the Weierstrass function. Is there precedent for this?

[erdOne]

I assume the last question is directed towards other reviewers but for the record my opinion is that I don't think this name is particular bad and it is quite straightforward but I am happy to change it to anything better. And no I don't know this part of the library well enough to know about any precedents.

[loefflerd]

Yes, there is precedent: jacobiTheta₂' is the derivative (in one of its variables) of the two-variable Jacobi theta function, and there are some API lemmas about it with names like norm_jacobiTheta₂'_term_le which have the "infix '" as in ℘'Except.

FWIW, you may end up regretting these naming choices if you ever write a paper about this, like Michael and I did with the L-functions stuff. The problem is that LaTeX doesn't seem to cope well with hyperlinks to URL's with unicode characters in them – I spent hours trying to make our paper hyperlink to the ref manual entry for jacobiTheta₂', but never got it to work, and heartily wished I hadn't used the subscript 2. You may face the same problem with ℘: it might have been safer to call it weierstrassP and then have ℘ be a notation for that. But that's orthogonal to Jireh's remark which is about the ', not the curly-p glyph.

[j-loreaux]

Thanks for the pointer to precedent. But I agree that the naming here is not ideal. I think weierstrassP and derivWeierstrassP (or similar) along with some scoped notation would be the best choice. There are only 9 declarations mentioning PeriodPair.℘ and only 16 that have "℘" in the name, so I don't think this is too deeply embedded to be changed.

I realize that the ℘ issue is slightly orthogonal to the ' issue, but they are certainly related. They both boil down to: "we shouldn't conflate notation and naming".

[erdOne]

I have pushed a commit changing the name. I do think this makes the readability of lemma names significantly worse and places an unnecessary cognitive load on users but if this is what the reviews prefer then I will follow it.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.