working

Nevanlinna/analyticOnNhd_divisor.lean

@@ -0,0 +1,187 @@
+import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
+import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
+import Nevanlinna.analyticAt
+
+open scoped Interval Topology
+open Real Filter MeasureTheory intervalIntegral
+
+
+
+
+structure Divisor where
+  toFun : ℂ → ℤ
+  -- This is not what we want. We want: locally finite
+  discreteSupport : DiscreteTopology (Function.support toFun)
+
+instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
+coe := Divisor.toFun
+attribute [coe] Divisor.toFun
+
+
+
+noncomputable def Divisor.deg
+  (D : Divisor) : ℤ := ∑ᶠ z, D z
+
+noncomputable def Divisor.n_trunk
+  (D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z)
+
+noncomputable def Divisor.n
+  (D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z
+
+noncomputable def Divisor.N_trunk
+  (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
+
+
+theorem Divisor.support_cap_closed₁
+  {S U : Set ℂ}
+  (hS : DiscreteTopology S)
+  (hU : IsClosed U) :
+  IsClosed (U ∩ S) := by
+
+  rw [← isOpen_compl_iff]
+  rw [isOpen_iff_forall_mem_open]
+  intro x hx
+  by_cases h₁x : x ∈ U
+  · simp at hx
+
+
+    sorry
+  · use Uᶜ
+    constructor
+    · simp
+    · constructor
+      · exact IsClosed.isOpen_compl
+      · assumption
+
+
+
+theorem Divisor.support_cap_closed
+  (D : Divisor)
+  {U : Set ℂ}
+  (h₁U : IsClosed U) :
+  IsClosed (U ∩ D.toFun.support) := by
+  sorry
+
+
+theorem Divisor.support_cap_compact
+  (D : Divisor)
+  {U : Set ℂ}
+  (h₁U : IsCompact U) :
+  Set.Finite (U ∩ (Function.support D)) := by
+
+  apply IsCompact.finite
+  -- Target set is compact
+  apply h₁U.of_isClosed_subset
+  apply D.support_cap_closed h₁U.isClosed
+  exact Set.inter_subset_left
+  -- Target set is discrete
+  apply DiscreteTopology.of_subset D.discreteSupport
+  exact Set.inter_subset_right
+
+
+noncomputable def AnalyticOnNhd.zeroDivisor
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : AnalyticOnNhd ℂ f U) :
+  Divisor where
+
+    toFun := by
+      intro z
+      if hz : z ∈ U then
+        exact ((hf z hz).order.toNat : ℤ)
+      else
+        exact 0
+
+    discreteSupport := by
+      simp_rw [← singletons_open_iff_discrete]
+      simp_rw [Metric.isOpen_singleton_iff]
+      simp
+
+      --  simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq]
+
+      intro a ha ⟨h₁a, h₂a⟩
+      obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a
+      rw [Metric.eventually_nhds_iff_ball] at h₃g
+
+      have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by
+        have h₄g : ContinuousAt g a :=
+          AnalyticAt.continuousAt h₁g
+        have : {0}ᶜ ∈ nhds (g a) := by
+          exact compl_singleton_mem_nhds_iff.mpr h₂g
+        let F := h₄g.preimage_mem_nhds this
+        rw [Metric.mem_nhds_iff] at F
+        obtain ⟨ε, h₁ε, h₂ε⟩ := F
+        use ε
+        constructor; exact h₁ε
+        intro y hy
+        let G := h₂ε hy
+        simp at G
+        exact G
+
+      obtain ⟨ε₁, h₁ε₁⟩ := this
+      obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g
+      use min ε₁ ε₂
+      constructor
+      · have : 0 < min ε₁ ε₂ := by
+          rw [lt_min_iff]
+          exact And.imp_right (fun _ => h₁ε₂) h₁ε₁
+        exact this
+
+      intro y hy ⟨h₁y, h₂y⟩ h₃
+
+      have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by
+        simp
+        calc dist y a
+        _ < min ε₁ ε₂ := by assumption
+        _ ≤ ε₂ := by exact min_le_right ε₁ ε₂
+
+      have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by
+        simp
+        calc dist y a
+        _ < min ε₁ ε₂ := by assumption
+        _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
+
+      have F := h₂ε₂ y h'₂y
+      have : f y = 0 := by
+        rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y
+        tauto
+      rw [this] at F
+      simp at F
+
+      have : g y ≠ 0 := by
+        exact h₁ε₁.2 y h₃y
+      simp [this] at F
+      rw [sub_eq_zero] at F
+      tauto
+
+
+theorem AnalyticOnNhd.support_of_zeroDivisor
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : AnalyticOnNhd ℂ f U) :
+  Function.support hf.zeroDivisor ⊆ U := by
+
+  intro z
+  contrapose
+  intro hz
+  dsimp [AnalyticOnNhd.zeroDivisor]
+  simp
+  tauto
+
+
+theorem AnalyticOnNhd.support_of_zeroDivisor₂
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : AnalyticOnNhd ℂ f U) :
+  Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
+
+  intro z hz
+  dsimp [AnalyticOnNhd.zeroDivisor] at hz
+  have t₀ := hf.support_of_zeroDivisor hz
+  simp [hf.support_of_zeroDivisor hz] at hz
+  let A := hz.1
+  let C := (hf z t₀).order_eq_zero_iff
+  simp
+  rw [C] at A
+  tauto

Nevanlinna/divisor.lean

@@ -3,185 +3,20 @@ import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.Analysis.Convex.SpecificFunctions.Deriv
 import Nevanlinna.analyticAt
 
-open scoped Interval Topology
+open Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
 
-
-
-structure Divisor where
+structure Divisor
+  (U : Set ℂ)
+  where
   toFun : ℂ → ℤ
-  -- This is not what we want. We want: locally finite
-  discreteSupport : DiscreteTopology (Function.support toFun)
+  supportInU : toFun.support ⊆ U
+  locallyFiniteInU : ∀ x ∈ U, ∃  N ∈ 𝓝 x, (N ∩ toFun.support).Finite
+
+instance
+  (U : Set ℂ) :
+  CoeFun (Divisor U) (fun _ ↦ ℂ → ℤ) where
+  coe := Divisor.toFun
 
-instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where
-coe := Divisor.toFun
 attribute [coe] Divisor.toFun
-
-
-
-noncomputable def Divisor.deg
-  (D : Divisor) : ℤ := ∑ᶠ z, D z
-
-noncomputable def Divisor.n_trunk
-  (D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z)
-
-noncomputable def Divisor.n
-  (D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z
-
-noncomputable def Divisor.N_trunk
-  (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t
-
-
-theorem Divisor.support_cap_closed₁
-  {S U : Set ℂ}
-  (hS : DiscreteTopology S)
-  (hU : IsClosed U) :
-  IsClosed (U ∩ S) := by
-
-  rw [← isOpen_compl_iff]
-  rw [isOpen_iff_forall_mem_open]
-  intro x hx
-  by_cases h₁x : x ∈ U
-  · simp at hx
-
-
-    sorry
-  · use Uᶜ
-    constructor
-    · simp
-    · constructor
-      · exact IsClosed.isOpen_compl
-      · assumption
-
-
-
-theorem Divisor.support_cap_closed
-  (D : Divisor)
-  {U : Set ℂ}
-  (h₁U : IsClosed U) :
-  IsClosed (U ∩ D.toFun.support) := by
-  sorry
-
-
-theorem Divisor.support_cap_compact
-  (D : Divisor)
-  {U : Set ℂ}
-  (h₁U : IsCompact U) :
-  Set.Finite (U ∩ (Function.support D)) := by
-
-  apply IsCompact.finite
-  -- Target set is compact
-  apply h₁U.of_isClosed_subset
-  apply D.support_cap_closed h₁U.isClosed
-  exact Set.inter_subset_left
-  -- Target set is discrete
-  apply DiscreteTopology.of_subset D.discreteSupport
-  exact Set.inter_subset_right
-
-
-noncomputable def AnalyticOnNhd.zeroDivisor
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOnNhd ℂ f U) :
-  Divisor where
-
-    toFun := by
-      intro z
-      if hz : z ∈ U then
-        exact ((hf z hz).order.toNat : ℤ)
-      else
-        exact 0
-
-    discreteSupport := by
-      simp_rw [← singletons_open_iff_discrete]
-      simp_rw [Metric.isOpen_singleton_iff]
-      simp
-
-      --  simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq]
-
-      intro a ha ⟨h₁a, h₂a⟩
-      obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a
-      rw [Metric.eventually_nhds_iff_ball] at h₃g
-
-      have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by
-        have h₄g : ContinuousAt g a :=
-          AnalyticAt.continuousAt h₁g
-        have : {0}ᶜ ∈ nhds (g a) := by
-          exact compl_singleton_mem_nhds_iff.mpr h₂g
-        let F := h₄g.preimage_mem_nhds this
-        rw [Metric.mem_nhds_iff] at F
-        obtain ⟨ε, h₁ε, h₂ε⟩ := F
-        use ε
-        constructor; exact h₁ε
-        intro y hy
-        let G := h₂ε hy
-        simp at G
-        exact G
-
-      obtain ⟨ε₁, h₁ε₁⟩ := this
-      obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g
-      use min ε₁ ε₂
-      constructor
-      · have : 0 < min ε₁ ε₂ := by
-          rw [lt_min_iff]
-          exact And.imp_right (fun _ => h₁ε₂) h₁ε₁
-        exact this
-
-      intro y hy ⟨h₁y, h₂y⟩ h₃
-
-      have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by
-        simp
-        calc dist y a
-        _ < min ε₁ ε₂ := by assumption
-        _ ≤ ε₂ := by exact min_le_right ε₁ ε₂
-
-      have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by
-        simp
-        calc dist y a
-        _ < min ε₁ ε₂ := by assumption
-        _ ≤ ε₁ := by exact min_le_left ε₁ ε₂
-
-      have F := h₂ε₂ y h'₂y
-      have : f y = 0 := by
-        rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y
-        tauto
-      rw [this] at F
-      simp at F
-
-      have : g y ≠ 0 := by
-        exact h₁ε₁.2 y h₃y
-      simp [this] at F
-      rw [sub_eq_zero] at F
-      tauto
-
-
-theorem AnalyticOnNhd.support_of_zeroDivisor
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOnNhd ℂ f U) :
-  Function.support hf.zeroDivisor ⊆ U := by
-
-  intro z
-  contrapose
-  intro hz
-  dsimp [AnalyticOnNhd.zeroDivisor]
-  simp
-  tauto
-
-
-theorem AnalyticOnNhd.support_of_zeroDivisor₂
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOnNhd ℂ f U) :
-  Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
-
-  intro z hz
-  dsimp [AnalyticOnNhd.zeroDivisor] at hz
-  have t₀ := hf.support_of_zeroDivisor hz
-  simp [hf.support_of_zeroDivisor hz] at hz
-  let A := hz.1
-  let C := (hf z t₀).order_eq_zero_iff
-  simp
-  rw [C] at A
-  tauto