Working…

Nevanlinna/codiscreteWithin.lean

@@ -0,0 +1,11 @@
+import Mathlib.Topology.DiscreteSubset
+
+theorem codiscreteWithin_congr
+  {X : Type u_1} [TopologicalSpace X]
+  {S T U : Set X}
+  (hST : S ∩ U = T ∩ U) :
+  S ∈ Filter.codiscreteWithin U ↔ T ∈ Filter.codiscreteWithin U := by
+  repeat rw [mem_codiscreteWithin]
+  rw [← Set.diff_inter_self_eq_diff (t := S)]
+  rw [← Set.diff_inter_self_eq_diff (t := T)]
+  rw [hST]

Nevanlinna/meromorphicOn.lean

@@ -107,40 +107,79 @@ theorem MeromorphicOn.clopen_of_order_eq_top
 theorem MeromorphicOn.order_ne_top'
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  (hU : IsConnected U)
   (h₁f : MeromorphicOn f U)
-  (h₂f : ∃ u : U, (h₁f u u.2).order ≠ ⊤) :
-  ∀ u : U, (h₁f u u.2).order ≠ ⊤ := by
+  (hU : IsConnected U) :
+  (∃ u : U, (h₁f u u.2).order ≠ ⊤) ↔ (∀ u : U, (h₁f u u.2).order ≠ ⊤) := by
 
-  let A := h₁f.clopen_of_order_eq_top
-  have : PreconnectedSpace U := by
-    apply isPreconnected_iff_preconnectedSpace.mp
-    exact IsConnected.isPreconnected hU
-  rw [isClopen_iff] at A
-  rcases A with h|h
-  · intro u
-    have : u ∉ (∅ : Set U) := by exact fun a => a
-    rw [← h] at this
-    simp at this
-    tauto
-  · obtain ⟨u, hU⟩ := h₂f
-    have A : u ∈ Set.univ := by trivial
-    rw [← h] at A
-    simp at A
-    tauto
+  constructor
+  · intro h₂f
+    let A := h₁f.clopen_of_order_eq_top
+    have : PreconnectedSpace U := by
+      apply isPreconnected_iff_preconnectedSpace.mp
+      exact IsConnected.isPreconnected hU
+    rw [isClopen_iff] at A
+    rcases A with h|h
+    · intro u
+      have : u ∉ (∅ : Set U) := by exact fun a => a
+      rw [← h] at this
+      simp at this
+      tauto
+    · obtain ⟨u, hU⟩ := h₂f
+      have A : u ∈ Set.univ := by trivial
+      rw [← h] at A
+      simp at A
+      tauto
+  · intro h₂f
+    let A := hU.nonempty
+    obtain ⟨v, hv⟩ := A
+    use ⟨v, hv⟩
+    exact h₂f ⟨v, hv⟩
 
 
-theorem MeromorphicOn.order_ne_top
+theorem StronglyMeromorphicOn.order_ne_top
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  (hU : IsConnected U)
   (h₁f : StronglyMeromorphicOn f U)
+  (hU : IsConnected U)
   (h₂f : ∃ u : U, f u ≠ 0) :
   ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
 
-  apply MeromorphicOn.order_ne_top' hU h₁f.meromorphicOn
+  rw [← h₁f.meromorphicOn.order_ne_top' hU]
   obtain ⟨u, hu⟩ := h₂f
   use u
   rw [← (h₁f u u.2).order_eq_zero_iff] at hu
   rw [hu]
   simp
+
+
+theorem MeromorphicOn.nonvanish_of_order_ne_top
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁f : MeromorphicOn f U)
+  (h₂f : ∃ u : U, (h₁f u u.2).order ≠ ⊤)
+  (h₁U : IsConnected U)
+  (h₂U : interior U ≠ ∅) :
+  ∃ u ∈ U, f u ≠ 0 := by
+
+  by_contra hCon
+  push_neg at hCon
+
+  have : ∃ u : U, (h₁f u u.2).order = ⊤ := by
+    obtain ⟨v, h₁v⟩ := Set.nonempty_iff_ne_empty'.2 h₂U
+    have h₂v : v ∈ U := by apply interior_subset h₁v
+    use ⟨v, h₂v⟩
+    rw [MeromorphicAt.order_eq_top_iff]
+    rw [eventually_nhdsWithin_iff]
+    rw [eventually_nhds_iff]
+    use interior U
+    constructor
+    · intro y h₁y h₂y
+      exact hCon y (interior_subset h₁y)
+    · simp [h₁v]
+
+  let A := h₁f.order_ne_top' h₁U
+  rw [← not_iff_not] at A
+  push_neg at A
+  have B := A.2 this
+  obtain ⟨u, hu⟩ := h₂f
+  tauto

Nevanlinna/meromorphicOn_divisor.lean

@@ -163,6 +163,8 @@ theorem MeromorphicOn.divisor_of_makeStronglyMeromorphicOn
 
 
 
+-- STRONGLY MEROMORPHIC THINGS
+
 /- Strongly MeromorphicOn of non-negative order is analytic -/
 theorem StronglyMeromorphicOn.analyticOnNhd
   {f : ℂ → ℂ}
@@ -188,16 +190,16 @@ theorem StronglyMeromorphicOn.analyticOnNhd
 theorem StronglyMeromorphicOn.support_divisor
   {f : ℂ → ℂ}
   {U : Set ℂ}
-  (hU : IsConnected U)
   (h₁f : StronglyMeromorphicOn f U)
-  (h₂f : ∃ u : U, f u ≠ 0) :
+  (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 [MeromorphicOn.order_ne_top hU h₁f h₂f ⟨u, hu.1⟩]
+    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

Nevanlinna/meromorphicOn_integrability.lean

@@ -6,6 +6,7 @@ import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
 import Nevanlinna.meromorphicOn_divisor
 import Nevanlinna.stronglyMeromorphicOn
+import Nevanlinna.stronglyMeromorphicOn_eliminate
 import Nevanlinna.mathlibAddOn
 
 open scoped Interval Topology
@@ -42,7 +43,7 @@ theorem d
 
 
 theorem integrability_congr_changeDiscrete₀
-  {f₁ f₂ : ℂ → ℂ}
+  {f₁ f₂ : ℂ → ℝ}
   {U : Set ℂ}
   {r : ℝ}
   (hU : Metric.sphere 0 |r| ⊆ U)
@@ -68,10 +69,10 @@ theorem integrability_congr_changeDiscrete₀
 
 
 theorem integrability_congr_changeDiscrete
-  {f₁ f₂ : ℂ → ℂ}
+  {f₁ f₂ : ℂ → ℝ}
   {U : Set ℂ}
   {r : ℝ}
-  (hU : Metric.sphere 0 |r| ⊆ U)
+  (hU : Metric.sphere (0 : ℂ) |r| ⊆ U)
   (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) :
   IntervalIntegrable (f₁ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) ↔ IntervalIntegrable (f₂ ∘ (circleMap 0 r)) MeasureTheory.volume 0 (2 * π) := by
 
@@ -81,7 +82,7 @@ theorem integrability_congr_changeDiscrete
 
 
 theorem integral_congr_changeDiscrete
-  {f₁ f₂ : ℂ → ℂ}
+  {f₁ f₂ : ℂ → ℝ}
   {U : Set ℂ}
   {r : ℝ}
   (hr : r ≠ 0)
@@ -95,3 +96,28 @@ theorem integral_congr_changeDiscrete
   constructor
   · apply Set.Countable.measure_zero (d hr hU hf)
   · tauto
+
+
+theorem MeromorphicOn.integrable_log_abs_f
+  {f : ℂ → ℂ}
+  {r : ℝ}
+  (hr : 0 < r)
+  (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) r))
+  (h₂f : ∃ u : (Metric.closedBall (0 : ℂ) r), (h₁f u u.2).order ≠ ⊤) :
+  IntervalIntegrable (fun z ↦ log ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by
+
+  have h₁U : IsCompact (Metric.closedBall (0 : ℂ) r) := by sorry
+  have h₂U : IsConnected (Metric.closedBall (0 : ℂ) r) := by sorry
+  have h₃U : interior (Metric.closedBall (0 : ℂ) r) ≠ ∅ := by sorry
+
+  obtain ⟨g, h₁g, h₂g, h₃g⟩ := MeromorphicOn.decompose_log h₁U h₂U h₃U h₁f h₂f
+  have : (fun z ↦ log ‖f (circleMap 0 r z)‖) = (fun z ↦ log ‖f z‖) ∘ (circleMap 0 r) := by
+    rfl
+  rw [this]
+  have : Metric.sphere (0 : ℂ) |r| ⊆ Metric.closedBall (0 : ℂ) r := by
+    sorry
+  rw [integrability_congr_changeDiscrete this h₃g]
+
+  apply IntervalIntegrable.add
+  sorry
+  sorry

Nevanlinna/stronglyMeromorphicOn_eliminate.lean

@@ -1,5 +1,6 @@
 import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.analyticAt
+import Nevanlinna.codiscreteWithin
 import Nevanlinna.divisor
 import Nevanlinna.meromorphicAt
 import Nevanlinna.meromorphicOn
@@ -293,7 +294,6 @@ theorem MeromorphicOn.decompose₂
           simpa
 
 
-
 theorem MeromorphicOn.decompose₃'
   {f : ℂ → ℂ}
   {U : Set ℂ}
@@ -306,7 +306,8 @@ theorem MeromorphicOn.decompose₃'
     ∧ (∀ 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 ≠ ⊤ := MeromorphicOn.order_ne_top h₂U h₁f h₂f
+  have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ :=
+    StronglyMeromorphicOn.order_ne_top h₁f h₂U h₂f
   have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U
 
   let d := - h₁f.meromorphicOn.divisor.toFun
@@ -492,8 +493,7 @@ theorem MeromorphicOn.decompose₃'
           tauto
 
 
-
-theorem MeromorphicOn.decompose_log
+theorem StronglyMeromorphicOn.decompose_log
   {f : ℂ → ℂ}
   {U : Set ℂ}
   (h₁U : IsCompact U)
@@ -529,8 +529,15 @@ theorem MeromorphicOn.decompose_log
   rw [Filter.eventuallyEq_iff_exists_mem]
   use {z | f z ≠ 0}
   constructor
-  ·
-    sorry
+  · have A := h₁f.meromorphicOn.divisor.codiscreteWithin
+    have : {z | f z ≠ 0} ∩ U = (Function.support h₁f.meromorphicOn.divisor)ᶜ ∩ U := by
+      rw [← h₁f.support_divisor h₂f h₂U]
+      ext u
+      simp; tauto
+
+    rw [codiscreteWithin_congr this]
+    exact A
+
   · intro z hz
     nth_rw 1 [h₄g]
     simp
@@ -588,3 +595,46 @@ theorem MeromorphicOn.decompose_log
     let c := b.1
     simp_rw [hCon] at c
     tauto
+
+  exact 0
+
+
+theorem MeromorphicOn.decompose_log
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (h₁U : IsCompact U)
+  (h₂U : IsConnected U)
+  (h₃U : interior U ≠ ∅)
+  (h₁f : MeromorphicOn f U)
+  (h₂f : ∃ u : U, (h₁f u u.2).order ≠ ⊤) :
+  ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U)
+    ∧ (∀ u : U, g u ≠ 0)
+    ∧ (fun z ↦ log ‖f z‖) =ᶠ[Filter.codiscreteWithin U] fun z ↦ log ‖g z‖ + ∑ᶠ s, (h₁f.divisor s) * log ‖z - s‖ := by
+
+  let F := h₁f.makeStronglyMeromorphicOn
+  have h₁F := stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁f
+  have h₂F : ∃ u : U, (h₁F.meromorphicOn u u.2).order ≠ ⊤ := by
+    obtain ⟨u, hu⟩ := h₂f
+    use u
+    rw [makeStronglyMeromorphicOn_changeOrder h₁f u.2]
+    assumption
+
+  have t₁ : ∃ u : U, F u ≠ 0 := by
+    let A := h₁F.meromorphicOn.nonvanish_of_order_ne_top h₂F h₂U h₃U
+    tauto
+  have t₃ : (fun z ↦ log ‖f z‖) =ᶠ[Filter.codiscreteWithin U] (fun z ↦ log ‖F z‖) := by
+    -- This would be interesting for a tactic
+    rw [eventuallyEq_iff_exists_mem]
+    obtain ⟨s, h₁s, h₂s⟩ := eventuallyEq_iff_exists_mem.1 (makeStronglyMeromorphicOn_changeDiscrete'' h₁f)
+    use s
+    tauto
+
+  obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := h₁F.decompose_log h₁U h₂U t₁
+  use g
+  constructor
+  · exact h₂g
+  · constructor
+    · exact h₃g
+    · apply t₃.trans
+      rw [h₁f.divisor_of_makeStronglyMeromorphicOn]
+      exact h₄g