Skip to content

feat(Analysis): characterizing and congr lemma for toMeromorphicNFAt #41092

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wwylele wants to merge 3 commits into
base: master
Choose a base branch
from
Open

feat(Analysis): characterizing and congr lemma for toMeromorphicNFAt #41092

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1833ce9
feat(Analysis): characterizing and congr lemma for toMeromorphicNFAt
wwylele Jun 27, 2026
b367868
fix name
wwylele Jun 27, 2026
d6d284f
Apply suggestions from code review
wwylele Jun 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions Mathlib/Analysis/Meromorphic/NormalForm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -437,11 +437,47 @@ lemma MeromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt (hf : MeromorphicAt f
toMeromorphicNFAt f x = 0 := by
simp [toMeromorphicNFAt, hf]

@[simp] lemma toMeromorphicNFAt_of_meromorphicOrderAt_ne_zero
(horder : meromorphicOrderAt f x ≠ 0) : toMeromorphicNFAt f x x = 0 := by
simp [toMeromorphicNFAt, meromorphicAt_of_meromorphicOrderAt_ne_zero, horder]

lemma MeromorphicAt.exists_analyticAt_and_toMeromorphicNFAt_eventuallyEq (hf : MeromorphicAt f x)
Comment thread
themathqueen marked this conversation as resolved.
(horder : meromorphicOrderAt f x = 0) :
∃ g : 𝕜 → E, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ toMeromorphicNFAt f x =ᶠ[𝓝 x] g := by
have := (meromorphicOrderAt_eq_int_iff hf).mp horder
obtain ⟨hanalytic, hgx, hg⟩ := this.choose_spec
refine ⟨this.choose, hanalytic, hgx, eventuallyEq_nhds_of_eventuallyEq_nhdsNE ?_ ?_⟩
Comment thread
themathqueen marked this conversation as resolved.
· trans f
· classical simpa [toMeromorphicNFAt, hf] using Function.update_eventuallyEq_nhdsNE _ _ _ _
simpa [Filter.EventuallyEq] using hg
· simp [toMeromorphicNFAt, hf, horder]

/-- Conversion to normal form at `x` changes the value only at x. -/
lemma MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt (hf : MeromorphicAt f x) :
f =ᶠ[𝓝[≠] x] toMeromorphicNFAt f x :=
eventually_nhdsWithin_of_forall (fun _ hz ↦ hf.eqOn_compl_singleton_toMeromorphicNFAt hz)

@[gcongr]
lemma toMeromorphicNFAt_congr {f g : 𝕜 → E} (hfg : f =ᶠ[𝓝[≠] x] g) :
toMeromorphicNFAt f x x = toMeromorphicNFAt g x x := by
by_cases hf : MeromorphicAt f x
<;> obtain hg := (MeromorphicAt.meromorphicAt_congr hfg).eq ▸ hf
· by_cases hforder : meromorphicOrderAt f x = 0
<;> obtain hgorder := meromorphicOrderAt_congr hfg ▸ hforder
· obtain ⟨f', hf'anl, _, hf'⟩ :=
hf.exists_analyticAt_and_toMeromorphicNFAt_eventuallyEq hforder
obtain ⟨g', hg'anl, _, hg'⟩ :=
hg.exists_analyticAt_and_toMeromorphicNFAt_eventuallyEq hgorder
have hf'g' : f' =ᶠ[𝓝[≠] x] g' := (hf'.symm.filter_mono nhdsWithin_le_nhds).trans <|
hf.eq_nhdsNE_toMeromorphicNFAt.symm.trans <| hfg.trans <|
hg.eq_nhdsNE_toMeromorphicNFAt.trans <|
hg'.filter_mono nhdsWithin_le_nhds
have heq : f' x = g' x := Filter.EventuallyEq.eq_of_nhds
((AnalyticAt.frequently_eq_iff_eventually_eq hf'anl hg'anl).mp hf'g'.frequently)
exact hf'.eq_of_nhds.trans <| heq.trans hg'.eq_of_nhds.symm
· simp [hforder, hgorder]
· simp [hf, hg]

/-- After conversion to normal form at `x`, the function has normal form. -/
theorem meromorphicNFAt_toMeromorphicNFAt :
MeromorphicNFAt (toMeromorphicNFAt f x) x := by
Expand Down
Loading