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
import Mathlib.MeasureTheory.Integral.IntervalIntegral



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 d
  {U S : Set ℂ}
  {r : ℝ}
  (hU : Metric.sphere 0 |r| ⊆ U)
  (hS : S ∈ Filter.codiscreteWithin U) :
  Countable ((circleMap 0 r)⁻¹' (S ∪ Uᶜ)ᶜ) := by

  have : (circleMap 0 r)⁻¹' U = ⊤ := by
    simpa
  simp [this]



  sorry


theorem integrability_congr_changeDiscrete₀
  {f₁ f₂ : ℂ → ℂ}
  {U : Set ℂ}
  {r : ℝ}
  (hU : Metric.sphere 0 |r| ⊆ U)
  (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₁

  by_cases hr : r = 0
  · unfold circleMap
    rw [hr]
    simp
    have : f₂ ∘ (fun (θ : ℝ) ↦ 0) = (fun r ↦ f₂ 0) := by
      exact rfl
    rw [this]
    simp

  · 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
      let A := c {z | f₁ z = f₂ z} U hf
      simp at A
      simpa
      exact hr
    · intro x hx
      simp at hx
      simp
      rcases hx with h|h
      · assumption
      · let A := hU (circleMap_mem_sphere' 0 r x)
        tauto

theorem integrability_congr_changeDiscrete
  {f₁ f₂ : ℂ → ℂ}
  {U : Set ℂ}
  {r : ℝ}
  (hU : Metric.sphere 0 |r| ⊆ U)
  (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

  constructor
  · exact integrability_congr_changeDiscrete₀ hU hf
  · exact integrability_congr_changeDiscrete₀ hU (EventuallyEq.symm hf)


theorem integral_congr_changeDiscrete
  {f₁ f₂ : ℂ → ℂ}
  {U : Set ℂ}
  {r : ℝ}
  (hU : Metric.sphere 0 |r| ⊆ U)
  (hf : f₁ =ᶠ[Filter.codiscreteWithin U] f₂) :
  ∫ (x : ℝ) in (0)..(2 * π), f₁ (circleMap 0 r x) = ∫ (x : ℝ) in (0)..(2 * π), f₂ (circleMap 0 r x) := by

  apply intervalIntegral.integral_congr_ae
  rw [eventually_iff_exists_mem]
  use (circleMap 0 r)⁻¹' ({z | f₁ z = f₂ z} ∪ Uᶜ)


  sorry