[Merged by Bors] - feat: API for continuous extension of meromorphic functions #22867

kebekus · 2025-03-12T08:30:23Z

Defines the normal form of meromorphic functions and provides API for continuous extension, as discussed on Zulip. More material will be provided in upcoming PRs.

This material is used in Project VD, which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

github-actions · 2025-03-12T08:32:12Z

PR summary 3a93a46216

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.Meromorphic.NormalFormAt` (new file)	1644

Declarations diff

+ AnalyticAt.meromorphicNFAt
+ MeromorphicAt.eqOn_compl_singleton_toMermomorphicNFAt
+ MeromorphicAt.eq_nhdNE_toMeromorphicNFAt
+ MeromorphicNFAt
+ MeromorphicNFAt.meromorphicAt
+ MeromorphicNFAt.order_nonneg_iff_analyticAt
+ eventuallyEq_nhds_of_eventuallyEq_nhdsNE
+ meromorphicNFAt_congr
+ meromorphicNFAt_iff_analyticAt_or
+ meromorphicNFAt_toMeromorphicNFAt
+ toMeromorphicNFAt
+ toMeromorphicNFAt_eq_self
+ toMeromorphicNFAt_of_not_meromorphicAt

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

Mathlib/Analysis/Analytic/IsolatedZeros.lean

Mathlib/Analysis/Meromorphic/NormalFormAt.lean

Co-authored-by: Yaël Dillies <[email protected]>

Co-authored-by: Johan Commelin <[email protected]>

Mathlib/Analysis/Meromorphic/NormalFormAt.lean

Co-authored-by: Yaël Dillies <[email protected]>

Mathlib/Analysis/Analytic/IsolatedZeros.lean

Co-authored-by: Yaël Dillies <[email protected]>

loefflerd

I took a careful look through this and found some golfs, and a few minor renaming suggestions, but the overall design looks great. Thanks for this nice contribution!

Mathlib/Analysis/Meromorphic/NormalFormAt.lean

Co-authored-by: David Loeffler <[email protected]>

Mathlib/Analysis/Meromorphic/NormalFormAt.lean

Co-authored-by: Yaël Dillies <[email protected]>

…ver-community/mathlib4 into kebekus/meromorphic_normalFormAt

Co-authored-by: Yaël Dillies <[email protected]>

loefflerd · 2025-03-16T09:21:37Z

I believe this PR is now ready for merging. One can debate forever about code-style issues, aesthetics etc; but I think all the necessary functionality is now present and in a good shape, and we shouldn't hold up the larger project of which this is part with further nit-picking.

maintainer merge

github-actions · 2025-03-16T09:21:55Z

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

kbuzzard

This looks great! I particularly like the (currently apparently rather unfashionable) idea of putting docstrings on the key theorems. I had a docstring nit.

bors d+

Mathlib/Analysis/Meromorphic/NormalFormAt.lean

mathlib-bors · 2025-03-16T10:56:54Z

✌️ kebekus can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Kevin Buzzard <[email protected]>

kebekus · 2025-03-16T12:35:34Z

@jcommelin @YaelDillies @loefflerd @kbuzzard Thank you for the incredible work and all the time and effort you are putting into this.

bors r+

Defines the normal form of meromorphic functions and provides API for continuous extension, as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/API.20for.20continuous.20extension.20of.20meromorphic.20functions). More material will be provided in upcoming PRs. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane.

mathlib-bors · 2025-03-16T13:01:46Z

Pull request successfully merged into master.

Build succeeded:

…vProdLpPiLp` (#22993) * feat: scalar tower instances for quotients (#22951) We already have the `SMulCommClass` and `IsScalarTower` versions for `RingQuot`; this develops them for `Con` and `RingCon`, with the eventual aim of replacing `RingQuot` with `RingCon.Quotient`. * chore(Order/Group/Abs): use `@[to_additive]` (#22468) * feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic (#22843) This PR adds some elementary results about the prime subfield of a characteristic p field, e.g., size is p, elements are integer multiples of one, and elements are characterized by being fixed by the p-th power map. * docs(Data/Real/EReal): fix capitalization error (#22943) Changes `Ereal` to `EReal` in the module docstring for `Data/Real/EReal`. * chore(Ideal/Quotient): change `Fintype` to `Finite` (#22947) As discussed [here](#22902 (comment)) * feat: add `norm_num` extensions for factorials (#8832) Add `norm_num` extensions to evaluate `Nat.factorial`, `Nat.ascFactorial` and `Nat.descFactorial`. Co-authored-by: Eric Wieser <[email protected]> * perf(CategoryTheory/Limits/Shapes): reorder instance arguments (#22968) This PR is in the same spirit as #22953. The problem is that some instances about category theoretical limits have silly side conditions that end up searching through the whole algebraic type class hierarchy. This PR attempts to keep the type class search limited to category theoretical type classes. * feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940) * feat: API for continuous extension of meromorphic functions (#22867) Defines the normal form of meromorphic functions and provides API for continuous extension, as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/API.20for.20continuous.20extension.20of.20meromorphic.20functions). More material will be provided in upcoming PRs. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. * feat(Data/Complex/Trigonometric): closer upper bound for cos 1 (#22945) cos 1 is approximately 0.5403..., so this bound is fairly tight. Co-authored-by: Vlad Tsyrklevich <[email protected]> * chore: move `List.Lex` lemmas out of the `List.Lex` namespace (#22935) This better matches the naming convention. * working on it. * Added sup_disjSum and inf_disjSum. * Finished one branch. * Finished proof. --------- Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Yury G. Kudryashov <[email protected]> Co-authored-by: Scott Carnahan <[email protected]> Co-authored-by: plp127 <[email protected]> Co-authored-by: Xavier Roblot <[email protected]> Co-authored-by: Sebastian Zimmer <[email protected]> Co-authored-by: JovanGerb <[email protected]> Co-authored-by: Stefan Kebekus <[email protected]> Co-authored-by: Vlad Tsyrklevich <[email protected]> Co-authored-by: Vlad Tsyrklevich <[email protected]> Co-authored-by: Yaël Dillies <[email protected]>

kebekus added 3 commits March 12, 2025 08:57

Working…

53bd594

Update Mathlib.lean

6294aef

Update ContinuousOn.lean

1f0faad

Fix docstrings

db4b87e

kebekus requested review from jcommelin, YaelDillies, loefflerd and sgouezel March 12, 2025 09:21

kebekus added the t-analysis Analysis (normed *, calculus) label Mar 12, 2025

jcommelin reviewed Mar 12, 2025

View reviewed changes

kebekus and others added 3 commits March 12, 2025 15:52

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

cc4998f

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

d401099

Co-authored-by: Johan Commelin <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

18c8cfe

Co-authored-by: Johan Commelin <[email protected]>

YaelDillies reviewed Mar 12, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 12, 2025

kebekus and others added 6 commits March 12, 2025 20:42

Fix naming

96140d3

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

aa448af

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

1192f02

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

348c17c

Co-authored-by: Yaël Dillies <[email protected]>

Implement Yael's suggestion

cc5bcc9

Update NormalFormAt.lean

42c7ac2

YaelDillies reviewed Mar 12, 2025

View reviewed changes

Mathlib/Analysis/Analytic/IsolatedZeros.lean Outdated Show resolved Hide resolved

Mathlib/Analysis/Analytic/IsolatedZeros.lean Outdated Show resolved Hide resolved

Update Mathlib/Analysis/Analytic/IsolatedZeros.lean

f800bac

Co-authored-by: Yaël Dillies <[email protected]>

loefflerd reviewed Mar 13, 2025

View reviewed changes

kebekus and others added 5 commits March 13, 2025 17:43

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

1e7fcb0

Co-authored-by: David Loeffler <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

dec5493

Co-authored-by: David Loeffler <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

2029023

Co-authored-by: David Loeffler <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

19582b4

Co-authored-by: David Loeffler <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

4658f38

Co-authored-by: David Loeffler <[email protected]>

kebekus added 2 commits March 16, 2025 08:53

Update NormalFormAt.lean

08d9c73

Update NormalFormAt.lean

7a7215a

kebekus removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 16, 2025

YaelDillies reviewed Mar 16, 2025

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 16, 2025

kebekus and others added 9 commits March 16, 2025 09:19

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

21bbf7b

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

9ea61c1

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

935d4f0

Co-authored-by: Yaël Dillies <[email protected]>

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

f76dd7a

Co-authored-by: Yaël Dillies <[email protected]>

Update NormalFormAt.lean

8ae7645

Merge branch 'kebekus/meromorphic_normalFormAt' of github.com:leanpro…

b50d621

…ver-community/mathlib4 into kebekus/meromorphic_normalFormAt

Update NormalFormAt.lean

b92d4fb

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

3261aa2

Co-authored-by: Yaël Dillies <[email protected]>

Update NormalFormAt.lean

b9725f1

kebekus removed the awaiting-author A reviewer has asked the author a question or requested changes label Mar 16, 2025

github-actions bot added the maintainer-merge label Mar 16, 2025

kbuzzard approved these changes Mar 16, 2025

View reviewed changes

Mathlib/Analysis/Meromorphic/NormalFormAt.lean Outdated Show resolved Hide resolved

leanprover-community-mathlib4-bot added delegated and removed maintainer-merge labels Mar 16, 2025

Update Mathlib/Analysis/Meromorphic/NormalFormAt.lean

3a93a46

Co-authored-by: Kevin Buzzard <[email protected]>

mathlib-bors bot changed the title ~~feat: API for continuous extension of meromorphic functions~~ [Merged by Bors] - feat: API for continuous extension of meromorphic functions Mar 16, 2025

mathlib-bors bot closed this Mar 16, 2025

mathlib-bors bot deleted the kebekus/meromorphic_normalFormAt branch March 16, 2025 13:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: API for continuous extension of meromorphic functions #22867

[Merged by Bors] - feat: API for continuous extension of meromorphic functions #22867

kebekus commented Mar 12, 2025 •

edited

Loading

github-actions bot commented Mar 12, 2025 •

edited

Loading

Declarations diff

loefflerd left a comment

loefflerd commented Mar 16, 2025

github-actions bot commented Mar 16, 2025

kbuzzard left a comment

mathlib-bors bot commented Mar 16, 2025

kebekus commented Mar 16, 2025

mathlib-bors bot commented Mar 16, 2025

[Merged by Bors] - feat: API for continuous extension of meromorphic functions #22867

[Merged by Bors] - feat: API for continuous extension of meromorphic functions #22867

Conversation

kebekus commented Mar 12, 2025 • edited Loading

github-actions bot commented Mar 12, 2025 • edited Loading

PR summary 3a93a46216

Import changes for modified files

Declarations diff

loefflerd left a comment

Choose a reason for hiding this comment

loefflerd commented Mar 16, 2025

github-actions bot commented Mar 16, 2025

kbuzzard left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Mar 16, 2025

kebekus commented Mar 16, 2025

mathlib-bors bot commented Mar 16, 2025

kebekus commented Mar 12, 2025 •

edited

Loading

github-actions bot commented Mar 12, 2025 •

edited

Loading