Nevanlinna/stronglyMeromorphic.lean

@@ -98,7 +98,6 @@ noncomputable def MeromorphicAt.makeStronglyMeromorphicAt
     · exact 0
   · exact f z
 
-
 lemma m₁
   {f : ℂ → ℂ}
   {z₀ : ℂ}
@@ -108,7 +107,6 @@ lemma m₁
   unfold MeromorphicAt.makeStronglyMeromorphicAt
   simp [hz]
 
-
 lemma m₂
   {f : ℂ → ℂ}
   {z₀ : ℂ}

Nevanlinna/stronglyMeromorphicOn.lean

@@ -1,175 +0,0 @@
-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 : AnalyticOn ℂ f U) :
-  StronglyMeromorphicOn f U := by
-  intro z hz
-  apply AnalyticAt.stronglyMeromorphicAt
-  let A := h₁f z hz
-  exact h₁f z hz
-
-
-/- 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]