Nevanlinna/analyticAt.lean

@@ -308,37 +308,3 @@ theorem AnalyticAt.zpow
       intro x
       rw [zpow_neg]
     exact AnalyticAt.inv (zpow_nonneg h₁f (by linarith)) (zpow_ne_zero (-n) h₂f)
-
-
-/- A function is analytic at a point iff it is analytic after multiplication
-   with a non-vanishing analytic function
--/
-theorem analyticAt_of_mul_analytic
-  {f g : ℂ → ℂ}
-  {z₀ : ℂ}
-  (h₁g : AnalyticAt ℂ g z₀)
-  (h₂g : g z₀ ≠ 0) :
-  AnalyticAt ℂ f z₀ ↔ AnalyticAt ℂ (f * g) z₀ := by
-  constructor
-  · exact fun a => AnalyticAt.mul₁ a h₁g
-  · intro hprod
-
-    let g' := fun z ↦ (g z)⁻¹
-    have h₁g' := h₁g.inv h₂g
-    have h₂g' : g' z₀ ≠ 0 := by
-      exact inv_ne_zero h₂g
-
-    have : f =ᶠ[𝓝 z₀] f * g * fun x => (g x)⁻¹ := by
-      unfold Filter.EventuallyEq
-      apply Filter.eventually_iff_exists_mem.mpr
-      use g⁻¹' {0}ᶜ
-      constructor
-      · apply ContinuousAt.preimage_mem_nhds
-        exact AnalyticAt.continuousAt h₁g
-        exact compl_singleton_mem_nhds_iff.mpr h₂g
-      · intro y hy
-        simp at hy
-        simp [hy]
-    rw [analyticAt_congr this]
-    apply hprod.mul
-    exact h₁g'

Nevanlinna/stronglyMeromorphicAt.lean

@@ -15,51 +15,6 @@ def StronglyMeromorphicAt
   (∀ᶠ (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))
 
 
-lemma stronglyMeromorphicAt_of_mul_analytic'
-  {f g : ℂ → ℂ}
-  {z₀ : ℂ}
-  (h₁g : AnalyticAt ℂ g z₀)
-  (h₂g : g z₀ ≠ 0) :
-  StronglyMeromorphicAt f z₀ → StronglyMeromorphicAt (f * g) z₀ := by
-
-  intro hf
-  --unfold StronglyMeromorphicAt at hf
-  rcases hf with h₁f|h₁f
-  · left
-    rw [eventually_nhds_iff] at h₁f
-    obtain ⟨t, ht⟩ := h₁f
-    rw [eventually_nhds_iff]
-    use t
-    constructor
-    · intro y hy
-      simp
-      left
-      exact ht.1 y hy
-    · exact ht.2
-  · right
-    obtain ⟨n, g_f, h₁g_f, h₂g_f, h₃g_f⟩ := h₁f
-    use n
-    use g * g_f
-    constructor
-    · apply AnalyticAt.mul
-      exact h₁g
-      exact h₁g_f
-    · constructor
-      · simp
-        exact ⟨h₂g, h₂g_f⟩
-      · rw [eventually_nhds_iff] at h₃g_f
-        obtain ⟨t, ht⟩ := h₃g_f
-        rw [eventually_nhds_iff]
-        use t
-        constructor
-        · intro y hy
-          simp
-          rw [ht.1]
-          simp
-          ring
-          exact hy
-        · exact ht.2
-
 
 /- Strongly MeromorphicAt is Meromorphic -/
 theorem StronglyMeromorphicAt.meromorphicAt
@@ -169,37 +124,6 @@ theorem stronglyMeromorphicAt_congr
         · apply Filter.EventuallyEq.trans hfg
           assumption
 
-/- A function is strongly meromorphic at a point iff it is strongly meromorphic
-   after multiplication with a non-vanishing analytic function
--/
-theorem stronglyMeromorphicAt_of_mul_analytic
-  {f g : ℂ → ℂ}
-  {z₀ : ℂ}
-  (h₁g : AnalyticAt ℂ g z₀)
-  (h₂g : g z₀ ≠ 0) :
-  StronglyMeromorphicAt f z₀ ↔ StronglyMeromorphicAt (f * g) z₀ := by
-  constructor
-  · apply stronglyMeromorphicAt_of_mul_analytic' h₁g h₂g
-  · intro hprod
-    let g' := fun z ↦ (g z)⁻¹
-    have h₁g' := h₁g.inv h₂g
-    have h₂g' : g' z₀ ≠ 0 := by
-      exact inv_ne_zero h₂g
-
-    let B := stronglyMeromorphicAt_of_mul_analytic' h₁g' h₂g' (f := f * g) hprod
-    have : f =ᶠ[𝓝 z₀] f * g * fun x => (g x)⁻¹ := by
-      unfold Filter.EventuallyEq
-      apply Filter.eventually_iff_exists_mem.mpr
-      use g⁻¹' {0}ᶜ
-      constructor
-      · apply ContinuousAt.preimage_mem_nhds
-        exact AnalyticAt.continuousAt h₁g
-        exact compl_singleton_mem_nhds_iff.mpr h₂g
-      · intro y hy
-        simp at hy
-        simp [hy]
-    rwa [stronglyMeromorphicAt_congr this]
-
 
 theorem StronglyMeromorphicAt.order_eq_zero_iff
   {f : ℂ → ℂ}

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -10,14 +10,22 @@ import Nevanlinna.mathlibAddOn
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
+lemma untop_eq_untop'
+  {n : WithTop ℤ}
+  (hn : n ≠ ⊤) :
+  n.untop' 0 = n.untop hn := by
+  rw [WithTop.untop'_eq_iff]
+  simp
+
+
 theorem MeromorphicOn.decompose₁
   {f : ℂ → ℂ}
   {U : Set ℂ}
   {z₀ : ℂ}
+  (hz₀ : z₀ ∈ U)
   (h₁f : MeromorphicOn f U)
   (h₂f : StronglyMeromorphicAt f z₀)
-  (h₃f : h₂f.meromorphicAt.order ≠ ⊤)
+  (h₃f : h₂f.meromorphicAt.order ≠ ⊤) :
-  (hz₀ : z₀ ∈ U) :
   ∃ g : ℂ → ℂ, (MeromorphicOn g U)
     ∧ (AnalyticAt ℂ g z₀)
     ∧ (g z₀ ≠ 0)
@@ -141,152 +149,3 @@ theorem MeromorphicOn.decompose₁
           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