From 89abb9190f48c3e92aa0aed74a3f49dfb46d2d80 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 14 Nov 2024 13:47:24 +0100 Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/mathlibAddOn.lean | 15 ------ Nevanlinna/meromorphicAt.lean | 72 +++++++++++++++++++++++++++ Nevanlinna/stronglyMeromorphicAt.lean | 57 +++++++++++++++++++++ 3 files changed, 129 insertions(+), 15 deletions(-) diff --git a/Nevanlinna/mathlibAddOn.lean b/Nevanlinna/mathlibAddOn.lean index 0ab0aef..d039589 100644 --- a/Nevanlinna/mathlibAddOn.lean +++ b/Nevanlinna/mathlibAddOn.lean @@ -37,21 +37,6 @@ theorem ContDiff.const_smul' {f : E → F} (c : R) (hf : ContDiff 𝕜 n f) : exact ContDiff.const_smul c hf --- Mathlib.Analysis.Analytic.Meromorphic - -theorem meromorphicAt_congr - {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] - {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] - {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜} - (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x := - ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩ - -theorem meromorphicAt_congr' - {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] - {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] - {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜} - (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x := - meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds) open Topology Filter diff --git a/Nevanlinna/meromorphicAt.lean b/Nevanlinna/meromorphicAt.lean index 1f9d557..942675e 100644 --- a/Nevanlinna/meromorphicAt.lean +++ b/Nevanlinna/meromorphicAt.lean @@ -7,6 +7,22 @@ open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral +theorem meromorphicAt_congr + {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] + {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] + {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜} + (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) : MeromorphicAt f x ↔ MeromorphicAt g x := + ⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩ + + +theorem meromorphicAt_congr' + {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] + {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] + {f : 𝕜 → E} {g : 𝕜 → E} {x : 𝕜} + (h : f =ᶠ[nhds x] g) : MeromorphicAt f x ↔ MeromorphicAt g x := + meromorphicAt_congr (Filter.EventuallyEq.filter_mono h nhdsWithin_le_nhds) + + theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero {f : ℂ → ℂ} {z₀ : ℂ} @@ -53,6 +69,7 @@ theorem MeromorphicAt.eventually_eq_zero_or_eventually_ne_zero · exact h₂N · exact h₃N + theorem MeromorphicAt.order_congr {f₁ f₂ : ℂ → ℂ} {z₀ : ℂ} @@ -73,3 +90,58 @@ theorem MeromorphicAt.order_congr · constructor · assumption · exact EventuallyEq.rw h₃g (fun x => Eq (f₂ x)) (_root_.id (EventuallyEq.symm h)) + + +theorem MeromorphicAt.order_mul + {f₁ f₂ : ℂ → ℂ} + {z₀ : ℂ} + (hf₁ : MeromorphicAt f₁ z₀) + (hf₂ : MeromorphicAt f₂ z₀) : + (hf₁.mul hf₂).order = hf₁.order + hf₂.order := by + by_cases h₂f₁ : hf₁.order = ⊤ + · simp [h₂f₁] + rw [hf₁.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₁ + rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] + obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁ + use t + constructor + · intro y h₁y h₂y + simp; left + rw [h₁t y h₁y h₂y] + · exact ⟨h₂t, h₃t⟩ + · by_cases h₂f₂ : hf₂.order = ⊤ + · simp [h₂f₂] + rw [hf₂.order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] at h₂f₂ + rw [(hf₁.mul hf₂).order_eq_top_iff, eventually_nhdsWithin_iff, eventually_nhds_iff] + obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂ + use t + constructor + · intro y h₁y h₂y + simp; right + rw [h₁t y h₁y h₂y] + · exact ⟨h₂t, h₃t⟩ + · have h₃f₁ := Eq.symm (WithTop.coe_untop hf₁.order h₂f₁) + have h₃f₂ := Eq.symm (WithTop.coe_untop hf₂.order h₂f₂) + obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (hf₁.order_eq_int_iff (hf₁.order.untop h₂f₁)).1 h₃f₁ + obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (hf₂.order_eq_int_iff (hf₂.order.untop h₂f₂)).1 h₃f₂ + rw [h₃f₁, h₃f₂, ← WithTop.coe_add] + rw [MeromorphicAt.order_eq_int_iff] + use g₁ * g₂ + constructor + · exact AnalyticAt.mul h₁g₁ h₁g₂ + · constructor + · simp; tauto + · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₁) + obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 (eventually_nhdsWithin_iff.1 h₃g₂) + rw [eventually_nhdsWithin_iff, eventually_nhds_iff] + use t₁ ∩ t₂ + constructor + · intro y h₁y h₂y + simp + rw [h₁t₁ y h₁y.1 h₂y, h₁t₂ y h₁y.2 h₂y] + simp + rw [zpow_add' (by left; exact sub_ne_zero_of_ne h₂y)] + group + · constructor + · exact IsOpen.inter h₂t₁ h₂t₂ + · exact Set.mem_inter h₃t₁ h₃t₂ diff --git a/Nevanlinna/stronglyMeromorphicAt.lean b/Nevanlinna/stronglyMeromorphicAt.lean index 1a41e1d..7224e3c 100644 --- a/Nevanlinna/stronglyMeromorphicAt.lean +++ b/Nevanlinna/stronglyMeromorphicAt.lean @@ -1,4 +1,5 @@ import Mathlib.Analysis.Analytic.Meromorphic +import Mathlib.Algebra.Order.AddGroupWithTop import Nevanlinna.analyticAt import Nevanlinna.mathlibAddOn import Nevanlinna.meromorphicAt @@ -199,6 +200,8 @@ theorem StronglyMeromorphicAt.localIdentity + + /- Make strongly MeromorphicAt -/ noncomputable def MeromorphicAt.makeStronglyMeromorphicAt {f : ℂ → ℂ} @@ -346,3 +349,57 @@ theorem makeStronglyMeromorphic_id tauto · exact m₁ (StronglyMeromorphicAt.meromorphicAt hf) z hz + + +theorem StronglyMeromorphicAt.decompose + {f : ℂ → ℂ} + {z₀ : ℂ} + (h₁f : StronglyMeromorphicAt f z₀) + (h₂f : h₁f.meromorphicAt.order ≠ ⊤) : + ∃ g : ℂ → ℂ, (AnalyticAt ℂ g z₀) + ∧ (g z₀ ≠ 0) + ∧ (f = (fun z ↦ (z-z₀) ^ (h₁f.meromorphicAt.order.untop h₂f)) * g) := by + + let n := - h₁f.meromorphicAt.order.untop h₂f + + let g₁ := (fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f)) * f + let g₁₁ := fun z ↦ (z-z₀) ^ (-h₁f.meromorphicAt.order.untop h₂f) + have h₁g₁₁ : MeromorphicAt g₁₁ z₀ := by + apply MeromorphicAt.zpow + apply AnalyticAt.meromorphicAt + apply AnalyticAt.sub + apply analyticAt_id + exact analyticAt_const + have h₂g₁₁ : h₁g₁₁.order = - h₁f.meromorphicAt.order.untop h₂f := by + rw [← WithTop.LinearOrderedAddCommGroup.coe_neg] + rw [h₁g₁₁.order_eq_int_iff] + use 1 + constructor + · exact analyticAt_const + · constructor + · simp + · apply eventually_nhdsWithin_of_forall + simp [g₁₁] + have h₁g₁ : MeromorphicAt g₁ z₀ := h₁g₁₁.mul h₁f.meromorphicAt + have h₂g₁ : h₁g₁.order = 0 := by + rw [h₁g₁₁.order_mul h₁f.meromorphicAt] + rw [h₂g₁₁] + simp + rw [add_comm] + rw [LinearOrderedAddCommGroupWithTop.add_neg_cancel_of_ne_top h₂f] + let g := h₁g₁.makeStronglyMeromorphicAt + use g + have h₁g : StronglyMeromorphicAt g z₀ := by + exact StronglyMeromorphicAt_of_makeStronglyMeromorphic h₁g₁ + have h₂g : h₁g.meromorphicAt.order = 0 := by + + + + sorry + constructor + · apply analytic + · sorry + · exact h₁g + · constructor + · sorry + · sorry