[Merged by Bors] - feat: use new predicate Meromorphic

[kebekus]

Following a discussion of Zulip, this very short PR ports the first functions to use the new predicate Meromorphic. Introduce two fun_props along the way. A much more massive PR that ports Value Distribution Theory will follow in a separate PR.

#mathlib4 > Introducing Meromorphic @ 💬

---

[github-actions]

PR summary 3cfe59e733

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ MeromorphicOn.countable_compl_analyticAt
+ MeromorphicOn.measurable
+ inv
+ smul

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]

I don't think we generally include the new declaration Meromorphic.meromorphicOn_univ. It would need to be protected if we did, but you should also just be able to use Meromorphic.meromorphicOn. When Lean can infer univ, it works, and when it can't, you can simply supply the implicit argument manually.

[kebekus]

Removed Meromorphic.meromorphicOn_univ as suggested by @j-loreaux

[j-loreaux]

bors merge

[mathlib-bors]

Merge conflict.

[mathlib4-merge-conflict-bot]

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

[kebekus]

@j-loreaux The merge conflict is now fixed.

[j-loreaux]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Post-Build Step
• Build
• Lint style