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 a
  (S : Set ℂ)
  (hS : S ∈ Filter.codiscreteWithin ⊤) :
  DiscreteTopology (Sᶜ : Set ℂ) := by

  rw [mem_codiscreteWithin] at hS
  simp at hS
  have : (Set.univ \ S)ᶜ = S := by ext z; simp
  rw [this] at hS

  rw [discreteTopology_subtype_iff]
  intro x hx
  rw [← mem_iff_inf_principal_compl]
  exact (hS x)


theorem integrability_congr_changeDiscrete
  {f₁ f₂ : ℂ → ℂ}
  {r : ℝ}
  (hf : f₁ =ᶠ[Filter.codiscreteWithin ⊤] 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}
  constructor
  · apply Set.Countable.measure_zero
    have : (circleMap 0 r ⁻¹' {z | f₁ z = f₂ z})ᶜ = (circleMap 0 r ⁻¹' {z | f₁ z = f₂ z}ᶜ) := by
      exact rfl
    rw [this]
    apply Set.Countable.preimage_circleMap

    sorry
    sorry
  · sorry