[Merged by Bors] - feat(Analysis/Analytic/Meromorphic): more API for meromorphic functions #9621
Conversation
loefflerd
added
awaiting-review
leanprover-community-mathlib4-bot
added
the
merge-conflict
loefflerd
force-pushed
the
DL_meromorphic_order
branch
from
a4861e1
to
4a99220
Compare
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero ⟨g, hg_an, hg_ne, hg_eq⟩⟩ | ||
|
|
||
| /-- Compatibility of notions of `order` for analytic and meromorphic functions. -/ | ||
| lemma order_of_analyticAt {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) : |
There was a problem hiding this comment.
could you change the name of the lemma and move it into the AnalyticAt namespace?
| ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ z in 𝓝[≠] x, f z = (z - x) ^ n • g z := by | ||
| constructor | ||
| · intro hf_m | ||
| rcases eq_or_ne hf_m.order ⊤ with ho | ho |
There was a problem hiding this comment.
do you really need to use the order for this? You could just start from the definition of a meromorphic function, and multiply by (z - x) ^ (-n).
| MeromorphicOn f U := | ||
| fun x hx ↦ (hf x hx).meromorphicAt | ||
|
|
||
| lemma meromorphicOn_id {U : Set 𝕜} : MeromorphicOn id U := fun x _ ↦ meromorphicAt_id x |
There was a problem hiding this comment.
With the new dot notation in Lean 4, this kind of lemma should be named MeromorphicOn.id. The reason is that, if you're proving that a function is MeromorphicOn, then Lean 4 will let you use .id for MeromorphicOn.id, and it turns out to be really convenient. Same thing below for const.
|
✌️ loefflerd can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
|
Many thanks @sgouezel for the review! bors r+ |
…ns (#9621) This PR adds "order of vanishing" for meromorphic functions, and some basic API for functions `MeromorphicOn` a set.
|
Build failed (retrying...): |
…ns (#9621) This PR adds "order of vanishing" for meromorphic functions, and some basic API for functions `MeromorphicOn` a set.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…ns (#9621) This PR adds "order of vanishing" for meromorphic functions, and some basic API for functions `MeromorphicOn` a set.
This PR adds "order of vanishing" for meromorphic functions, and some basic API for functions
MeromorphicOna set.