nevanlinna/Nevanlinna/divisor.lean

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