import Mathlib.Analysis.Analytic.Meromorphic import Nevanlinna.analyticAt import Nevanlinna.mathlibAddOn 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 /- 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 lemma Mnhds {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 theorem 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 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 localIdentity h₁g 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 let 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 localIdentity h₁g 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