feat(Manifold/MFDeriv): add fun_prop to MDifferentiable

[seewoo5]

---

Add FunProp to MDifferentiable. For example, the following works (when F' is normed 𝕜-algebra)

example (hp : MDifferentiable I 𝓘(𝕜, F') p) (hq : MDifferentiable I 𝓘(𝕜, F') q) :
    MDifferentiable I 𝓘(𝕜, F') ((p * q + p - q) * q * p) := by fun_prop

Motivated from sphere packing project.

[github-actions]

PR summary cb3ccde1ed

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

[grunweg]

Hi! Thank you for making this PR. Indeed, fun_prop support for MDifferentiable and ContMDiff is sorely missing, and I appreciate you wanting to change this. That said, there is a good reason this tagging has not been made yet, having to do with the design of the manifold library. To apply MDifferentiable.comp (or any of its cousins), fun_prop needs to find a model with corners on the intermediate manifold. This problem does not have a unique solution in general; in particular, you cannot rely on typeclass inference or unification. (There is a silver lining; you can write custom code to enable inferring the model in the vast majority of cases where it is unique. I have a prototype for this and will supervise a master's student to complete this, starting in March.)

In the mean-time, I am not sure if we want to merge this PR. Tagging the comp lemma (or in general, tagging this property with fun_prop) may induce the expectation that fun_prop just works here, which is decidedly not the case. I'd rather fix this properly, than land a half-baked solution now and deal with the user confusion. Can you live with maintaining these tags (ideally, with some warning that this is not robust support yet) in the sphere-packing repository for a little while? Once fun_prop support has improved, I'll gladly review a PR making these tags.

[grunweg]

Regarding this PR itself: if you're tagging MDifferentiable, I would also expect tags on MDifferentiableAt, and presumably also MDifferentiableOn and MDifferentiableWithinAt (to match what we do for Differentiable). That's a secondary concern compared to my previous comment.

[seewoo5]

Hi! Thank you for making this PR. Indeed, fun_prop support for MDifferentiable and ContMDiff is sorely missing, and I appreciate you wanting to change this. That said, there is a good reason this tagging has not been made yet, having to do with the design of the manifold library. To apply MDifferentiable.comp (or any of its cousins), fun_prop needs to find a model with corners on the intermediate manifold. This problem does not have a unique solution in general; in particular, you cannot rely on typeclass inference or unification. (There is a silver lining; you can write custom code to enable inferring the model in the vast majority of cases where it is unique. I have a prototype for this and will supervise a master's student to complete this, starting in March.)

In the mean-time, I am not sure if we want to merge this PR. Tagging the comp lemma (or in general, tagging this property with fun_prop) may induce the expectation that fun_prop just works here, which is decidedly not the case. I'd rather fix this properly, than land a half-baked solution now and deal with the user confusion. Can you live with maintaining these tags (ideally, with some warning that this is not robust support yet) in the sphere-packing repository for a little while? Once fun_prop support has improved, I'll gladly review a PR making these tags.

Thank you, I wasn't aware of that. Does it mean that I can still fun_prop-ing for specific model with corners? For the actual application on sphere packing side, every function will be a modularform-like objects with same domain (upper half plane) and codomain (C). I believe I can do this on sphere packing repo (probably put fun_prop there?), and then remove them when everything is ready and this PR got merged.

Regarding this PR itself: if you're tagging MDifferentiable, I would also expect tags on MDifferentiableAt, and presumably also MDifferentiableOn and MDifferentiableWithinAt (to match what we do for Differentiable). That's a secondary concern compared to my previous comment.

Yes, I agree with it. I can also take account this later.

In that case, is it still makes sense to add pow as introduced in #33814 without fun_prop? If it is, I can make new PR for it.

[grunweg]

Does it mean that I can still fun_prop-ing for specific model with corners? For the actual application on sphere packing side, every function will be a modularform-like objects with same domain (upper half plane) and codomain (C). I believe I can do this on sphere packing repo (probably put fun_prop there?), and then remove them when everything is ready and this PR got merged.

If fun_prop works in your repository, it works (and I'm not telling you to not use, merely that this will not be robust).
You can of course maintain all fun_prop annotations in your repository that you find useful (and you submitting these once fun_prop is more powerful is helpful!). Writing attribute [fun_prop] mylemma tags a lemma with fun_prop (at every point after writing this, and also in all downstream files), so you can emulate fun_prop tags in mathlib in your project.

[grunweg]

Since we have Differentiable.pow: sure, why not add MDifferentiable versions? I'll be happy to review a new PR. Please do add MDifferentiableAt, MDifferentiableOn and MDifferentiableWithinAt version. Thanks!

[grunweg]

(At some point, we should have automation to verify that these sets of lemmas are in sync. But that's a different matter.)

[seewoo5]

Since we have Differentiable.pow: sure, why not add MDifferentiable versions? I'll be happy to review a new PR. Please do add MDifferentiableAt, MDifferentiableOn and MDifferentiableWithinAt version. Thanks!

I made #33830 !