Nevanlinna/analyticAt.lean

@@ -3,18 +3,6 @@ import Mathlib.Analysis.Complex.Basic
 import Mathlib.Analysis.Analytic.Linear
 
 
-theorem AnalyticAt.order_neq_top_iff
-  {f : ℂ → ℂ}
-  {z₀ : ℂ}
-  (hf : AnalyticAt ℂ f z₀) :
-  hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhds z₀, f z = (z - z₀) ^ (hf.order.toNat) • g z := by
-  rw [← hf.order_eq_nat_iff]
-  constructor
-  · intro h₁f
-    exact Eq.symm (ENat.coe_toNat h₁f)
-  · intro h₁f
-    exact ENat.coe_toNat_eq_self.mp (id (Eq.symm h₁f))
-
 
 theorem AnalyticAt.order_mul
   {f₁ f₂ : ℂ → ℂ}

Nevanlinna/divisor.lean

@@ -1,139 +0,0 @@
-import Nevanlinna.analyticAt
-
-
-structure Divisor where
-  toFun : ℂ → ℤ
-  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.compactSupport
-  (D : Divisor)
-  {U : Set ℂ}
-  (h₁U : IsCompact U)
-  (h₂U : Function.support D ⊆ U) :
-  Set.Finite (Function.support D) := by
-  sorry
-
-
-noncomputable def AnalyticOn.zeroDivisor
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ 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 AnalyticOn.support_of_zeroDivisor
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
-  Function.support hf.zeroDivisor ⊆ U := by
-
-  intro z
-  contrapose
-  intro hz
-  dsimp [AnalyticOn.zeroDivisor]
-  simp
-  tauto
-
-
-theorem AnalyticOn.support_of_zeroDivisor₂
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (hf : AnalyticOn ℂ f U) :
-  Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by
-
-  intro z hz
-  dsimp [AnalyticOn.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/firstMain.lean

@@ -1,19 +1,15 @@
-import Mathlib.Analysis.Analytic.Meromorphic
 import Nevanlinna.holomorphic_JensenFormula
 
 open Real
 
-variable (f : ℂ → ℂ)
+variable {f : ℂ → ℂ}
-variable {h₁f : MeromorphicOn f ⊤}
+variable {h₁f : AnalyticOn ℂ f ⊤}
 variable {h₂f : f 0 ≠ 0}
 
-
+noncomputable def unintegratedCounting : ℝ → ℕ := by
-
-noncomputable def Nevanlinna.n : ℝ → ℤ := by
   intro r
-  have : MeromorphicAt f z := by
+  let A := h₁f.mono (by tauto : Metric.closedBall (0 : ℂ) r ⊆ ⊤)
-    exact h₁f (sorryAx ℂ true) trivial
+  exact ∑ᶠ z, (A.order z).toNat
-  exact ∑ᶠ z ∈ Metric.ball (0 : ℂ) r, (h₁f z trivial).order
 
 noncomputable def integratedCounting : ℝ → ℝ := by
   intro r