Working…

Nevanlinna/meromorphicOn_integrability.lean

@@ -0,0 +1,33 @@
+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
+
+
+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

Nevanlinna/stronglyMeromorphicOn.lean

@@ -4,6 +4,22 @@ import Mathlib.Algebra.BigOperators.Finprod
 open Topology
 
 
+
+theorem MeromorphicOn.analyticOnCodiscreteWithin
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  { x | AnalyticAt ℂ f x } ∈ Filter.codiscreteWithin U := by
+
+  rw [mem_codiscreteWithin]
+  intro x hx
+  simp
+  rw [← Filter.eventually_mem_set]
+  apply Filter.Eventually.mono (hf x hx).eventually_analyticAt
+  simp
+  tauto
+
+
 /- Strongly MeromorphicOn -/
 def StronglyMeromorphicOn
   (f : ℂ → ℂ)
@@ -106,6 +122,25 @@ theorem makeStronglyMeromorphicOn_changeDiscrete'
     simp [hz₀]
 
 
+theorem makeStronglyMeromorphicOn_changeDiscrete''
+  {f : ℂ → ℂ}
+  {U : Set ℂ}
+  (hf : MeromorphicOn f U) :
+  f =ᶠ[Filter.codiscreteWithin U] hf.makeStronglyMeromorphicOn := by
+
+  rw [Filter.eventuallyEq_iff_exists_mem]
+  use { x | AnalyticAt ℂ f x }
+  constructor
+  · exact MeromorphicOn.analyticOnCodiscreteWithin hf
+  · intro x hx
+    simp at hx
+    rw [MeromorphicOn.makeStronglyMeromorphicOn]
+    by_cases h₁x : x ∈ U
+    · simp [h₁x]
+      rw [← StronglyMeromorphicAt.makeStronglyMeromorphic_id hx.stronglyMeromorphicAt]
+    · simp [h₁x]
+
+
 theorem stronglyMeromorphicOn_of_makeStronglyMeromorphicOn
   {f : ℂ → ℂ}
   {U : Set ℂ}