From dfc67cec4a202ee9e7fb5f9af6e6b7e9c42cdd5a Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 7 Nov 2024 12:08:52 +0100 Subject: [PATCH] working --- Nevanlinna/meromorphicOn_decompose.lean | 23 +++++++++++++++++++++++ Nevanlinna/stronglyMeromorphicAt.lean | 6 +++--- 2 files changed, 26 insertions(+), 3 deletions(-) create mode 100644 Nevanlinna/meromorphicOn_decompose.lean diff --git a/Nevanlinna/meromorphicOn_decompose.lean b/Nevanlinna/meromorphicOn_decompose.lean new file mode 100644 index 0000000..ceb2ba4 --- /dev/null +++ b/Nevanlinna/meromorphicOn_decompose.lean @@ -0,0 +1,23 @@ +import Mathlib.Analysis.Analytic.Meromorphic +import Nevanlinna.analyticAt +import Nevanlinna.divisor +import Nevanlinna.meromorphicAt +import Nevanlinna.meromorphicOn_divisor +import Nevanlinna.stronglyMeromorphicOn + + +open scoped Interval Topology +open Real Filter MeasureTheory intervalIntegral + + +theorem MeromorphicOn.decompose + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsConnected U) + (h₂U : IsCompact U) + (h₁f : MeromorphicOn f U) + (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) : + ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U) + ∧ (∀ z ∈ U, g z ≠ 0) + ∧ (Set.EqOn h₁f.makeStronglyMeromorphicOn (fun z ↦ ∏ᶠ p ∈ h₁f.divisor.support, (z-p) ) U) := by + sorry diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean index ccfdb36..4f24a1a 100644 --- a/Nevanlinna/stronglyMeromorphicAt.lean +++ b/Nevanlinna/stronglyMeromorphicAt.lean @@ -155,7 +155,7 @@ lemma m₂ apply eventually_nhdsWithin_of_forall exact fun x a => m₁ hf x a - +/- lemma Mnhds {f g : ℂ → ℂ} {z₀ : ℂ} @@ -172,7 +172,7 @@ lemma Mnhds · simp at h₂y rwa [h₂y] · exact h₂t - +-/ theorem localIdentity {f g : ℂ → ℂ} @@ -262,7 +262,7 @@ theorem makeStronglyMeromorphic_id · rw [hz] unfold MeromorphicAt.makeStronglyMeromorphicAt simp - let h₀f := hf + have h₀f := hf rcases hf with h₁f|h₁f · have A : f =ᶠ[𝓝[≠] z₀] 0 := by apply Filter.EventuallyEq.filter_mono h₁f