Update stronglyMeromorphicOn_ratlPolynomial.lean

Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean

@@ -1,344 +1,167 @@
-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₁
+
+theorem analyticAt_ratlPolynomial₁
+  {z : ℂ}
+  (d : ℂ → ℤ)
+  (P : Finset ℂ) :
+  z ∉ P → AnalyticAt ℂ (∏ u ∈ P, fun z ↦ (z - u) ^ d u) z := by
+  intro hz
+  rw [Finset.prod_fn]
+  apply Finset.analyticAt_prod
+  intro u hu
+  apply AnalyticAt.zpow
+  apply AnalyticAt.sub
+  apply analyticAt_id
+  apply analyticAt_const
+  rw [sub_ne_zero, ne_comm]
+  exact ne_of_mem_of_not_mem hu hz
+
+
+theorem stronglyMeromorphicOn_ratlPolynomial₂
+  (d : ℂ → ℤ)
+  (P : Finset ℂ) :
+  StronglyMeromorphicOn (∏ u ∈ P, fun z ↦ (z - u) ^ d u) ⊤ := by
+
+  intro z hz
+  by_cases h₂z : z ∈ P
+  · rw [← Finset.mul_prod_erase P _ h₂z]
+    right
+    use d z
+    use ∏ x ∈ P.erase z, fun z => (z - x) ^ d x
+    constructor
+    · have : z ∉ P.erase z := Finset.not_mem_erase z P
+      apply analyticAt_ratlPolynomial₁ d (P.erase z) this
+    · constructor
+      · simp only [Finset.prod_apply]
+        rw [Finset.prod_ne_zero_iff]
+        intro u hu
+        apply zpow_ne_zero
+        rw [sub_ne_zero]
+        by_contra hCon
+        rw [hCon] at hu
+        let A := Finset.not_mem_erase u P
+        tauto
+      · exact Filter.Eventually.of_forall (congrFun rfl)
+  · apply AnalyticAt.stronglyMeromorphicAt
+    exact analyticAt_ratlPolynomial₁ d P (z := z) h₂z
+
+
+theorem stronglyMeromorphicOn_ratlPolynomial₃
+  (d : ℂ → ℤ) :
+  StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) ⊤ := by
+  by_cases hd : (Function.mulSupport fun u z => (z - u) ^ d u).Finite
+  · rw [finprod_eq_prod _ hd]
+    apply stronglyMeromorphicOn_ratlPolynomial₂ d hd.toFinset
+  · rw [finprod_of_infinite_mulSupport hd]
+    apply AnalyticOn.stronglyMeromorphicOn
+    apply analyticOnNhd_const
+
+
+theorem stronglyMeromorphicOn_divisor_ratlPolynomial₁
+  {z : ℂ}
+  (d : ℂ → ℤ)
+  (h₁d : Set.Finite d.support) :
+  (((stronglyMeromorphicOn_ratlPolynomial₃ d).meromorphicOn) z trivial).order = d z := by
+
+  have h₂d : (Function.mulSupport fun u z ↦ (z - u) ^ d u) = d.support := by
+    ext u
+    constructor
+    · intro h
+      simp at h
+      simp
+      by_contra hCon
+      rw [hCon] at h
+      simp at h
+      tauto
+    · intro h
+      simp
+      by_contra hCon
+      let A := congrFun hCon u
+      simp at A
+      have t₁ : (0 : ℂ) ^ d u ≠ 0 := by
+        exact ne_zero_of_eq_one A
+      rw [zpow_ne_zero_iff h] at t₁
+      tauto
+
+  rw [MeromorphicAt.order_eq_int_iff]
+  use ∏ x ∈ h₁d.toFinset.erase z, fun z => (z - x) ^ d x
+  constructor
+  · have : z ∉ h₁d.toFinset.erase z := Finset.not_mem_erase z h₁d.toFinset
+    apply analyticAt_ratlPolynomial₁ d (h₁d.toFinset.erase z) this
+  · constructor
+    · simp only [Finset.prod_apply]
+      rw [Finset.prod_ne_zero_iff]
+      intro u hu
+      apply zpow_ne_zero
+      rw [sub_ne_zero]
+      by_contra hCon
+      rw [hCon] at hu
+      let A := Finset.not_mem_erase u h₁d.toFinset
+      tauto
+    · apply Filter.Eventually.of_forall
+      intro x
+      simp
+
+      rw [← Finset.mul_prod_erase]
+      sorry
+
+  by_cases hz : z ∈ d.support
+  · sorry
+  · use (∏ᶠ u, fun z ↦ (z - u) ^ d u)
+  constructor
+  ·
+    apply?
+
+  simp [hz]
+
+    sorry
+  · rw [Function.nmem_support.mp fun a => hz (h₂d a)]
+    rw [MeromorphicOn.divisor]
+    simp [hz]
+
+
+
+theorem stronglyMeromorphicOn_divisor_ratlPolynomial
+  {U : Set ℂ}
+  (d : ℂ → ℤ)
+  (h₁d : Set.Finite d.support)
+  (h₂d : d.support ⊆ U) :
+  (stronglyMeromorphicOn_ratlPolynomial₃ d (U := U)).meromorphicOn.divisor = d := by
+  funext z
+  by_cases hz : z ∈ U
+  · rw [MeromorphicOn.divisor]
+    simp [hz]
+
+    sorry
+  · rw [Function.nmem_support.mp fun a => hz (h₂d a)]
+    rw [MeromorphicOn.divisor]
+    simp [hz]
+
+
+theorem makeStronglyMeromorphicOn_changeDiscrete'
   {f : ℂ → ℂ}
   {U : Set ℂ}
   {z₀ : ℂ}
-  (h₁f : MeromorphicOn f U)
+  (hf : MeromorphicOn f U)
-  (h₂f : StronglyMeromorphicAt f z₀)
-  (h₃f : h₂f.meromorphicAt.order ≠ ⊤)
   (hz₀ : z₀ ∈ U) :
-  ∃ g : ℂ → ℂ, (MeromorphicOn g U)
+  hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
-    ∧ (AnalyticAt ℂ g z₀)
+  apply Mnhds
-    ∧ (g z₀ ≠ 0)
+  let A := makeStronglyMeromorphicOn_changeDiscrete hf hz₀
-    ∧ (f = g * fun z ↦ (z - z₀) ^ (h₁f.divisor z₀)) := by
+  apply Filter.EventuallyEq.trans A
-
+  exact m₂ (hf z₀ hz₀)
-  let h₁ := fun z ↦ (z - z₀) ^ (-h₁f.divisor z₀)
+  unfold MeromorphicOn.makeStronglyMeromorphicOn
-  have h₁h₁ : MeromorphicOn h₁ U := by
+  simp [hz₀]
-    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₂
+theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  {P : Finset U}
+  (hf : MeromorphicOn f U) :
-  (hf : StronglyMeromorphicOn f U) :
+  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
-  (∀ p ∈ P, (hf p p.2).meromorphicAt.order ≠ ⊤) →
+  intro z₀ hz₀
-    ∃ g : ℂ → ℂ, (MeromorphicOn g U)
+  rw [stronglyMeromorphicAt_congr (makeStronglyMeromorphicOn_changeDiscrete' hf hz₀)]
-    ∧ (∀ p : P, AnalyticAt ℂ g p)
+  exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z₀ hz₀)
-    ∧ (∀ 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, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by
-
-  have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
-    apply MeromorphicOn.order_ne_top h₂U h₁f h₂f
-
-  have h₄f : Set.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
-  let P := (h₄f.preimage Set.injOn_subtype_val : Set.Finite P').toFinset
-  have hP : ∀ p ∈ P, (h₁f p p.2).meromorphicAt.order ≠ ⊤ := by
-    intro p hp
-    apply h₃f
-
-  obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := MeromorphicOn.decompose₂ h₁f (P := P) hP
-
-  let h := ∏ p ∈ P, fun z => (z - p.1) ^ h₁f.meromorphicOn.divisor p.1
-
-  have h₂h : StronglyMeromorphicOn h U := by
-    unfold h
-    apply stronglyMeromorphicOn_ratlPolynomial₂
-  have h₁h : MeromorphicOn h U := by
-    exact StronglyMeromorphicOn.meromorphicOn h₂h
-  have h₃h : h₁h.divisor = h₁f.meromorphicOn.divisor := by
-    sorry
-
-
-  use g
-  constructor
-  · exact h₁g
-  · constructor
-    · sorry
-    · constructor
-      · sorry
-      · conv =>
-          left
-          rw [h₄g]
-        congr
-        simp
-        sorry