Working…

Nevanlinna/stronglyMeromorphicOn.lean

@@ -78,96 +78,3 @@ theorem makeStronglyMeromorphicOn_changeDiscrete
       rw [← StronglyMeromorphicAt.makeStronglyMeromorphic_id]
       exact AnalyticAt.stronglyMeromorphicAt (h₂V v hv)
     · simp [h₂v]
-
-
-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₂
-  {U : Set ℂ}
-  (d : ℂ → ℤ)
-  (P : Finset ℂ) :
-  StronglyMeromorphicOn (∏ u ∈ P, fun z ↦ (z - u) ^ d u) 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₃
-  {U : Set ℂ}
-  (d : ℂ → ℤ) :
-  StronglyMeromorphicOn (∏ᶠ u, fun z ↦ (z - u) ^ d u) U := by
-  by_cases hd : (Function.mulSupport fun u z => (z - u) ^ d u).Finite
-  · rw [finprod_eq_prod _ hd]
-    apply stronglyMeromorphicOn_ratlPolynomial₂ (U := U) d hd.toFinset
-  · rw [finprod_of_infinite_mulSupport hd]
-    apply AnalyticOn.stronglyMeromorphicOn
-    apply analyticOnNhd_const
-
-
-theorem stronglyMeromorphicOn_divisor_ratlPolynomial
-  {U : Set ℂ}
-  (d : ℂ → ℤ)
-  (hd : Set.Finite d.support) :
-  (stronglyMeromorphicOn_ratlPolynomial₃ d (U := U)).meromorphicOn.divisor = d := by
-  sorry
-
-
-theorem makeStronglyMeromorphicOn_changeDiscrete'
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  {z₀ : ℂ}
-  (hf : MeromorphicOn f U)
-  (hz₀ : z₀ ∈ U) :
-  hf.makeStronglyMeromorphicOn =ᶠ[𝓝 z₀] (hf z₀ hz₀).makeStronglyMeromorphicAt := by
-  apply Mnhds
-  let A := makeStronglyMeromorphicOn_changeDiscrete hf hz₀
-  apply Filter.EventuallyEq.trans A
-  exact m₂ (hf z₀ hz₀)
-  unfold MeromorphicOn.makeStronglyMeromorphicOn
-  simp [hz₀]
-
-
-theorem StronglyMeromorphicOn_of_makeStronglyMeromorphicOn
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : MeromorphicOn f U) :
-  StronglyMeromorphicOn hf.makeStronglyMeromorphicOn U := by
-  intro z₀ hz₀
-  rw [stronglyMeromorphicAt_congr (makeStronglyMeromorphicOn_changeDiscrete' hf hz₀)]
-  exact StronglyMeromorphicAt_of_makeStronglyMeromorphic (hf z₀ hz₀)

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -1,5 +1,4 @@
 import Mathlib.Analysis.Analytic.Meromorphic
-import Mathlib.Data.Set.Finite
 import Nevanlinna.analyticAt
 import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt

Nevanlinna/stronglyMeromorphicOn_ratlPolynomial.lean

@@ -0,0 +1,344 @@
+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, 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