nevanlinna/Nevanlinna/meromorphicOn_integrability.lean

import Mathlib.Analysis.Analytic.Meromorphic
import Nevanlinna.analyticAt
import Nevanlinna.divisor
import Nevanlinna.meromorphicAt
import Nevanlinna.meromorphicOn_divisor
import Nevanlinna.stronglyMeromorphicOn
import Nevanlinna.mathlibAddOn
import Mathlib.MeasureTheory.Integral.CircleIntegral


open scoped Interval Topology
open Real Filter MeasureTheory intervalIntegral


lemma b
  (S U : Set ℂ)
  (hS : S ∈ Filter.codiscreteWithin U) :
  DiscreteTopology ((S ∪ Uᶜ)ᶜ : Set ℂ) := by

  rw [mem_codiscreteWithin] at hS
  simp at hS
  have : (U \ S)ᶜ = S ∪ Uᶜ := by
    ext z
    simp
    tauto

  rw [discreteTopology_subtype_iff]
  intro x hx
  rw [← mem_iff_inf_principal_compl]

  simp at hx
  let A := hS x hx.2
  rw [← this]
  assumption


lemma c
  (S U : Set ℂ)
  (hS : S ∈ Filter.codiscreteWithin U) :
  Countable ((S ∪ Uᶜ)ᶜ : Set ℂ) := by
  let A := b S U hS
  apply TopologicalSpace.separableSpace_iff_countable.1
  exact TopologicalSpace.SecondCountableTopology.to_separableSpace


theorem integrability_congr_changeDiscrete
  {f₁ f₂ : ℂ → ℂ}
  {U : Set ℂ}
  {r : ℝ}
  (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
  intro hf₁

  apply IntervalIntegrable.congr hf₁
  rw [Filter.eventuallyEq_iff_exists_mem]
  use (circleMap 0 r)⁻¹' ({z | f₁ z = f₂ z} ∩ U)
  constructor
  · apply Set.Countable.measure_zero
    have : (circleMap 0 r ⁻¹' ({z | f₁ z = f₂ z} ∩ U))ᶜ = (circleMap 0 r ⁻¹' ({z | f₁ z = f₂ z} ∩ U)ᶜ) := by
      exact rfl
    rw [this]
    apply Set.Countable.preimage_circleMap
    apply c
    sorry
    sorry
  · intro x hx
    simp at hx
    simp
    exact hx.1