import Mathlib.Analysis.Analytic.Meromorphic import Nevanlinna.analyticAt import Nevanlinna.divisor import Nevanlinna.meromorphicAt import Nevanlinna.meromorphicOn import Nevanlinna.stronglyMeromorphicOn 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 theorem MeromorphicOn.divisor_def₁ {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ} (hf : MeromorphicOn f U) (hz : z ∈ U) : hf.divisor z = ((hf z hz).order.untop' 0 : ℤ) := by unfold MeromorphicOn.divisor simp [hz] theorem MeromorphicOn.divisor_def₂ {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ} (hf : MeromorphicOn f U) (hz : z ∈ U) (h₂f : (hf z hz).order ≠ ⊤) : hf.divisor z = (hf z hz).order.untop h₂f := by unfold MeromorphicOn.divisor simp [hz] rw [WithTop.untop'_eq_iff] left exact Eq.symm (WithTop.coe_untop (hf z hz).order h₂f) theorem MeromorphicOn.divisor_mul₀ {f₁ f₂ : ℂ → ℂ} {U : Set ℂ} {z : ℂ} (hz : z ∈ U) (h₁f₁ : MeromorphicOn f₁ U) (h₂f₁ : (h₁f₁ z hz).order ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ U) (h₂f₂ : (h₁f₂ z hz).order ≠ ⊤) : (h₁f₁.mul h₁f₂).divisor.toFun z = h₁f₁.divisor.toFun z + h₁f₂.divisor.toFun z := by by_cases h₁z : z ∈ U · rw [MeromorphicOn.divisor_def₂ h₁f₁ hz h₂f₁] rw [MeromorphicOn.divisor_def₂ h₁f₂ hz h₂f₂] have B : ((h₁f₁.mul h₁f₂) z hz).order ≠ ⊤ := by rw [MeromorphicAt.order_mul (h₁f₁ z hz) (h₁f₂ z hz)] simp; tauto rw [MeromorphicOn.divisor_def₂ (h₁f₁.mul h₁f₂) hz B] simp_rw [MeromorphicAt.order_mul (h₁f₁ z hz) (h₁f₂ z hz)] rw [untop_add] · unfold MeromorphicOn.divisor simp [h₁z] theorem MeromorphicOn.divisor_mul {f₁ f₂ : ℂ → ℂ} {U : Set ℂ} (h₁f₁ : MeromorphicOn f₁ U) (h₂f₁ : ∀ z, (hz : z ∈ U) → (h₁f₁ z hz).order ≠ ⊤) (h₁f₂ : MeromorphicOn f₂ U) (h₂f₂ : ∀ z, (hz : z ∈ U) → (h₁f₂ z hz).order ≠ ⊤) : (h₁f₁.mul h₁f₂).divisor.toFun = h₁f₁.divisor.toFun + h₁f₂.divisor.toFun := by funext z by_cases hz : z ∈ U · rw [MeromorphicOn.divisor_mul₀ hz h₁f₁ (h₂f₁ z hz) h₁f₂ (h₂f₂ z hz)] simp · simp rw [Function.nmem_support.mp (fun a => hz (h₁f₁.divisor.supportInU a))] rw [Function.nmem_support.mp (fun a => hz (h₁f₂.divisor.supportInU a))] rw [Function.nmem_support.mp (fun a => hz ((h₁f₁.mul h₁f₂).divisor.supportInU a))] simp theorem MeromorphicOn.divisor_inv {f: ℂ → ℂ} {U : Set ℂ} (h₁f : MeromorphicOn f U) : h₁f.inv.divisor.toFun = -h₁f.divisor.toFun := by funext z by_cases hz : z ∈ U · rw [MeromorphicOn.divisor_def₁] simp rw [MeromorphicOn.divisor_def₁] rw [MeromorphicAt.order_inv] simp by_cases h₂f : (h₁f z hz).order = ⊤ · simp [h₂f] · let A := untop'_of_ne_top (d := 0) h₂f rw [← A] exact rfl repeat exact hz · unfold MeromorphicOn.divisor simp [hz] theorem MeromorphicOn.divisor_add_const₁ {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ} (hf : MeromorphicOn f U) (a : ℂ) : 0 ≤ hf.divisor z → 0 ≤ (hf.add (MeromorphicOn.const a)).divisor z := by intro h unfold MeromorphicOn.divisor -- Trivial case: z ∉ U by_cases hz : z ∉ U · simp [hz] -- Non-trivial case: z ∈ U simp at hz; simp [hz] by_cases h₁f : (hf z hz).order = ⊤ · have : f + (fun z ↦ a) =ᶠ[𝓝[≠] z] (fun z ↦ a) := by rw [MeromorphicAt.order_eq_top_iff] at h₁f rw [eventually_nhdsWithin_iff] at h₁f rw [eventually_nhds_iff] at h₁f obtain ⟨t, ht⟩ := h₁f rw [eventuallyEq_nhdsWithin_iff] rw [eventually_nhds_iff] use t simp [ht] tauto rw [((hf z hz).add (MeromorphicAt.const a z)).order_congr this] by_cases ha: (MeromorphicAt.const a z).order = ⊤ · simp [ha] · rw [WithTop.le_untop'_iff] apply AnalyticAt.meromorphicAt_order_nonneg exact analyticAt_const tauto · rw [WithTop.le_untop'_iff] let A := (hf z hz).order_add (MeromorphicAt.const a z) have : 0 ≤ min (hf z hz).order (MeromorphicAt.const a z).order := by apply le_min -- unfold MeromorphicOn.divisor at h simp [hz] at h let V := untop'_of_ne_top (d := 0) h₁f rw [← V] simp [h] -- apply AnalyticAt.meromorphicAt_order_nonneg exact analyticAt_const exact le_trans this A tauto theorem MeromorphicOn.divisor_add_const₂ {f : ℂ → ℂ} {U : Set ℂ} {z : ℂ} (hf : MeromorphicOn f U) (a : ℂ) : hf.divisor z < 0 → (hf.add (MeromorphicOn.const a)).divisor z < 0 := by intro h by_cases hz : z ∉ U · have : hf.divisor z = 0 := by unfold MeromorphicOn.divisor simp [hz] rw [this] at h tauto simp at hz unfold MeromorphicOn.divisor simp [hz] unfold MeromorphicOn.divisor at h simp [hz] at h have : (hf z hz).order = (((hf.add (MeromorphicOn.const a))) z hz).order := by have t₀ : (hf z hz).order < (0 : ℤ) := by by_contra hCon simp only [not_lt] at hCon rw [←WithTop.le_untop'_iff (b := 0)] at hCon exact Lean.Omega.Int.le_lt_asymm hCon h tauto rw [← MeromorphicAt.order_add_of_ne_orders (hf z hz) (MeromorphicAt.const a z)] simp by_cases ha: (MeromorphicAt.const a z).order = ⊤ · simp [ha] · calc (hf z hz).order _ ≤ 0 := by exact le_of_lt t₀ _ ≤ (MeromorphicAt.const a z).order := by apply AnalyticAt.meromorphicAt_order_nonneg exact analyticAt_const apply ne_of_lt calc (hf z hz).order _ < 0 := by exact t₀ _ ≤ (MeromorphicAt.const a z).order := by apply AnalyticAt.meromorphicAt_order_nonneg exact analyticAt_const rwa [this] at h theorem MeromorphicOn.divisor_of_makeStronglyMeromorphicOn {f : ℂ → ℂ} {U : Set ℂ} (hf : MeromorphicOn f U) : hf.divisor = (stronglyMeromorphicOn_of_makeStronglyMeromorphicOn hf).meromorphicOn.divisor := by unfold MeromorphicOn.divisor simp funext z by_cases hz : z ∈ U · simp [hz] congr 1 apply MeromorphicAt.order_congr exact EventuallyEq.symm (makeStronglyMeromorphicOn_changeDiscrete hf hz) · simp [hz] -- STRONGLY MEROMORPHIC THINGS /- Strongly MeromorphicOn of non-negative order is analytic -/ theorem StronglyMeromorphicOn.analyticOnNhd {f : ℂ → ℂ} {U : Set ℂ} (h₁f : StronglyMeromorphicOn f U) (h₂f : ∀ x, (hx : x ∈ U) → 0 ≤ h₁f.meromorphicOn.divisor x) : AnalyticOnNhd ℂ f U := by apply StronglyMeromorphicOn.analytic intro z hz let A := h₂f z hz unfold MeromorphicOn.divisor at A simp [hz] at A by_cases h : (h₁f z hz).meromorphicAt.order = ⊤ · rw [h] simp · rw [WithTop.le_untop'_iff] at A tauto tauto assumption theorem StronglyMeromorphicOn.support_divisor {f : ℂ → ℂ} {U : Set ℂ} (h₁f : StronglyMeromorphicOn f U) (h₂f : ∃ u : U, f u ≠ 0) (hU : IsConnected U) : U ∩ f⁻¹' {0} = (Function.support h₁f.meromorphicOn.divisor) := by ext u constructor · intro hu unfold MeromorphicOn.divisor simp [h₁f.order_ne_top hU h₂f ⟨u, hu.1⟩] use hu.1 rw [(h₁f u hu.1).order_eq_zero_iff] simp exact hu.2 · intro hu simp at hu let A := h₁f.meromorphicOn.divisor.supportInU hu constructor · exact h₁f.meromorphicOn.divisor.supportInU hu · simp let B := (h₁f u A).order_eq_zero_iff.not simp at B rw [← B] unfold MeromorphicOn.divisor at hu simp [A] at hu exact hu.1