Update meromorphicOn.lean

Nevanlinna/analyticAt.lean

@@ -2,6 +2,20 @@ import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Analytic.Linear
 
+open Topology
+
+
+theorem AnalyticAt.order_neq_top_iff
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀) :
+  hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (hf.order.toNat) • g z := by
+  rw [← hf.order_eq_nat_iff]
+  constructor
+  · intro h₁f
+    exact Eq.symm (ENat.coe_toNat h₁f)
+  · intro h₁f
+    exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))
 
 
 theorem AnalyticAt.order_mul
@@ -105,10 +119,6 @@ theorem AnalyticAt.supp_order_toNat
   simp [hf.order_eq_zero_iff.2 h₁f]
 
 
-theorem ContinuousLinearEquiv.analyticAt
-  (ℓ : ℂ ≃L[ℂ] ℂ) (z₀ : ℂ) : AnalyticAt ℂ (⇑ℓ) z₀ := ℓ.toContinuousLinearMap.analyticAt z₀
-
-
 theorem eventually_nhds_comp_composition
   {f₁ f₂ ℓ : ℂ → ℂ}
   {z₀ : ℂ}
@@ -224,3 +234,77 @@ theorem AnalyticAt.order_comp_CLE
     rw [this]
 
     simp
+
+
+theorem AnalyticAt.localIdentity
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : AnalyticAt ℂ f z₀)
+  (hg : AnalyticAt ℂ g z₀) :
+  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
+  intro h
+  let Δ := f - g
+  have : AnalyticAt ℂ Δ z₀ := AnalyticAt.sub hf hg
+  have t₁ : Δ =ᶠ[𝓝[≠] z₀] 0 := by
+    exact Filter.eventuallyEq_iff_sub.mp h
+
+  have : Δ =ᶠ[𝓝 z₀] 0 := by
+    rcases (AnalyticAt.eventually_eq_zero_or_eventually_ne_zero this) with h | h
+    · exact h
+    · have := Filter.EventuallyEq.eventually t₁
+      let A := Filter.eventually_and.2 ⟨this, h⟩
+      let _ := Filter.Eventually.exists A
+      tauto
+  exact Filter.eventuallyEq_iff_sub.mpr this
+
+
+theorem AnalyticAt.mul₁
+  {f g : ℂ → ℂ}
+  {z : ℂ}
+  (hf : AnalyticAt ℂ f z)
+  (hg : AnalyticAt ℂ g z) :
+  AnalyticAt ℂ (f * g) z := by
+  rw [(by rfl : f * g = (fun x ↦ f x * g x))]
+  exact mul hf hg
+
+
+theorem analyticAt_finprod
+  {α : Type}
+  {f : α → ℂ → ℂ}
+  {z : ℂ}
+  (hf : ∀ a, AnalyticAt ℂ (f a) z) :
+  AnalyticAt ℂ (∏ᶠ a, f a) z := by
+  by_cases h₁f : (Function.mulSupport f).Finite
+  · rw [finprod_eq_prod f h₁f]
+    rw [Finset.prod_fn h₁f.toFinset f]
+    exact Finset.analyticAt_prod h₁f.toFinset (fun a _ ↦ hf a)
+  · rw [finprod_of_infinite_mulSupport h₁f]
+    exact analyticAt_const
+
+
+lemma AnalyticAt.zpow_nonneg
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  {n : ℤ}
+  (hf : AnalyticAt ℂ f z₀)
+  (hn : 0 ≤ n) :
+  AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
+  simp_rw [(Eq.symm (Int.toNat_of_nonneg hn) : n = OfNat.ofNat n.toNat), zpow_ofNat]
+  apply AnalyticAt.pow hf
+
+
+theorem AnalyticAt.zpow
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  {n : ℤ}
+  (h₁f : AnalyticAt ℂ f z₀)
+  (h₂f : f z₀ ≠ 0) :
+  AnalyticAt ℂ (fun x ↦ (f x) ^ n) z₀ := by
+  by_cases hn : 0 ≤ n
+  · exact zpow_nonneg h₁f hn
+  · rw [(Int.eq_neg_comm.mp rfl : n = - (- n))]
+    conv =>
+      arg 2
+      intro x
+      rw [zpow_neg]
+    exact AnalyticAt.inv (zpow_nonneg h₁f (by linarith)) (zpow_ne_zero (-n) h₂f)

Nevanlinna/analyticOnNhd_divisor.lean

@@ -0,0 +1,59 @@
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+noncomputable def AnalyticOnNhd.zeroDivisor
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : AnalyticOnNhd ℂ f U) :
+  Divisor U where
+
+  toFun := by
+    intro z
+    if hz : z ∈ U then
+      exact ((hf z hz).order.toNat : ℤ)
+    else
+      exact 0
+
+  supportInU := by
+    intro z hz
+    simp at hz
+    by_contra h₂z
+    simp [h₂z] at hz
+
+  locallyFiniteInU := by
+    intro z hz
+
+    apply eventually_nhdsWithin_iff.2
+    rw [eventually_nhds_iff]
+
+    rcases AnalyticAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
+    · rw [eventually_nhds_iff] at h
+      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
+      use N
+      constructor
+      · intro y h₁y _
+        by_cases h₃y : y ∈ U
+        · simp [h₃y]
+          right
+          rw [AnalyticAt.order_eq_top_iff (hf y h₃y)]
+          rw [eventually_nhds_iff]
+          use N
+        · simp [h₃y]
+      · tauto
+
+    · rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at h
+      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
+      use N
+      constructor
+      · intro y h₁y h₂y
+        by_cases h₃y : y ∈ U
+        · simp [h₃y]
+          left
+          rw [AnalyticAt.order_eq_zero_iff (hf y h₃y)]
+          exact h₁N y h₁y h₂y
+        · simp [h₃y]
+      · tauto

Nevanlinna/analyticOnNhd_zeroSet.lean

@@ -4,17 +4,17 @@ import Mathlib.Analysis.Complex.Basic
 import Nevanlinna.analyticAt
 
 
-noncomputable def AnalyticOn.order
-  {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOn ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
+noncomputable def AnalyticOnNhd.order
+  {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOnNhd ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order
 
 
-theorem AnalyticOn.order_eq_nat_iff
+theorem AnalyticOnNhd.order_eq_nat_iff
   {f : ℂ → ℂ}
   {U : Set ℂ}
   {z₀ : U}
-  (hf : AnalyticOn ℂ f U)
+  (hf : AnalyticOnNhd ℂ f U)
   (n : ℕ) :
-  hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
+  hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by
 
   constructor
   -- Direction →
@@ -91,31 +91,31 @@ theorem AnalyticOn.order_eq_nat_iff
   -- direction ←
   intro h
   obtain ⟨g, h₁g, h₂g, h₃g⟩ := h
-  dsimp [AnalyticOn.order]
+  dsimp [AnalyticOnNhd.order]
   rw [AnalyticAt.order_eq_nat_iff]
   use g
   exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩
 
 
-theorem AnalyticOn.support_of_order₁
+theorem AnalyticOnNhd.support_of_order₁
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
+  (hf : AnalyticOnNhd ℂ f U) :
   Function.support hf.order = U.restrict f⁻¹' {0} := by
   ext u
-  simp [AnalyticOn.order]
+  simp [AnalyticOnNhd.order]
   rw [not_iff_comm, (hf u u.2).order_eq_zero_iff]
 
 
-theorem AnalyticOn.eliminateZeros
+theorem AnalyticOnNhd.eliminateZeros
   {f : ℂ → ℂ}
   {U : Set ℂ}
   {A : Finset U}
-  (hf : AnalyticOn ℂ f U)
+  (hf : AnalyticOnNhd ℂ f U)
   (n : U → ℕ) :
-  (∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
+  (∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by
 
-  apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
+  apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z)
 
   -- case empty
   simp
@@ -146,7 +146,7 @@ theorem AnalyticOn.eliminateZeros
       intro b _
       apply AnalyticAt.pow
       apply AnalyticAt.sub
-      apply analyticAt_id ℂ
+      apply analyticAt_id
       exact analyticAt_const
 
     have h₂φ : h₁φ.order = (0 : ℕ) := by
@@ -173,7 +173,7 @@ theorem AnalyticOn.eliminateZeros
     rw [h₂φ]
     simp
 
-  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this
+  obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOnNhd.order_eq_nat_iff h₁g₀ (n b₀)).1 this
 
   use g₁
   constructor
@@ -203,7 +203,7 @@ theorem XX
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hU : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
   ∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by
 
@@ -221,7 +221,7 @@ theorem discreteZeros
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hU : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
   DiscreteTopology ((U.restrict f)⁻¹' {0}) := by
 
@@ -293,7 +293,7 @@ theorem finiteZeros
   {U : Set ℂ}
   (h₁U : IsPreconnected U)
   (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
   Set.Finite (U.restrict f⁻¹' {0}) := by
 
@@ -310,14 +310,14 @@ theorem finiteZeros
   exact discreteZeros h₁U h₁f h₂f
 
 
-theorem AnalyticOnCompact.eliminateZeros
+theorem AnalyticOnNhdCompact.eliminateZeros
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (h₁U : IsPreconnected U)
   (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by
+  ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by
 
   let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
 
@@ -325,13 +325,13 @@ theorem AnalyticOnCompact.eliminateZeros
 
   have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
     intro a _
-    dsimp [n, AnalyticOn.order]
+    dsimp [n, AnalyticOnNhd.order]
     rw [eq_comm]
     apply XX h₁U
     exact h₂f
 
 
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
   use g
   use A
 
@@ -357,14 +357,14 @@ theorem AnalyticOnCompact.eliminateZeros
     · exact inter
 
 
-theorem AnalyticOnCompact.eliminateZeros₂
+theorem AnalyticOnNhdCompact.eliminateZeros₂
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (h₁U : IsPreconnected U)
   (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by
+  ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by
 
   let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
 
@@ -372,12 +372,12 @@ theorem AnalyticOnCompact.eliminateZeros₂
 
   have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
     intro a _
-    dsimp [n, AnalyticOn.order]
+    dsimp [n, AnalyticOnNhd.order]
     rw [eq_comm]
     apply XX h₁U
     exact h₂f
 
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
   use g
 
   have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by
@@ -402,14 +402,14 @@ theorem AnalyticOnCompact.eliminateZeros₂
     · exact h₃g
 
 
-theorem AnalyticOnCompact.eliminateZeros₁
+theorem AnalyticOnNhdCompact.eliminateZeros₁
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (h₁U : IsPreconnected U)
   (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ u ∈ U, f u ≠ 0) :
-  ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by
+  ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by
 
   let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset
 
@@ -417,12 +417,12 @@ theorem AnalyticOnCompact.eliminateZeros₁
 
   have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by
     intro a _
-    dsimp [n, AnalyticOn.order]
+    dsimp [n, AnalyticOnNhd.order]
     rw [eq_comm]
     apply XX h₁U
     exact h₂f
 
-  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn
   use g
 
   have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by

Nevanlinna/bilinear.lean

@@ -28,7 +28,7 @@ orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`.
 
 -/
 
-
+open InnerProductSpace
 open TensorProduct
 
 
@@ -41,12 +41,11 @@ noncomputable def InnerProductSpace.canonicalCovariantTensor
   (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
   : E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i)
 
-
 theorem InnerProductSpace.canonicalCovariantTensorRepresentation
   (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
   [Fintype ι]
-  (v : OrthonormalBasis ι ℝ E)
-  : InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
+  (v : OrthonormalBasis ι ℝ E) :
+  InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
 
   let w := stdOrthonormalBasis ℝ E
   conv =>

Nevanlinna/cauchyRiemann.lean

@@ -31,7 +31,7 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
   have ContinuousLinearMap.comp_lineDeriv : ∀ w : ℂ, ∀ l : ℂ →L[ℝ] ℝ, lineDeriv ℝ (l ∘ f) z w = l ((fderiv ℝ f z) w) := by
     intro w l
     rw [DifferentiableAt.lineDeriv_eq_fderiv]
-    rw [fderiv.comp]
+    rw [fderiv_comp]
     simp
     fun_prop
     exact h.restrictScalars ℝ

Nevanlinna/divisor.lean

@@ -0,0 +1,93 @@
+import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
+import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
+import Nevanlinna.analyticAt
+import Nevanlinna.mathlibAddOn
+
+open Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+structure Divisor
+  (U : Set ℂ)
+  where
+  toFun : ℂ → ℤ
+  supportInU : toFun.support ⊆ U
+  locallyFiniteInU : ∀ x ∈ U, toFun =ᶠ[𝓝[≠] x] 0
+
+instance
+  (U : Set ℂ) :
+  CoeFun (Divisor U) (fun _ ↦ ℂ → ℤ) where
+  coe := Divisor.toFun
+
+attribute [coe] Divisor.toFun
+
+
+theorem Divisor.discreteSupport
+  {U : Set ℂ}
+  (hU : IsClosed U)
+  (D : Divisor U) :
+  DiscreteTopology D.toFun.support := by
+  apply discreteTopology_subtype_iff.mpr
+  intro x hx
+  apply inf_principal_eq_bot.mpr
+  by_cases h₁x : x ∈ U
+  · let A := D.locallyFiniteInU x h₁x
+    refine mem_nhdsWithin.mpr ?_
+    rw [eventuallyEq_nhdsWithin_iff] at A
+    obtain ⟨U, h₁U, h₂U, h₃U⟩ := eventually_nhds_iff.1 A
+    use U
+    constructor
+    · exact h₂U
+    · constructor
+      · exact h₃U
+      · intro y hy
+        let C := h₁U y hy.1 hy.2
+        tauto
+  · refine mem_nhdsWithin.mpr ?_
+    use Uᶜ
+    constructor
+    · simpa
+    · constructor
+      · tauto
+      · intro y _
+        let A := D.supportInU
+        simp at A
+        simp
+        exact False.elim (h₁x (A x hx))
+
+
+
+theorem Divisor.closedSupport
+  {U : Set ℂ}
+  (hU : IsClosed U)
+  (D : Divisor U) :
+  IsClosed D.toFun.support := by
+
+  rw [← isOpen_compl_iff]
+  rw [isOpen_iff_eventually]
+  intro x hx
+  by_cases h₁x : x ∈ U
+  · have A := D.locallyFiniteInU x h₁x
+    simp [A]
+    simp at hx
+    let B := Mnhds A hx
+    simpa
+  · rw [eventually_iff_exists_mem]
+    use Uᶜ
+    constructor
+    · exact IsClosed.compl_mem_nhds hU h₁x
+    · intro y hy
+      simp
+      exact Function.nmem_support.mp fun a => hy (D.supportInU a)
+
+
+theorem Divisor.finiteSupport
+  {U : Set ℂ}
+  (hU : IsCompact U)
+  (D : Divisor U) :
+  Set.Finite D.toFun.support := by
+  apply IsCompact.finite
+  · apply IsCompact.of_isClosed_subset hU (D.closedSupport hU.isClosed)
+    exact D.supportInU
+  · exact D.discreteSupport hU.isClosed

Nevanlinna/firstMain.lean

@@ -1,15 +1,19 @@
+import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.holomorphic_JensenFormula
 
 open Real
 
-variable {f : ℂ → ℂ}
-variable {h₁f : AnalyticOn ℂ f ⊤}
+variable (f : ℂ → ℂ)
+variable {h₁f : MeromorphicOn f ⊤}
 variable {h₂f : f 0 ≠ 0}
 
-noncomputable def unintegratedCounting : ℝ → ℕ := by
+
+
+noncomputable def Nevanlinna.n : ℝ → ℤ := by
   intro r
-  let A := h₁f.mono (by tauto : Metric.closedBall (0 : ℂ) r ⊆ ⊤)
-  exact ∑ᶠ z, (A.order z).toNat
+  have : MeromorphicAt f z := by
+    exact h₁f (sorryAx ℂ true) trivial
+  exact ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f z trivial).order
 
 noncomputable def integratedCounting : ℝ → ℝ := by
   intro r

Nevanlinna/holomorphic_JensenFormula.lean

@@ -1,6 +1,6 @@
 import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.Analytic.IsolatedZeros
-import Nevanlinna.analyticOn_zeroSet
+import Nevanlinna.analyticOnNhd_zeroSet
 import Nevanlinna.harmonicAt_examples
 import Nevanlinna.harmonicAt_meanValue
 import Nevanlinna.specialFunctions_CircleIntegral_affine
@@ -11,7 +11,7 @@ open Real
 
 theorem jensen_case_R_eq_one
   (f : ℂ → ℂ)
-  (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 1))
+  (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 1))
   (h₂f : f 0 ≠ 0) :
   log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
 
@@ -24,7 +24,7 @@ theorem jensen_case_R_eq_one
   have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
     use 0; simp; exact h₂f
 
-  obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f
+  obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnNhdCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f
 
   have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by
     intro z h₁z
@@ -259,9 +259,9 @@ theorem jensen_case_R_eq_one
   intro x ⟨h₁x, _⟩
   simp
 
-  dsimp [AnalyticOn.order] at h₁x
+  dsimp [AnalyticOnNhd.order] at h₁x
   simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x
-  exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h₁f x) h₁x
+  exact AnalyticAt.supp_order_toNat (AnalyticOnNhd.order.proof_1 h₁f x) h₁x
 
   --
   intro x hx
@@ -297,7 +297,7 @@ theorem jensen
   {R : ℝ}
   (hR : 0 < R)
   (f : ℂ → ℂ)
-  (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 R))
+  (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 R))
   (h₂f : f 0 ≠ 0) :
   log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
 
@@ -327,8 +327,8 @@ theorem jensen
 
   let F := f ∘ ℓ
 
-  have h₁F : AnalyticOn ℂ F (Metric.closedBall 0 1) := by
-    apply AnalyticOn.comp (t := Metric.closedBall 0 R)
+  have h₁F : AnalyticOnNhd ℂ F (Metric.closedBall 0 1) := by
+    apply AnalyticOnNhd.comp (t := Metric.closedBall 0 R)
     exact h₁f
     intro x _
     apply ℓ.toContinuousLinearMap.analyticAt x
@@ -430,7 +430,7 @@ theorem jensen
   left
   congr 1
 
-  dsimp [AnalyticOn.order]
+  dsimp [AnalyticOnNhd.order]
   rw [← AnalyticAt.order_comp_CLE ℓ]
 
   --

Nevanlinna/holomorphic_examples.lean

@@ -277,7 +277,7 @@ theorem harmonic_is_realOfHolomorphic
 
     intro x hx
     rw [fderivWithin_eq_fderiv, fderivWithin_eq_fderiv]
-    rw [fderiv.comp]
+    rw [fderiv_comp]
     simp
     apply ContinuousLinearMap.ext
     intro w

Nevanlinna/holomorphic_primitive.lean

@@ -666,7 +666,7 @@ theorem primitive_additivity'
       dsimp [ε']; simp
       have : |ε| = ε := by apply abs_of_pos h₁ε
       rw [this]
-      apply (inv_mul_lt_iff zero_lt_two).mpr
+      apply (inv_mul_lt_iff₀ zero_lt_two).mpr
       linarith
     have h₁ε' : 0 < ε' := by
       apply mul_pos _ h₁ε

Nevanlinna/holomorphic_zero.lean

@@ -3,7 +3,7 @@ import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Topology.ContinuousOn
 import Mathlib.Analysis.Analytic.IsolatedZeros
 import Nevanlinna.holomorphic
-import Nevanlinna.analyticOn_zeroSet
+import Nevanlinna.analyticOnNhd_zeroSet
 
 
 noncomputable def zeroDivisor
@@ -134,7 +134,7 @@ theorem topOnPreconnected
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hU : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ z ∈ U, f z ≠ 0) :
   ∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by
 
@@ -143,7 +143,7 @@ theorem topOnPreconnected
   obtain ⟨z', hz'⟩ := H
   rw [AnalyticAt.order_eq_top_iff] at hz'
   rw [← AnalyticAt.frequently_zero_iff_eventually_zero (h₁f z z')] at hz'
-  have A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
+  have A := AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz'
   tauto
 
 
@@ -151,7 +151,7 @@ theorem supportZeroSet
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hU : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ z ∈ U, f z ≠ 0) :
   U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by
 
@@ -180,7 +180,7 @@ theorem supportZeroSet
           refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a)
           exact topOnPreconnected hU h₁f h₂f h₁x
 
-
+/-
 theorem discreteZeros
   {f : ℂ → ℂ} :
   DiscreteTopology (Function.support (zeroDivisor f)) := by
@@ -254,13 +254,13 @@ theorem discreteZeros
   simp [this] at F
   ext
   rwa [sub_eq_zero] at F
-
+-/
 
 theorem zeroDivisor_finiteOnCompact
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (hU : IsPreconnected U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ z ∈ U, f z ≠ 0) -- not needed!
   (h₂U : IsCompact U) :
   Set.Finite (U ∩ Function.support (zeroDivisor f)) := by
@@ -289,7 +289,7 @@ noncomputable def zeroDivisorDegree
   {U : Set ℂ}
   (h₁U : IsPreconnected U) -- not needed!
   (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
   ℕ := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset.card
 
@@ -299,7 +299,7 @@ lemma zeroDivisorDegreeZero
   {U : Set ℂ}
   (h₁U : IsPreconnected U) -- not needed!
   (h₂U : IsCompact U)
-  (h₁f : AnalyticOn ℂ f U)
+  (h₁f : AnalyticOnNhd ℂ f U)
   (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed!
   0 = zeroDivisorDegree h₁U h₂U h₁f h₂f ↔ U ∩ (zeroDivisor f).support = ∅ := by
   sorry
@@ -309,9 +309,9 @@ lemma eliminatingZeros₀
   {U : Set ℂ}
   (h₁U : IsPreconnected U)
   (h₂U : IsCompact U) :
-  ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOn ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
+  ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOnNhd ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) →
   (n = zeroDivisorDegree h₁U h₂U h₁f h₂f) →
-  ∃ F : ℂ → ℂ, (AnalyticOn ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by
+  ∃ F : ℂ → ℂ, (AnalyticOnNhd ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by
 
   intro n
   induction' n with n ih
@@ -340,7 +340,7 @@ lemma eliminatingZeros₀
 
 
 
-  let A := AnalyticOn.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
+  let A := AnalyticOnNhd.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀)
   let B := zeroDivisor_eq_ord_AtZeroDivisorSupport hz₀.2
   let B := zeroDivisor_eq_ord_AtZeroDivisorSupport' hz₀.2
   rw [eq_comm] at B

Nevanlinna/mathlibAddOn.lean

@@ -1,5 +1,7 @@
+import Mathlib.Analysis.Analytic.Meromorphic
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Add
+import Nevanlinna.analyticAt
 
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
@@ -33,3 +35,42 @@ theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) :
   have : c • f = fun x ↦ c • f x := rfl
   rw [this]
   exact ContDiff.const_smul c hf
+
+
+
+open Topology Filter
+
+lemma Mnhds
+  {α : Type}
+  {f g : ℂ → α}
+  {z₀ : ℂ}
+  (h₁ : f =ᶠ[𝓝[≠] z₀] g)
+  (h₂ : f z₀ = g z₀) :
+  f =ᶠ[𝓝 z₀] g := by
+  apply eventually_nhds_iff.2
+  obtain ⟨t, h₁t, h₂t⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₁)
+  use t
+  constructor
+  · intro y hy
+    by_cases h₂y : y ∈ ({z₀}ᶜ : Set ℂ)
+    · exact h₁t y hy h₂y
+    · simp at h₂y
+      rwa [h₂y]
+  · exact h₂t
+
+-- unclear where this should go
+
+lemma WithTopCoe
+  {n : WithTop ℕ} :
+  WithTop.map (Nat.cast : ℕ → ℤ) n = 0 → n = 0 := by
+  rcases n with h|h
+  · intro h
+    contradiction
+  · intro h₁
+    simp only [WithTop.map, Option.map] at h₁
+    have : (h : ℤ) = 0 := by
+      exact WithTop.coe_eq_zero.mp h₁
+    have : h = 0 := by
+      exact Int.ofNat_eq_zero.mp this
+    rw [this]
+    rfl

Nevanlinna/meromorphicAt.lean

@@ -0,0 +1,147 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+theorem meromorphicAt_congr
+  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
+  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
+  (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
+  ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩
+
+
+theorem meromorphicAt_congr'
+  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
+  {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+  {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜}
+  (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x :=
+  meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds)
+
+
+theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  (∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = 0) ∨ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0 := by
+
+  obtain ⟨n, h⟩ := hf
+  let A := h.eventually_eq_zero_or_eventually_ne_zero
+
+  rw [eventually_nhdsWithin_iff]
+  rw [eventually_nhds_iff]
+  rcases A with h₁|h₂
+  · rw [eventually_nhds_iff] at h₁
+    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₁
+    left
+    use N
+    constructor
+    · intro y h₁y h₂y
+      let A := h₁N y h₁y
+      simp at A
+      rcases A with h₃|h₄
+      · let B := h₃.1
+        simp at h₂y
+        let C := sub_eq_zero.1 B
+        tauto
+      · assumption
+    · constructor
+      · exact h₂N
+      · exact h₃N
+  · right
+    rw [eventually_nhdsWithin_iff]
+    rw [eventually_nhds_iff]
+    rw [eventually_nhdsWithin_iff] at h₂
+    rw [eventually_nhds_iff] at h₂
+    obtain ⟨N, h₁N, h₂N, h₃N⟩ := h₂
+    use N
+    constructor
+    · intro y h₁y h₂y
+      by_contra h
+      let A := h₁N y h₁y h₂y
+      rw [h] at A
+      simp at A
+    · constructor
+      · exact h₂N
+      · exact h₃N
+
+
+theorem MeromorphicAt.order_congr
+  {f₁ f₂ : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf₁ : MeromorphicAt f₁ z₀)
+  (h : f₁ =ᶠ[𝓝[≠] z₀] f₂):
+  hf₁.order = (hf₁.congr h).order := by
+  by_cases hord : hf₁.order = ⊤
+  · rw [hord, eq_comm]
+    rw [hf₁.order_eq_top_iff] at hord
+    rw [(hf₁.congr h).order_eq_top_iff]
+    exact EventuallyEq.rw hord (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
+  · obtain ⟨n, hn : hf₁.order = n⟩ := Option.ne_none_iff_exists'.mp hord
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := (hf₁.order_eq_int_iff n).1 hn
+    rw [hn, eq_comm, (hf₁.congr h).order_eq_int_iff]
+    use g
+    constructor
+    · assumption
+    · constructor
+      · assumption
+      · exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h))
+
+
+theorem MeromorphicAt.order_mul
+  {f₁ f₂ : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf₁ : MeromorphicAt f₁ z₀)
+  (hf₂ : MeromorphicAt f₂ z₀) :
+  (hf₁.mul hf₂).order = hf₁.order + hf₂.order := by
+  by_cases h₂f₁ : hf₁.order = ⊤
+  · simp [h₂f₁]
+    rw [hf₁.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₁
+    rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
+    obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁
+    use t
+    constructor
+    · intro y h₁y h₂y
+      simp; left
+      rw [h₁t y h₁y h₂y]
+    · exact ⟨h₂t, h₃t⟩
+  · by_cases h₂f₂ : hf₂.order = ⊤
+    · simp [h₂f₂]
+      rw [hf₂.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₂
+      rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff]
+      obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂
+      use t
+      constructor
+      · intro y h₁y h₂y
+        simp; right
+        rw [h₁t y h₁y h₂y]
+      · exact ⟨h₂t, h₃t⟩
+    · have h₃f₁ := Eq.symm (WithTop.coe_untop hf₁.order h₂f₁)
+      have h₃f₂ := Eq.symm (WithTop.coe_untop hf₂.order h₂f₂)
+      obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (hf₁.order_eq_int_iff (hf₁.order.untop h₂f₁)).1 h₃f₁
+      obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (hf₂.order_eq_int_iff (hf₂.order.untop h₂f₂)).1 h₃f₂
+      rw [h₃f₁, h₃f₂, ← WithTop.coe_add]
+      rw [MeromorphicAt.order_eq_int_iff]
+      use g₁ * g₂
+      constructor
+      · exact AnalyticAt.mul h₁g₁ h₁g₂
+      · constructor
+        · simp; tauto
+        · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₁)
+          obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₂)
+          rw [eventually_nhdsWithin_iff, eventually_nhds_iff]
+          use t₁ ∩ t₂
+          constructor
+          · intro y h₁y h₂y
+            simp
+            rw [h₁t₁ y h₁y.1 h₂y, h₁t₂ y h₁y.2 h₂y]
+            simp
+            rw [zpow_add' (by left; exact sub_ne_zero_of_ne h₂y)]
+            group
+          · constructor
+            · exact IsOpen.inter h₂t₁ h₂t₂
+            · exact Set.mem_inter h₃t₁ h₃t₂

Nevanlinna/meromorphicOn.lean

@@ -0,0 +1,54 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+import Nevanlinna.meromorphicAt
+import Nevanlinna.meromorphicOn_divisor
+import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.mathlibAddOn
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+theorem MeromorphicOn.open_of_order_eq_top
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : MeromorphicOn f U) :
+  IsOpen { u : U | (h₁f u.1 u.2).order = ⊤ } := by
+
+  apply isOpen_iff_forall_mem_open.mpr
+  intro z hz
+  simp at hz
+  rw [MeromorphicAt.order_eq_top_iff] at hz
+  rw [eventually_nhdsWithin_iff] at hz
+  rw [eventually_nhds_iff] at hz
+  obtain ⟨t', h₁t', h₂t', h₃t'⟩ := hz
+
+  let t : Set U := Subtype.val ⁻¹' t'
+  use t
+  constructor
+  · intro w hw
+    simp
+    sorry
+  · constructor
+    · exact isOpen_induced h₂t'
+    · exact h₃t'
+
+theorem MeromorphicOn.order_ne_top
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsConnected U)
+  (h₁f : MeromorphicOn f U) :
+  (∃ z₀ : U, (h₁f z₀.1 z₀.2).order = ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order = ⊤) := by
+
+  constructor
+  · intro h
+    obtain ⟨h₁z₀, h₂z₀⟩ := h
+    intro hz
+
+
+    sorry
+
+  · intro h
+    obtain ⟨w, hw⟩ := h₁U.nonempty
+    use ⟨w, hw⟩
+    exact h ⟨w, hw⟩

Nevanlinna/meromorphicOn_divisor.lean

@@ -0,0 +1,76 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+import Nevanlinna.meromorphicAt
+
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+noncomputable def MeromorphicOn.divisor
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  Divisor U where
+
+  toFun := by
+    intro z
+    if hz : z ∈ U then
+      exact ((hf z hz).order.untop' 0 : ℤ)
+    else
+      exact 0
+
+  supportInU := by
+    intro z hz
+    simp at hz
+    by_contra h₂z
+    simp [h₂z] at hz
+
+  locallyFiniteInU := by
+    intro z hz
+
+    apply eventually_nhdsWithin_iff.2
+    rw [eventually_nhds_iff]
+
+    rcases MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero (hf z hz) with h|h
+    · rw [eventually_nhdsWithin_iff] at h
+      rw [eventually_nhds_iff] at h
+      obtain ⟨N, h₁N, h₂N, h₃N⟩ := h
+      use N
+      constructor
+      · intro y h₁y h₂y
+        by_cases h₃y : y ∈ U
+        · simp [h₃y]
+          right
+          rw [MeromorphicAt.order_eq_top_iff (hf y h₃y)]
+          rw [eventually_nhdsWithin_iff]
+          rw [eventually_nhds_iff]
+          use N ∩ {z}ᶜ
+          constructor
+          · intro x h₁x _
+            exact h₁N x h₁x.1 h₁x.2
+          · constructor
+            · exact IsOpen.inter h₂N isOpen_compl_singleton
+            · exact Set.mem_inter h₁y h₂y
+        · simp [h₃y]
+      · tauto
+
+    · let A := (hf z hz).eventually_analyticAt
+      let B := Filter.eventually_and.2 ⟨h, A⟩
+      rw [eventually_nhdsWithin_iff, eventually_nhds_iff] at B
+      obtain ⟨N, h₁N, h₂N, h₃N⟩ := B
+      use N
+      constructor
+      · intro y h₁y h₂y
+        by_cases h₃y : y ∈ U
+        · simp [h₃y]
+          left
+          rw [(h₁N y h₁y h₂y).2.meromorphicAt_order]
+          let D := (h₁N y h₁y h₂y).2.order_eq_zero_iff.2
+          let C := (h₁N y h₁y h₂y).1
+          let E := D C
+          rw [E]
+          simp
+        · simp [h₃y]
+      · tauto

Nevanlinna/partialDeriv.lean

@@ -202,14 +202,14 @@ theorem partialDeriv_compContLin
     left
     intro w
     left
-    rw [fderiv.comp w (ContinuousLinearMap.differentiableAt l) (h w)]
+    rw [fderiv_comp w (ContinuousLinearMap.differentiableAt l) (h w)]
   simp
   rfl
 
 
 theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x : E} (h : DifferentiableAt 𝕜 f x) : (partialDeriv 𝕜 v (l ∘ f)) x = (l ∘ partialDeriv 𝕜 v f) x:= by
   unfold partialDeriv
-  rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
+  rw [fderiv_comp x (ContinuousLinearMap.differentiableAt l) h]
   simp
 
 

Nevanlinna/specialFunctions_Integral_log_sin.lean

@@ -24,7 +24,7 @@ lemma logsinBound : ∀ x ∈ (Set.Icc 0 1), ‖(log ∘ sin) x‖ ≤ ‖log ((
     exact zero_lt_two
     apply (Set.mem_Icc.1 hx).1
     simp
-    apply mul_le_one
+    apply mul_le_one₀
     rw [div_le_one pi_pos]
     exact two_le_pi
     exact (Set.mem_Icc.1 hx).1

Nevanlinna/stronglyMeromorphicAt.lean

@@ -0,0 +1,437 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Mathlib.Algebra.Order.AddGroupWithTop
+import Nevanlinna.analyticAt
+import Nevanlinna.mathlibAddOn
+import Nevanlinna.meromorphicAt
+
+
+open Topology
+
+
+/- Strongly MeromorphicAt -/
+def StronglyMeromorphicAt
+  (f : ℂ → ℂ)
+  (z₀ : ℂ) :=
+  (∀ᶠ (z : ℂ) in nhds z₀, f z = 0) ∨ (∃ (n : ℤ), ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ n • g z))
+
+
+
+/- Strongly MeromorphicAt is Meromorphic -/
+theorem StronglyMeromorphicAt.meromorphicAt
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : StronglyMeromorphicAt f z₀) :
+  MeromorphicAt f z₀ := by
+  rcases hf with h|h
+  · use 0; simp
+    rw [analyticAt_congr h]
+    exact analyticAt_const
+  · obtain ⟨n, g, h₁g, _, h₃g⟩ := h
+    rw [meromorphicAt_congr' h₃g]
+    apply MeromorphicAt.smul
+    apply MeromorphicAt.zpow
+    apply MeromorphicAt.sub
+    apply MeromorphicAt.id
+    apply MeromorphicAt.const
+    exact AnalyticAt.meromorphicAt h₁g
+
+
+/- Strongly MeromorphicAt of non-negative order is analytic -/
+theorem StronglyMeromorphicAt.analytic
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁f : StronglyMeromorphicAt f z₀)
+  (h₂f : 0 ≤ h₁f.meromorphicAt.order):
+  AnalyticAt ℂ f z₀ := by
+  let h₁f' := h₁f
+  rcases h₁f' with h|h
+  · rw [analyticAt_congr h]
+    exact analyticAt_const
+  · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h
+    rw [analyticAt_congr h₃g]
+
+    have : h₁f.meromorphicAt.order = n := by
+      rw [MeromorphicAt.order_eq_int_iff]
+      use g
+      constructor
+      · exact h₁g
+      · constructor
+        · exact h₂g
+        · exact Filter.EventuallyEq.filter_mono h₃g nhdsWithin_le_nhds
+    rw [this] at h₂f
+    apply AnalyticAt.smul
+    nth_rw 1 [← Int.toNat_of_nonneg (WithTop.coe_nonneg.mp h₂f)]
+    apply AnalyticAt.pow
+    apply AnalyticAt.sub
+    apply analyticAt_id -- Warning: want apply AnalyticAt.id
+    apply analyticAt_const -- Warning: want AnalyticAt.const
+    exact h₁g
+
+
+/- Analytic functions are strongly meromorphic -/
+theorem AnalyticAt.stronglyMeromorphicAt
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁f : AnalyticAt ℂ f z₀) :
+  StronglyMeromorphicAt f z₀ := by
+  by_cases h₂f : h₁f.order = ⊤
+  · rw [AnalyticAt.order_eq_top_iff] at h₂f
+    tauto
+  · have : h₁f.order ≠ ⊤ := h₂f
+    rw [← ENat.coe_toNat_eq_self] at this
+    rw [eq_comm, AnalyticAt.order_eq_nat_iff] at this
+    right
+    use h₁f.order.toNat
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
+    use g
+    tauto
+
+
+/- Strong meromorphic depends only on germ -/
+theorem stronglyMeromorphicAt_congr
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hfg : f =ᶠ[𝓝 z₀] g) :
+  StronglyMeromorphicAt f z₀ ↔ StronglyMeromorphicAt g z₀ := by
+  unfold StronglyMeromorphicAt
+  constructor
+  · intro h
+    rcases h with h|h
+    · left
+      exact Filter.EventuallyEq.rw h (fun x => Eq (g x)) (id (Filter.EventuallyEq.symm hfg))
+    · obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
+      right
+      use n
+      use h
+      constructor
+      · assumption
+      · constructor
+        · assumption
+        · apply Filter.EventuallyEq.trans hfg.symm
+          assumption
+  · intro h
+    rcases h with h|h
+    · left
+      exact Filter.EventuallyEq.rw h (fun x => Eq (f x)) hfg
+    · obtain ⟨n, h, h₁h, h₂h, h₃h⟩ := h
+      right
+      use n
+      use h
+      constructor
+      · assumption
+      · constructor
+        · assumption
+        · apply Filter.EventuallyEq.trans hfg
+          assumption
+
+
+theorem StronglyMeromorphicAt.order_eq_zero_iff
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : StronglyMeromorphicAt f z₀) :
+  hf.meromorphicAt.order = 0 ↔ f z₀ ≠ 0 := by
+  constructor
+  · intro h₁f
+    let A := hf.analytic (le_of_eq (id (Eq.symm h₁f)))
+    apply A.order_eq_zero_iff.1
+    let B := A.meromorphicAt_order
+    rw [h₁f] at B
+    apply WithTopCoe
+    rw [eq_comm]
+    exact B
+  · intro h
+    have hf' := hf
+    rcases hf with h₁|h₁
+    · have : f z₀ = 0 := by
+        apply Filter.EventuallyEq.eq_of_nhds h₁
+      tauto
+    · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁
+      have : n = 0 := by
+        by_contra hContra
+        let A := Filter.EventuallyEq.eq_of_nhds h₃g
+        have : (0 : ℂ) ^ n = 0 := by
+          exact zero_zpow n hContra
+        simp at A
+        simp_rw [this] at A
+        simp at A
+        tauto
+      rw [this] at h₃g
+      simp at h₃g
+
+      have : hf'.meromorphicAt.order = 0 := by
+        apply (hf'.meromorphicAt.order_eq_int_iff 0).2
+        use g
+        constructor
+        · assumption
+        · constructor
+          · assumption
+          · simp
+            apply Filter.EventuallyEq.filter_mono h₃g
+            exact nhdsWithin_le_nhds
+      exact this
+
+
+theorem StronglyMeromorphicAt.localIdentity
+  {f g : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : StronglyMeromorphicAt f z₀)
+  (hg : StronglyMeromorphicAt g z₀) :
+  f =ᶠ[𝓝[≠] z₀] g → f =ᶠ[𝓝 z₀] g := by
+
+  intro h
+
+  have t₀ : hf.meromorphicAt.order = hg.meromorphicAt.order := by
+    exact hf.meromorphicAt.order_congr h
+
+  by_cases cs : hf.meromorphicAt.order = 0
+  · rw [cs] at t₀
+    have h₁f := hf.analytic (le_of_eq (id (Eq.symm cs)))
+    have h₁g := hg.analytic (le_of_eq t₀)
+    exact h₁f.localIdentity h₁g h
+  · apply Mnhds h
+    let A := cs
+    rw [hf.order_eq_zero_iff] at A
+    simp at A
+    let B := cs
+    rw [t₀] at B
+    rw [hg.order_eq_zero_iff] at B
+    simp at B
+    rw [A, B]
+
+
+
+/- Make strongly MeromorphicAt -/
+noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  ℂ → ℂ := by
+  intro z
+  by_cases z = z₀
+  · by_cases h₁f : hf.order = (0 : ℤ)
+    · rw [hf.order_eq_int_iff] at h₁f
+      exact (Classical.choose h₁f) z₀
+    · exact 0
+  · exact f z
+
+
+lemma m₁
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  ∀ z ≠ z₀, f z = hf.makeStronglyMeromorphicAt z := by
+  intro z hz
+  unfold MeromorphicAt.makeStronglyMeromorphicAt
+  simp [hz]
+
+
+lemma m₂
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  f =ᶠ[𝓝[≠] z₀] hf.makeStronglyMeromorphicAt := by
+  apply eventually_nhdsWithin_of_forall
+  exact fun x a => m₁ hf x a
+
+
+theorem StronglyMeromorphicAt_of_makeStronglyMeromorphic
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicAt f z₀) :
+  StronglyMeromorphicAt hf.makeStronglyMeromorphicAt z₀ := by
+
+  by_cases h₂f : hf.order = ⊤
+  · have : hf.makeStronglyMeromorphicAt =ᶠ[𝓝 z₀] 0 := by
+      apply Mnhds
+      · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
+        exact (MeromorphicAt.order_eq_top_iff hf).1 h₂f
+      · unfold MeromorphicAt.makeStronglyMeromorphicAt
+        simp [h₂f]
+
+    apply AnalyticAt.stronglyMeromorphicAt
+    rw [analyticAt_congr this]
+    apply analyticAt_const
+  · let n := hf.order.untop h₂f
+    have : hf.order = n := by
+      exact Eq.symm (WithTop.coe_untop hf.order h₂f)
+    rw [hf.order_eq_int_iff] at this
+    obtain ⟨g, h₁g, h₂g, h₃g⟩ := this
+    right
+    use n
+    use g
+    constructor
+    · assumption
+    · constructor
+      · assumption
+      · apply Mnhds
+        · apply Filter.EventuallyEq.trans (Filter.EventuallyEq.symm (m₂ hf))
+          exact h₃g
+        · unfold MeromorphicAt.makeStronglyMeromorphicAt
+          simp
+          by_cases h₃f : hf.order = (0 : ℤ)
+          · let h₄f := (hf.order_eq_int_iff 0).1 h₃f
+            simp [h₃f]
+            obtain ⟨h₁G, h₂G, h₃G⟩  := Classical.choose_spec h₄f
+            simp at h₃G
+            have hn : n = 0 := Eq.symm ((fun {α} {a} {b} h => (WithTop.eq_untop_iff h).mpr) h₂f (id (Eq.symm h₃f)))
+            rw [hn]
+            rw [hn] at h₃g; simp at h₃g
+            simp
+            have : g =ᶠ[𝓝 z₀] (Classical.choose h₄f) := by
+              apply h₁g.localIdentity h₁G
+              exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₃g) h₃G
+            rw [Filter.EventuallyEq.eq_of_nhds this]
+          · have : hf.order ≠ 0 := h₃f
+            simp [this]
+            left
+            apply zero_zpow n
+            dsimp [n]
+            rwa [WithTop.untop_eq_iff h₂f]
+
+
+theorem makeStronglyMeromorphic_id
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (hf : StronglyMeromorphicAt f z₀) :
+  f = hf.meromorphicAt.makeStronglyMeromorphicAt := by
+
+  funext z
+  by_cases hz : z = z₀
+  · rw [hz]
+    unfold MeromorphicAt.makeStronglyMeromorphicAt
+    simp
+    have h₀f := hf
+    rcases hf with h₁f|h₁f
+    · have A : f =ᶠ[𝓝[≠] z₀] 0 := by
+        apply Filter.EventuallyEq.filter_mono h₁f
+        exact nhdsWithin_le_nhds
+      let B := (MeromorphicAt.order_eq_top_iff h₀f.meromorphicAt).2 A
+      simp [B]
+      exact Filter.EventuallyEq.eq_of_nhds h₁f
+    · obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁f
+      rw [Filter.EventuallyEq.eq_of_nhds h₃g]
+      have : h₀f.meromorphicAt.order = n := by
+        rw [MeromorphicAt.order_eq_int_iff (StronglyMeromorphicAt.meromorphicAt h₀f) n]
+        use g
+        constructor
+        · assumption
+        · constructor
+          · assumption
+          · exact eventually_nhdsWithin_of_eventually_nhds h₃g
+      by_cases h₃f : h₀f.meromorphicAt.order = 0
+      · simp [h₃f]
+        have hn : n = (0 : ℤ) := by
+          rw [h₃f] at this
+          exact WithTop.coe_eq_zero.mp (id (Eq.symm this))
+        simp_rw [hn]
+        simp
+        let t₀ : h₀f.meromorphicAt.order = (0 : ℤ) := by
+          exact h₃f
+        let A := (h₀f.meromorphicAt.order_eq_int_iff 0).1 t₀
+        have : g =ᶠ[𝓝 z₀] (Classical.choose A) := by
+          obtain ⟨h₀, h₁, h₂⟩  := Classical.choose_spec A
+          apply h₁g.localIdentity h₀
+          rw [hn] at h₃g
+          simp at h₃g
+          simp at h₂
+          have h₄g : f =ᶠ[𝓝[≠] z₀] g := by
+            apply Filter.EventuallyEq.filter_mono h₃g
+            exact nhdsWithin_le_nhds
+          exact Filter.EventuallyEq.trans (Filter.EventuallyEq.symm h₄g) h₂
+        exact Filter.EventuallyEq.eq_of_nhds this
+      · simp [h₃f]
+        left
+        apply zero_zpow n
+        by_contra hn
+        rw [hn] at this
+        tauto
+  · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz
+
+
+theorem StronglyMeromorphicAt.eliminate
+  {f : ℂ → ℂ}
+  {z₀ : ℂ}
+  (h₁f : StronglyMeromorphicAt f z₀)
+  (h₂f : h₁f.meromorphicAt.order ≠ ⊤) :
+  ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀)
+    ∧ (g z₀ ≠ 0)
+    ∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by
+
+  let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f
+  let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)
+  have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by
+    apply MeromorphicAt.zpow
+    apply AnalyticAt.meromorphicAt
+    apply AnalyticAt.sub
+    apply analyticAt_id
+    exact analyticAt_const
+  have h₂g₁₁ : h₁g₁₁.order = - h₁f.meromorphicAt.order.untop h₂f := by
+    rw [← WithTop.LinearOrderedAddCommGroup.coe_neg]
+    rw [h₁g₁₁.order_eq_int_iff]
+    use 1
+    constructor
+    · exact analyticAt_const
+    · constructor
+      · simp
+      · apply eventually_nhdsWithin_of_forall
+        simp [g₁₁]
+  have h₁g₁ : MeromorphicAt g₁ z₀ := h₁g₁₁.mul h₁f.meromorphicAt
+  have h₂g₁ : h₁g₁.order = 0 := by
+    rw [h₁g₁₁.order_mul h₁f.meromorphicAt]
+    rw [h₂g₁₁]
+    simp
+    rw [add_comm]
+    rw [LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top h₂f]
+  let g := h₁g₁.makeStronglyMeromorphicAt
+  use g
+  have h₁g : StronglyMeromorphicAt g z₀ := by
+    exact StronglyMeromorphicAt_of_makeStronglyMeromorphic h₁g₁
+  have h₂g : h₁g.meromorphicAt.order = 0 := by
+    rw [← h₁g₁.order_congr (m₂ h₁g₁)]
+    exact h₂g₁
+  constructor
+  · apply analytic
+    · rw [h₂g]
+    · exact h₁g
+  · constructor
+    · rwa [← h₁g.order_eq_zero_iff]
+    · funext z
+      by_cases hz : z = z₀
+      · by_cases hOrd : h₁f.meromorphicAt.order.untop h₂f = 0
+        · simp [hOrd]
+          have : StronglyMeromorphicAt g₁ z₀ := by
+            unfold g₁
+            simp [hOrd]
+            have : (fun z => 1) * f = f := by
+              funext z
+              simp
+            rwa [this]
+          rw [hz]
+          unfold g
+          let A := makeStronglyMeromorphic_id this
+          rw [← A]
+          unfold g₁
+          rw [hOrd]
+          simp
+        · have : h₁f.meromorphicAt.order ≠ 0 := by
+            by_contra hC
+            simp_rw [hC] at hOrd
+            tauto
+          let A := h₁f.order_eq_zero_iff.not.1 this
+          simp at A
+          rw [hz, A]
+          simp
+          left
+          rw [zpow_eq_zero_iff]
+          assumption
+      · simp
+        have : g z = g₁ z := by
+          exact Eq.symm (m₁ h₁g₁ z hz)
+        rw [this]
+        unfold g₁
+        simp [hz]
+        rw [← mul_assoc]
+        rw [mul_inv_cancel₀]
+        simp
+        apply zpow_ne_zero
+        exact sub_ne_zero_of_ne hz

Nevanlinna/stronglyMeromorphicOn.lean

@@ -0,0 +1,112 @@
+import Nevanlinna.stronglyMeromorphicAt
+
+
+open Topology
+
+
+/- Strongly MeromorphicOn -/
+def StronglyMeromorphicOn
+  (f : ℂ → ℂ)
+  (U : Set ℂ) :=
+  ∀ z ∈ U, StronglyMeromorphicAt f z
+
+
+/- Strongly MeromorphicAt is Meromorphic -/
+theorem StronglyMeromorphicOn.meromorphicOn
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : StronglyMeromorphicOn f U) :
+  MeromorphicOn f U := by
+  intro z hz
+  exact StronglyMeromorphicAt.meromorphicAt (hf z hz)
+
+
+/- Strongly MeromorphicOn of non-negative order is analytic -/
+theorem StronglyMeromorphicOn.analytic
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : StronglyMeromorphicOn f U)
+  (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ (h₁f x hx).meromorphicAt.order):
+  ∀ z ∈ U, AnalyticAt ℂ f z := by
+  intro z hz
+  apply StronglyMeromorphicAt.analytic
+  exact h₂f z hz
+  exact h₁f z hz
+
+
+/- Analytic functions are strongly meromorphic -/
+theorem AnalyticOn.stronglyMeromorphicOn
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : AnalyticOnNhd ℂ f U) :
+  StronglyMeromorphicOn f U := by
+  intro z hz
+  apply AnalyticAt.stronglyMeromorphicAt
+  exact h₁f z hz
+
+
+/- Make strongly MeromorphicAt -/
+noncomputable def MeromorphicOn.makeStronglyMeromorphicOn
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  ℂ → ℂ := by
+  intro z
+  by_cases hz : z ∈ U
+  · exact (hf z hz).makeStronglyMeromorphicAt z
+  · exact f z
+
+
+theorem makeStronglyMeromorphicOn_changeDiscrete
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicOn f U)
+  (hz₀ : z₀ ∈ U) :
+  hf.makeStronglyMeromorphicOn =ᶠ[𝓝[≠] z₀] f := by
+  apply Filter.eventually_iff_exists_mem.2
+  let A := (hf z₀ hz₀).eventually_analyticAt
+  obtain ⟨V, h₁V, h₂V⟩  := Filter.eventually_iff_exists_mem.1 A
+  use V
+  constructor
+  · assumption
+  · intro v hv
+    unfold MeromorphicOn.makeStronglyMeromorphicOn
+    by_cases h₂v : v ∈ U
+    · simp [h₂v]
+      rw [← makeStronglyMeromorphic_id]
+      exact AnalyticAt.stronglyMeromorphicAt (h₂V v hv)
+    · simp [h₂v]
+
+
+theorem StronglyMeromorphicOn_of_makeStronglyMeromorphic
+  {f : ℂ → ℂ}
+  (hf : MeromorphicOn f U) :
+  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
+
+  sorry
+
+
+theorem makeStronglyMeromorphicOn_changeDiscrete'
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  {z₀ : ℂ}
+  (hf : MeromorphicOn f U)
+  (hz₀ : z₀ ∈ U) :
+  hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
+  apply Mnhds
+  let A := makeStronglyMeromorphicOn_changeDiscrete hf hz₀
+  apply Filter.EventuallyEq.trans A
+  exact m₂ (hf z₀ hz₀)
+  unfold MeromorphicOn.makeStronglyMeromorphicOn
+  simp [hz₀]
+
+
+theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
+  intro z₀ hz₀
+  rw [stronglyMeromorphicAt_congr (makeStronglyMeromorphicOn_changeDiscrete' hf hz₀)]
+  exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z₀ hz₀)

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -0,0 +1,86 @@
+import Mathlib.Analysis.Analytic.Meromorphic
+import Nevanlinna.analyticAt
+import Nevanlinna.divisor
+import Nevanlinna.meromorphicAt
+import Nevanlinna.meromorphicOn_divisor
+import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.mathlibAddOn
+
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+
+theorem MeromorphicOn.decompose
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsConnected U)
+  (h₂U : IsCompact U)
+  (h₁f : MeromorphicOn f U)
+  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
+  ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U)
+    ∧ (∀ z ∈ U, g z ≠ 0)
+    ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn ((∏ᶠ p, fun z ↦ (z - p) ^ (h₁f.divisor p)) * g) U) := by
+
+  let g₁ : ℂ → ℂ := f * (fun z ↦ ∏ᶠ p, (z - p) ^ (h₁f.divisor p))
+  have h₁g₁ : MeromorphicOn g₁ U := by
+    sorry
+  let g := h₁g₁.makeStronglyMeromorphicOn
+  have h₁g : MeromorphicOn g U := by
+    sorry
+  have h₂g : ∀ z : U, (h₁g z.1 z.2).order = 0 := by
+    sorry
+  have h₃g : StronglyMeromorphicOn g U := by
+    sorry
+  have h₄g : AnalyticOnNhd ℂ g U := by
+    intro z hz
+    apply StronglyMeromorphicAt.analytic (h₃g z hz)
+    rw [h₂g ⟨z, hz⟩]
+  use g
+  constructor
+  · exact h₄g
+  · constructor
+    · intro z hz
+      rw [← (h₄g z hz).order_eq_zero_iff]
+      have A := (h₄g z hz).meromorphicAt_order
+      rw [h₂g ⟨z, hz⟩] at A
+      have t₀ : (h₄g z hz).order ≠ ⊤ := by
+        by_contra hC
+        rw [hC] at A
+        tauto
+      have t₁ : ∃ n : ℕ, (h₄g z hz).order = n := by
+        exact Option.ne_none_iff_exists'.mp t₀
+      obtain ⟨n, hn⟩ := t₁
+      rw [hn] at A
+      apply WithTopCoe
+      rw [eq_comm]
+      rw [hn]
+      exact A
+    · intro z hz
+      have t₀ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ f x := by
+        sorry
+      have t₂ : ∀ᶠ x in 𝓝[≠] z, h₁f.divisor z = 0 := by
+        sorry
+      have t₁ : ∀ᶠ x in 𝓝[≠] z, AnalyticAt ℂ (fun z => ∏ᶠ (p : ℂ), (z - p) ^ h₁f.divisor p * g z) x := by
+        sorry
+      apply Filter.EventuallyEq.eq_of_nhds
+      apply StronglyMeromorphicAt.localIdentity
+      · exact StronglyMeromorphicOn_of_makeStronglyMeromorphic h₁f z hz
+      · right
+        use h₁f.divisor z
+        use (∏ᶠ p : ({z}ᶜ : Set ℂ), (fun x ↦ (x - p.1) ^ h₁f.divisor p.1)) * g
+        constructor
+        · apply AnalyticAt.mul₁
+          · apply analyticAt_finprod
+            intro w
+
+
+            sorry
+          · apply (h₃g z hz).analytic
+            rw [h₂g ⟨z, hz⟩]
+        · constructor
+          · sorry
+          · sorry
+
+      sorry

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85",
+   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7",
+   "rev": "de91b59101763419997026c35a41432ac8691f15",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,17 +35,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.42",
+   "inputRev": "v0.0.46",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "scope": "leanprover",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,27 +55,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
-  {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git",
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1",
+   "scope": "leanprover-community",
+   "rev": "86d0d0584f5cd165353e2f8a30c455cd0e168ac2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "4e40837aec257729b3c38dc3e635fc64a7a8a8c1",
+   "rev": "e3d7d7f053ea862ffb7d1613eff6de0f2e3e8e14",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.14.0-rc2