import Mathlib.Analysis.Analytic.Meromorphic import Nevanlinna.analyticAt import Nevanlinna.divisor import Nevanlinna.meromorphicAt import Nevanlinna.meromorphicOn 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 ℂ} {z₀ : ℂ} (h₁f : MeromorphicOn f U) (h₂f : StronglyMeromorphicAt f z₀) (h₃f : h₂f.meromorphicAt.order ≠ ⊤) (hz₀ : z₀ ∈ U) : ∃ g : ℂ → ℂ, (MeromorphicOn g U) ∧ (AnalyticAt ℂ g z₀) ∧ (g z₀ ≠ 0) ∧ (f = g * fun z ↦ (z - z₀) ^ (h₁f.divisor z₀)) := by let h₁ := fun z ↦ (z - z₀) ^ (-h₁f.divisor z₀) have h₁h₁ : MeromorphicOn h₁ U := by apply MeromorphicOn.zpow apply AnalyticOnNhd.meromorphicOn apply AnalyticOnNhd.sub exact analyticOnNhd_id exact analyticOnNhd_const let n : ℤ := (-h₁f.divisor z₀) have h₂h₁ : (h₁h₁ z₀ hz₀).order = n := by simp_rw [(h₁h₁ z₀ hz₀).order_eq_int_iff] use 1 constructor · apply analyticAt_const · constructor · simp · apply eventually_nhdsWithin_of_forall intro z hz simp let g₁ := f * h₁ have h₁g₁ : MeromorphicOn g₁ U := by apply h₁f.mul h₁h₁ have h₂g₁ : (h₁g₁ z₀ hz₀).order = 0 := by rw [(h₁f z₀ hz₀).order_mul (h₁h₁ z₀ hz₀)] rw [h₂h₁] unfold n rw [MeromorphicOn.divisor_def₂ h₁f hz₀ h₃f] conv => left left rw [Eq.symm (WithTop.coe_untop (h₁f z₀ hz₀).order h₃f)] have (a b c : ℤ) (h : a + b = c) : (a : WithTop ℤ) + (b : WithTop ℤ) = (c : WithTop ℤ) := by rw [← h] simp rw [this ((h₁f z₀ hz₀).order.untop h₃f) (-(h₁f z₀ hz₀).order.untop h₃f) 0] simp ring let g := (h₁g₁ z₀ hz₀).makeStronglyMeromorphicAt have h₂g : StronglyMeromorphicAt g z₀ := by exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (h₁g₁ z₀ hz₀) have h₁g : MeromorphicOn g U := by intro z hz by_cases h₁z : z = z₀ · rw [h₁z] apply h₂g.meromorphicAt · apply (h₁g₁ z hz).congr rw [eventuallyEq_nhdsWithin_iff] rw [eventually_nhds_iff] use {z₀}ᶜ constructor · intro y h₁y h₂y let A := m₁ (h₁g₁ z₀ hz₀) y h₁y unfold g rw [← A] · constructor · exact isOpen_compl_singleton · exact h₁z have h₃g : (h₁g z₀ hz₀).order = 0 := by unfold g let B := m₂ (h₁g₁ z₀ hz₀) let A := (h₁g₁ z₀ hz₀).order_congr B rw [← A] rw [h₂g₁] have h₄g : AnalyticAt ℂ g z₀ := by apply h₂g.analytic rw [h₃g] use g constructor · exact h₁g · constructor · exact h₄g · constructor · exact (h₂g.order_eq_zero_iff).mp h₃g · funext z by_cases hz : z = z₀ · rw [hz] simp by_cases h : h₁f.divisor z₀ = 0 · simp [h] have h₂h₁ : h₁ = 1 := by funext w unfold h₁ simp [h] have h₃g₁ : g₁ = f := by unfold g₁ rw [h₂h₁] simp have h₄g₁ : StronglyMeromorphicAt g₁ z₀ := by rwa [h₃g₁] let A := h₄g₁.makeStronglyMeromorphic_id unfold g rw [← A, h₃g₁] · have : (0 : ℂ) ^ h₁f.divisor z₀ = (0 : ℂ) := by exact zero_zpow (h₁f.divisor z₀) h rw [this] simp let A := h₂f.order_eq_zero_iff.not simp at A rw [← A] unfold MeromorphicOn.divisor at h simp [hz₀] at h exact h.1 · simp let B := m₁ (h₁g₁ z₀ hz₀) z hz unfold g rw [← B] unfold g₁ h₁ simp [hz] rw [mul_assoc] rw [inv_mul_cancel₀] simp apply zpow_ne_zero rwa [sub_ne_zero] theorem MeromorphicOn.decompose₂ {f : ℂ → ℂ} {U : Set ℂ} {P : Finset U} (hf : StronglyMeromorphicOn f U) : (∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) → ∃ g : ℂ → ℂ, (MeromorphicOn g U) ∧ (∀ p : P, AnalyticAt ℂ g p) ∧ (∀ p : P, g p ≠ 0) ∧ (f = g * ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by apply Finset.induction (p := fun (P : Finset U) ↦ (∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) → ∃ g : ℂ → ℂ, (MeromorphicOn g U) ∧ (∀ p : P, AnalyticAt ℂ g p) ∧ (∀ p : P, g p ≠ 0) ∧ (f = g * ∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1))) -- case empty simp exact hf.meromorphicOn -- case insert intro u P hu iHyp intro hOrder obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀, h₄g₀⟩ := iHyp (fun p hp ↦ hOrder p (Finset.mem_insert_of_mem hp)) have h₀ : AnalyticAt ℂ (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u := by have : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) = (fun z => ∏ p : P, (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by funext w simp rw [this] apply Finset.analyticAt_prod intro p hp apply AnalyticAt.zpow apply AnalyticAt.sub apply analyticAt_id apply analyticAt_const by_contra hCon rw [sub_eq_zero] at hCon have : p.1 = u := by exact SetCoe.ext (_root_.id (Eq.symm hCon)) rw [← this] at hu simp [hp] at hu have h₁ : (∏ p : P, fun z ↦ (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) u ≠ 0 := by simp only [Finset.prod_apply] rw [Finset.prod_ne_zero_iff] intro p hp apply zpow_ne_zero by_contra hCon rw [sub_eq_zero] at hCon have : p.1 = u := by exact SetCoe.ext (_root_.id (Eq.symm hCon)) rw [← this] at hu simp [hp] at hu have h₅g₀ : StronglyMeromorphicAt g₀ u := by rw [stronglyMeromorphicAt_of_mul_analytic h₀ h₁] rw [← h₄g₀] exact hf u u.2 have h₆g₀ : (h₁g₀ u u.2).order ≠ ⊤ := by by_contra hCon let A := (h₁g₀ u u.2).order_mul h₀.meromorphicAt simp_rw [← h₄g₀, hCon] at A simp at A let B := hOrder u (Finset.mem_insert_self u P) tauto obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := h₁g₀.decompose₁ h₅g₀ h₆g₀ u.2 use g · constructor · exact h₁g · constructor · intro ⟨v₁, v₂⟩ simp simp at v₂ rcases v₂ with hv|hv · rwa [hv] · let A := h₂g₀ ⟨v₁, hv⟩ rw [h₄g] at A rw [← analyticAt_of_mul_analytic] at A simp at A exact A -- simp apply AnalyticAt.zpow apply AnalyticAt.sub apply analyticAt_id apply analyticAt_const by_contra hCon rw [sub_eq_zero] at hCon have : v₁ = u := by exact SetCoe.ext hCon rw [this] at hv tauto -- apply zpow_ne_zero simp by_contra hCon rw [sub_eq_zero] at hCon have : v₁ = u := by exact SetCoe.ext hCon rw [this] at hv tauto · constructor · intro ⟨v₁, v₂⟩ simp simp at v₂ rcases v₂ with hv|hv · rwa [hv] · by_contra hCon let A := h₃g₀ ⟨v₁,hv⟩ rw [h₄g] at A simp at A tauto · conv => left rw [h₄g₀, h₄g] simp rw [mul_assoc] congr rw [Finset.prod_insert] simp congr have : (hf u u.2).meromorphicAt.order = (h₁g₀ u u.2).order := by have h₅g₀ : f =ᶠ[𝓝 u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by exact Eq.eventuallyEq h₄g₀ have h₆g₀ : f =ᶠ[𝓝[≠] u.1] (g₀ * ∏ p : P, fun z => (z - p.1.1) ^ (hf.meromorphicOn.divisor p.1.1)) := by exact eventuallyEq_nhdsWithin_of_eqOn fun ⦃x⦄ a => congrFun h₄g₀ x rw [(hf u u.2).meromorphicAt.order_congr h₆g₀] let C := (h₁g₀ u u.2).order_mul h₀.meromorphicAt rw [C] let D := h₀.order_eq_zero_iff.2 h₁ let E := h₀.meromorphicAt_order rw [E, D] simp have : hf.meromorphicOn.divisor u = h₁g₀.divisor u := by unfold MeromorphicOn.divisor simp rw [this] rw [this] -- simpa theorem MeromorphicOn.decompose₃ {f : ℂ → ℂ} {U : Set ℂ} (h₁U : IsCompact U) (h₂U : IsConnected U) (h₁f : StronglyMeromorphicOn f U) (h₂f : ∃ u : U, f u ≠ 0) : ∃ g : ℂ → ℂ, (MeromorphicOn g U) ∧ (AnalyticOn ℂ g U) ∧ (∀ u : U, g u ≠ 0) ∧ (f = g * ∏ᶠ u : U, fun z ↦ (z - u.1) ^ (h₁f.meromorphicOn.divisor u.1)) := by have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by let A := h₁f.meromorphicOn.clopen_of_order_eq_top have : PreconnectedSpace U := by apply isPreconnected_iff_preconnectedSpace.mp exact IsConnected.isPreconnected h₂U rw [isClopen_iff] at A rcases A with h|h · intro u have : u ∉ (∅ : Set U) := by exact fun a => a rw [← h] at this simp at this tauto · obtain ⟨u, hu⟩ := h₂f let A := (h₁f u u.2).order_eq_zero_iff.2 hu have : u ∈ (Set.univ : Set U) := by trivial rw [← h] at this simp at this rw [A] at this tauto have h₄f : Finite (Function.support h₁f.meromorphicOn.divisor) := by exact h₁f.meromorphicOn.divisor.finiteSupport h₁U let P' : Set U := Subtype.val ⁻¹' Function.support h₁f.meromorphicOn.divisor have : Finite P' := by unfold P' refine Finite.of_injective ?f ?H simp apply Finite.of_injective sorry sorry