feat: a continuous meromorphic function is analytic (#24370)

We also characterize the order of a meromorphic function being `< 0`, or `= 0`, or `> 0`, as the convergence of the function
to infinity, resp. a nonzero constant, resp. zero.

This is used to generalize `analyticAt_mem_codiscreteWithin`, and from there remove completeness assumptions throughout the meromorphic functions theory.

Author: sgouezel

Mathlib/Analysis/Analytic/Basic.lean

@@ -1322,6 +1322,14 @@ protected theorem AnalyticAt.continuousAt (hf : AnalyticAt 𝕜 f x) : Continuou
   let ⟨_, hp⟩ := hf
   hp.continuousAt
 
+protected theorem AnalyticAt.eventually_continuousAt (hf : AnalyticAt 𝕜 f x) :
+    ∀ᶠ y in 𝓝 x, ContinuousAt f y := by
+  rcases hf with ⟨g, r, hg⟩
+  have : EMetric.ball x r ∈ 𝓝 x := EMetric.ball_mem_nhds _ hg.r_pos
+  filter_upwards [this] with y hy
+  apply hg.continuousOn.continuousAt
+  exact EMetric.isOpen_ball.mem_nhds hy
+
 protected theorem AnalyticOnNhd.continuousOn {s : Set E} (hf : AnalyticOnNhd 𝕜 f s) :
     ContinuousOn f s :=
   fun x hx => (hf x hx).continuousAt.continuousWithinAt

Mathlib/Analysis/Meromorphic/Basic.lean

@@ -218,9 +218,25 @@ lemma zpow' {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) (n : ℤ) :
     MeromorphicAt (fun z ↦ (f z) ^ n) x :=
   hf.zpow n
 
+/-- If a function is meromorphic at a point, then it is continuous at nearby points. -/
+theorem eventually_continuousAt {f : 𝕜 → E} {x : 𝕜}
+    (h : MeromorphicAt f x) : ∀ᶠ y in 𝓝[≠] x, ContinuousAt f y := by
+  obtain ⟨n, h⟩ := h
+  have : ∀ᶠ y in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y :=
+    nhdsWithin_le_nhds h.eventually_continuousAt
+  filter_upwards [this, self_mem_nhdsWithin] with y hy h'y
+  simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at h'y
+  have : ContinuousAt (fun z ↦ ((z - x) ^ n)⁻¹) y :=
+    ContinuousAt.inv₀ (by fun_prop) (by simp [sub_eq_zero, h'y])
+  apply (this.smul hy).congr
+  filter_upwards [eventually_ne_nhds h'y] with z hz
+  simp [smul_smul, hz, sub_eq_zero]
+
+/-- In a complete space, a function which is meromorphic at a point is analytic at all nearby
+points. The completeness assumption can be dispensed with if one assumes that `f` is meromorphic
+on a set around `x`, see `MeromorphicOn.eventually_analyticAt`. -/
 theorem eventually_analyticAt [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜}
     (h : MeromorphicAt f x) : ∀ᶠ y in 𝓝[≠] x, AnalyticAt 𝕜 f y := by
-  rw [MeromorphicAt] at h
   obtain ⟨n, h⟩ := h
   apply AnalyticAt.eventually_analyticAt at h
   refine (h.filter_mono ?_).mp ?_
@@ -266,17 +282,6 @@ lemma const (e : E) {U : Set 𝕜} : MeromorphicOn (fun _ ↦ e) U :=
 
 section arithmetic
 
-include hf in
-/-- Meromorphic functions on `U` are analytic on `U`, outside of a discrete subset. -/
-theorem analyticAt_mem_codiscreteWithin [CompleteSpace E] :
-    { x | AnalyticAt 𝕜 f x } ∈ Filter.codiscreteWithin U := by
-  rw [mem_codiscreteWithin]
-  intro x hx
-  rw [Filter.disjoint_principal_right, ← Filter.eventually_mem_set]
-  apply (hf x hx).eventually_analyticAt.mono
-  simp only [Set.mem_compl_iff, Set.mem_diff, Set.mem_setOf_eq, not_and, not_not]
-  tauto
-
 include hf in
 lemma mono_set {V : Set 𝕜} (hv : V ⊆ U) : MeromorphicOn f V := fun x hx ↦ hf x (hv hx)
 

Mathlib/Analysis/Meromorphic/Divisor.lean

@@ -19,7 +19,7 @@ divisors.
 -/
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {U : Set 𝕜} {z : 𝕜}
-  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 
 namespace MeromorphicOn
 
@@ -90,7 +90,7 @@ See `MeromorphicOn.exists_order_ne_top_iff_forall` and
 `MeromorphicOn.order_ne_top_of_isPreconnected` for two convenient criteria to guarantee conditions
 `h₂f₁` and `h₂f₂`.
 -/
-theorem divisor_smul [CompleteSpace 𝕜] {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E} (h₁f₁ : MeromorphicOn f₁ U)
+theorem divisor_smul {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E} (h₁f₁ : MeromorphicOn f₁ U)
     (h₁f₂ : MeromorphicOn f₂ U) (h₂f₁ : ∀ z, (hz : z ∈ U) → (h₁f₁ z hz).order ≠ ⊤)
     (h₂f₂ : ∀ z, (hz : z ∈ U) → (h₁f₂ z hz).order ≠ ⊤) :
     divisor (f₁ • f₂) U = divisor f₁ U + divisor f₂ U := by
@@ -110,15 +110,15 @@ See `MeromorphicOn.exists_order_ne_top_iff_forall` and
 `MeromorphicOn.order_ne_top_of_isPreconnected` for two convenient criteria to guarantee conditions
 `h₂f₁` and `h₂f₂`.
 -/
-theorem divisor_mul [CompleteSpace 𝕜] {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ U)
+theorem divisor_mul {f₁ f₂ : 𝕜 → 𝕜} (h₁f₁ : MeromorphicOn f₁ U)
     (h₁f₂ : MeromorphicOn f₂ U) (h₂f₁ : ∀ z, (hz : z ∈ U) → (h₁f₁ z hz).order ≠ ⊤)
     (h₂f₂ : ∀ z, (hz : z ∈ U) → (h₁f₂ z hz).order ≠ ⊤) :
     divisor (f₁ * f₂) U = divisor f₁ U + divisor f₂ U :=
   divisor_smul h₁f₁ h₁f₂ h₂f₁ h₂f₂
 
 /-- The divisor of the inverse is the negative of the divisor. -/
 @[simp]
-theorem divisor_inv [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} :
+theorem divisor_inv {f : 𝕜 → 𝕜} :
     divisor f⁻¹ U = -divisor f U := by
   ext z
   by_cases h : MeromorphicOn f U ∧ z ∈ U

Mathlib/Analysis/Meromorphic/NormalForm.lean

@@ -127,7 +127,7 @@ theorem AnalyticAt.meromorphicNFAt (hf : AnalyticAt 𝕜 f x) :
 
 /-- Meromorphic functions have normal form outside of a discrete subset in the domain of
 meromorphicity. -/
-theorem MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin [CompleteSpace E] {U : Set 𝕜}
+theorem MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin {U : Set 𝕜}
     (hf : MeromorphicOn f U) :
     { x | MeromorphicNFAt f x } ∈ Filter.codiscreteWithin U := by
   filter_upwards [hf.analyticAt_mem_codiscreteWithin] with _ ha
@@ -171,7 +171,7 @@ theorem MeromorphicNFAt.order_eq_zero_iff (hf : MeromorphicNFAt f x) :
 /-- **Local identity theorem**: two meromorphic functions in normal form agree in a
 neighborhood iff they agree in a pointed neighborhood.
 
-See `ContinuousAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd` for the analogous
+See `ContinuousAt.eventuallyEq_nhd_iff_eventuallyEq_nhdNE` for the analogous
 statement for continuous functions.
 -/
 theorem MeromorphicNFAt.eventuallyEq_nhdNE_iff_eventuallyEq_nhd {g : 𝕜 → E}
@@ -427,7 +427,7 @@ theorem MeromorphicNFOn.meromorphicOn (hf : MeromorphicNFOn f U) :
 If a function is meromorphic in normal form on `U`, then its divisor is
 non-negative iff it is analytic.
 -/
-theorem MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd [CompleteSpace E]
+theorem MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd
     (h₁f : MeromorphicNFOn f U) :
     0 ≤ MeromorphicOn.divisor f U ↔ AnalyticOnNhd 𝕜 f U := by
   constructor <;> intro h x
@@ -455,7 +455,7 @@ theorem AnalyticOnNhd.meromorphicNFOn (h₁f : AnalyticOnNhd 𝕜 f U) :
 If `f` is meromorphic in normal form on `U` and nowhere locally constant zero,
 then its zero set equals the support of the associated divisor.
 -/
-theorem MeromorphicNFOn.zero_set_eq_divisor_support [CompleteSpace E] (h₁f : MeromorphicNFOn f U)
+theorem MeromorphicNFOn.zero_set_eq_divisor_support (h₁f : MeromorphicNFOn f U)
     (h₂f : ∀ u : U, (h₁f u.2).meromorphicAt.order ≠ ⊤) :
     U ∩ f⁻¹' {0} = Function.support (MeromorphicOn.divisor f U) := by
   ext u
@@ -559,7 +559,7 @@ Conversion to normal form on `U` does not change values outside of `U`.
 Conversion to normal form on `U` changes the value only along a discrete subset
 of `U`.
 -/
-theorem toMeromorphicNFOn_eqOn_codiscrete [CompleteSpace E] (hf : MeromorphicOn f U) :
+theorem toMeromorphicNFOn_eqOn_codiscrete (hf : MeromorphicOn f U) :
     f =ᶠ[Filter.codiscreteWithin U] toMeromorphicNFOn f U := by
   have : U ∈ Filter.codiscreteWithin U := by
     simp [mem_codiscreteWithin.2]
@@ -570,17 +570,20 @@ theorem toMeromorphicNFOn_eqOn_codiscrete [CompleteSpace E] (hf : MeromorphicOn
 If `f` is meromorphic on `U` and `x ∈ U`, then `f` and its conversion to normal
 form on `U` agree in a punctured neighborhood of `x`.
 -/
-theorem MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdNE [CompleteSpace E]
+theorem MeromorphicOn.toMeromorphicNFOn_eq_self_on_nhdNE
     (hf : MeromorphicOn f U) (hx : x ∈ U) :
     toMeromorphicNFOn f U =ᶠ[𝓝[≠] x] f := by
-  filter_upwards [(hf x hx).eventually_analyticAt] with a ha
-  simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 ha.meromorphicNFAt).symm]
+  filter_upwards [hf.eventually_analyticAt_or_mem_compl hx] with a ha
+  rcases ha with ha | ha
+  · simp [toMeromorphicNFOn, hf, ← (toMeromorphicNFAt_eq_self.2 ha.meromorphicNFAt).symm]
+  · simp only [Set.mem_compl_iff] at ha
+    simp [toMeromorphicNFOn, ha, hf]
 
 /--
 If `f` is meromorphic on `U` and `x ∈ U`, then conversion to normal form at `x`
 and conversion to normal form on `U` agree in a neighborhood of `x`.
 -/
-theorem toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhd [CompleteSpace E] (hf : MeromorphicOn f U)
+theorem toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhd (hf : MeromorphicOn f U)
     (hx : x ∈ U) :
     toMeromorphicNFOn f U =ᶠ[𝓝 x] toMeromorphicNFAt f x := by
   apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE
@@ -591,7 +594,7 @@ theorem toMeromorphicNFOn_eq_toMeromorphicNFAt_on_nhd [CompleteSpace E] (hf : Me
 If `f` is meromorphic on `U` and `x ∈ U`, then conversion to normal form at `x`
 and conversion to normal form on `U` agree at `x`.
 -/
-theorem toMeromorphicNFOn_eq_toMeromorphicNFAt [CompleteSpace E] (hf : MeromorphicOn f U)
+theorem toMeromorphicNFOn_eq_toMeromorphicNFAt (hf : MeromorphicOn f U)
     (hx : x ∈ U) :
     toMeromorphicNFOn f U x = toMeromorphicNFAt f x x := by
   apply Filter.EventuallyEq.eq_of_nhds (g := toMeromorphicNFAt f x)
@@ -601,7 +604,7 @@ variable (f U) in
 /--
 After conversion to normal form on `U`, the function has normal form.
 -/
-theorem meromorphicNFOn_toMeromorphicNFOn [CompleteSpace E] :
+theorem meromorphicNFOn_toMeromorphicNFOn :
     MeromorphicNFOn (toMeromorphicNFOn f U) U := by
   by_cases hf : MeromorphicOn f U
   · intro z hz
@@ -614,7 +617,7 @@ theorem meromorphicNFOn_toMeromorphicNFOn [CompleteSpace E] :
 /--
 If `f` has normal form on `U`, then `f` equals `toMeromorphicNFOn f U`.
 -/
-@[simp] theorem toMeromorphicNFOn_eq_self [CompleteSpace E] :
+@[simp] theorem toMeromorphicNFOn_eq_self :
     toMeromorphicNFOn f U = f ↔ MeromorphicNFOn f U := by
   constructor <;> intro h
   · rw [h.symm]
@@ -628,16 +631,15 @@ If `f` has normal form on `U`, then `f` equals `toMeromorphicNFOn f U`.
 /--
 Conversion of normal form does not affect orders.
 -/
-@[simp] theorem order_toMeromorphicNFOn [CompleteSpace E] (hf : MeromorphicOn f U) (hx : x ∈ U) :
+@[simp] theorem order_toMeromorphicNFOn (hf : MeromorphicOn f U) (hx : x ∈ U) :
     ((meromorphicNFOn_toMeromorphicNFOn f U) hx).meromorphicAt.order = (hf x hx).order := by
   apply MeromorphicAt.order_congr
   exact hf.toMeromorphicNFOn_eq_self_on_nhdNE hx
 
 /--
 Conversion of normal form does not affect divisors.
 -/
-@[simp] theorem MeromorphicOn.divisor_of_toMeromorphicNFOn [CompleteSpace E]
-    (hf : MeromorphicOn f U) :
+@[simp] theorem MeromorphicOn.divisor_of_toMeromorphicNFOn (hf : MeromorphicOn f U) :
     divisor (toMeromorphicNFOn f U) U = divisor f U := by
   ext z
   by_cases hz : z ∈ U <;> simp [hf, (meromorphicNFOn_toMeromorphicNFOn f U).meromorphicOn, hz]