From 309724de369f696fb1b93e6927549a2cb23ffb66 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 16 Dec 2024 17:17:43 +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/codiscreteWithin.lean | 11 +++ Nevanlinna/meromorphicOn.lean | 83 ++++++++++++++----- Nevanlinna/meromorphicOn_divisor.lean | 8 +- Nevanlinna/meromorphicOn_integrability.lean | 34 +++++++- .../stronglyMeromorphicOn_eliminate.lean | 62 ++++++++++++-- 5 files changed, 163 insertions(+), 35 deletions(-) create mode 100644 Nevanlinna/codiscreteWithin.lean diff --git a/Nevanlinna/codiscreteWithin.lean b/Nevanlinna/codiscreteWithin.lean new file mode 100644 index 0000000..395e61f --- /dev/null +++ b/Nevanlinna/codiscreteWithin.lean @@ -0,0 +1,11 @@ +import Mathlib.Topology.DiscreteSubset + +theorem codiscreteWithin_congr + {X : Type u_1} [TopologicalSpace X] + {S T U : Set X} + (hST : S ∩ U = T ∩ U) : + S ∈ Filter.codiscreteWithin U ↔ T ∈ Filter.codiscreteWithin U := by + repeat rw [mem_codiscreteWithin] + rw [← Set.diff_inter_self_eq_diff (t := S)] + rw [← Set.diff_inter_self_eq_diff (t := T)] + rw [hST] diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean index fe5e141..3455ecb 100644 --- a/Nevanlinna/meromorphicOn.lean +++ b/Nevanlinna/meromorphicOn.lean @@ -107,40 +107,79 @@ theorem MeromorphicOn.clopen_of_order_eq_top theorem MeromorphicOn.order_ne_top' {f : ℂ → ℂ} {U : Set ℂ} - (hU : IsConnected U) (h₁f : MeromorphicOn f U) - (h₂f : ∃ u : U, (h₁f u u.2).order ≠ ⊤) : - ∀ u : U, (h₁f u u.2).order ≠ ⊤ := by + (hU : IsConnected U) : + (∃ u : U, (h₁f u u.2).order ≠ ⊤) ↔ (∀ u : U, (h₁f u u.2).order ≠ ⊤) := by - let A := h₁f.clopen_of_order_eq_top - have : PreconnectedSpace U := by - apply isPreconnected_iff_preconnectedSpace.mp - exact IsConnected.isPreconnected hU - rw [isClopen_iff] at A - rcases A with h|h - · intro u - have : u ∉ (∅ : Set U) := by exact fun a => a - rw [← h] at this - simp at this - tauto - · obtain ⟨u, hU⟩ := h₂f - have A : u ∈ Set.univ := by trivial - rw [← h] at A - simp at A - tauto + constructor + · intro h₂f + let A := h₁f.clopen_of_order_eq_top + have : PreconnectedSpace U := by + apply isPreconnected_iff_preconnectedSpace.mp + exact IsConnected.isPreconnected hU + rw [isClopen_iff] at A + rcases A with h|h + · intro u + have : u ∉ (∅ : Set U) := by exact fun a => a + rw [← h] at this + simp at this + tauto + · obtain ⟨u, hU⟩ := h₂f + have A : u ∈ Set.univ := by trivial + rw [← h] at A + simp at A + tauto + · intro h₂f + let A := hU.nonempty + obtain ⟨v, hv⟩ := A + use ⟨v, hv⟩ + exact h₂f ⟨v, hv⟩ -theorem MeromorphicOn.order_ne_top +theorem StronglyMeromorphicOn.order_ne_top {f : ℂ → ℂ} {U : Set ℂ} - (hU : IsConnected U) (h₁f : StronglyMeromorphicOn f U) + (hU : IsConnected U) (h₂f : ∃ u : U, f u ≠ 0) : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by - apply MeromorphicOn.order_ne_top' hU h₁f.meromorphicOn + rw [← h₁f.meromorphicOn.order_ne_top' hU] obtain ⟨u, hu⟩ := h₂f use u rw [← (h₁f u u.2).order_eq_zero_iff] at hu rw [hu] simp + + +theorem MeromorphicOn.nonvanish_of_order_ne_top + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁f : MeromorphicOn f U) + (h₂f : ∃ u : U, (h₁f u u.2).order ≠ ⊤) + (h₁U : IsConnected U) + (h₂U : interior U ≠ ∅) : + ∃ u ∈ U, f u ≠ 0 := by + + by_contra hCon + push_neg at hCon + + have : ∃ u : U, (h₁f u u.2).order = ⊤ := by + obtain ⟨v, h₁v⟩ := Set.nonempty_iff_ne_empty'.2 h₂U + have h₂v : v ∈ U := by apply interior_subset h₁v + use ⟨v, h₂v⟩ + rw [MeromorphicAt.order_eq_top_iff] + rw [eventually_nhdsWithin_iff] + rw [eventually_nhds_iff] + use interior U + constructor + · intro y h₁y h₂y + exact hCon y (interior_subset h₁y) + · simp [h₁v] + + let A := h₁f.order_ne_top' h₁U + rw [← not_iff_not] at A + push_neg at A + have B := A.2 this + obtain ⟨u, hu⟩ := h₂f + tauto diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean index 94353f4..671e90f 100644 --- a/Nevanlinna/meromorphicOn_divisor.lean +++ b/Nevanlinna/meromorphicOn_divisor.lean @@ -163,6 +163,8 @@ theorem MeromorphicOn.divisor_of_makeStronglyMeromorphicOn +-- STRONGLY MEROMORPHIC THINGS + /- Strongly MeromorphicOn of non-negative order is analytic -/ theorem StronglyMeromorphicOn.analyticOnNhd {f : ℂ → ℂ} @@ -188,16 +190,16 @@ theorem StronglyMeromorphicOn.analyticOnNhd theorem StronglyMeromorphicOn.support_divisor {f : ℂ → ℂ} {U : Set ℂ} - (hU : IsConnected U) (h₁f : StronglyMeromorphicOn f U) - (h₂f : ∃ u : U, f u ≠ 0) : + (h₂f : ∃ u : U, f u ≠ 0) + (hU : IsConnected U) : U ∩ f⁻¹' {0} = (Function.support h₁f.meromorphicOn.divisor) := by ext u constructor · intro hu unfold MeromorphicOn.divisor - simp [MeromorphicOn.order_ne_top hU h₁f h₂f ⟨u, hu.1⟩] + simp [h₁f.order_ne_top hU h₂f ⟨u, hu.1⟩] use hu.1 rw [(h₁f u hu.1).order_eq_zero_iff] simp diff --git a/Nevanlinna/meromorphicOn_integrability.lean b/Nevanlinna/meromorphicOn_integrability.lean index 0be7e59..c43bf23 100644 --- a/Nevanlinna/meromorphicOn_integrability.lean +++ b/Nevanlinna/meromorphicOn_integrability.lean @@ -6,6 +6,7 @@ import Nevanlinna.divisor import Nevanlinna.meromorphicAt import Nevanlinna.meromorphicOn_divisor import Nevanlinna.stronglyMeromorphicOn +import Nevanlinna.stronglyMeromorphicOn_eliminate import Nevanlinna.mathlibAddOn open scoped Interval Topology @@ -42,7 +43,7 @@ theorem d theorem integrability_congr_changeDiscrete₀ - {f₁ f₂ : ℂ → ℂ} + {f₁ f₂ : ℂ → ℝ} {U : Set ℂ} {r : ℝ} (hU : Metric.sphere 0 |r| ⊆ U) @@ -68,10 +69,10 @@ theorem integrability_congr_changeDiscrete₀ theorem integrability_congr_changeDiscrete - {f₁ f₂ : ℂ → ℂ} + {f₁ f₂ : ℂ → ℝ} {U : Set ℂ} {r : ℝ} - (hU : Metric.sphere 0 |r| ⊆ U) + (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 @@ -81,7 +82,7 @@ theorem integrability_congr_changeDiscrete theorem integral_congr_changeDiscrete - {f₁ f₂ : ℂ → ℂ} + {f₁ f₂ : ℂ → ℝ} {U : Set ℂ} {r : ℝ} (hr : r ≠ 0) @@ -95,3 +96,28 @@ theorem integral_congr_changeDiscrete constructor · apply Set.Countable.measure_zero (d hr hU hf) · tauto + + +theorem MeromorphicOn.integrable_log_abs_f + {f : ℂ → ℂ} + {r : ℝ} + (hr : 0 < r) + (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) r)) + (h₂f : ∃ u : (Metric.closedBall (0 : ℂ) r), (h₁f u u.2).order ≠ ⊤) : + IntervalIntegrable (fun z ↦ log ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by + + have h₁U : IsCompact (Metric.closedBall (0 : ℂ) r) := by sorry + have h₂U : IsConnected (Metric.closedBall (0 : ℂ) r) := by sorry + have h₃U : interior (Metric.closedBall (0 : ℂ) r) ≠ ∅ := by sorry + + obtain ⟨g, h₁g, h₂g, h₃g⟩ := MeromorphicOn.decompose_log h₁U h₂U h₃U h₁f h₂f + have : (fun z ↦ log ‖f (circleMap 0 r z)‖) = (fun z ↦ log ‖f z‖) ∘ (circleMap 0 r) := by + rfl + rw [this] + have : Metric.sphere (0 : ℂ) |r| ⊆ Metric.closedBall (0 : ℂ) r := by + sorry + rw [integrability_congr_changeDiscrete this h₃g] + + apply IntervalIntegrable.add + sorry + sorry diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean index 7b29890..16a23c0 100644 --- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean +++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean @@ -1,5 +1,6 @@ import Mathlib.Analysis.Analytic.Meromorphic import Nevanlinna.analyticAt +import Nevanlinna.codiscreteWithin import Nevanlinna.divisor import Nevanlinna.meromorphicAt import Nevanlinna.meromorphicOn @@ -293,7 +294,6 @@ theorem MeromorphicOn.decompose₂ simpa - theorem MeromorphicOn.decompose₃' {f : ℂ → ℂ} {U : Set ℂ} @@ -306,7 +306,8 @@ theorem MeromorphicOn.decompose₃' ∧ (∀ u : U, g u ≠ 0) ∧ (f = g * ∏ᶠ u, fun z ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) := by - have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := MeromorphicOn.order_ne_top h₂U h₁f h₂f + have h₃f : ∀ u : U, (h₁f u u.2).meromorphicAt.order ≠ ⊤ := + StronglyMeromorphicOn.order_ne_top h₁f h₂U h₂f have h₄f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := h₁f.meromorphicOn.divisor.finiteSupport h₁U let d := - h₁f.meromorphicOn.divisor.toFun @@ -492,8 +493,7 @@ theorem MeromorphicOn.decompose₃' tauto - -theorem MeromorphicOn.decompose_log +theorem StronglyMeromorphicOn.decompose_log {f : ℂ → ℂ} {U : Set ℂ} (h₁U : IsCompact U) @@ -529,8 +529,15 @@ theorem MeromorphicOn.decompose_log rw [Filter.eventuallyEq_iff_exists_mem] use {z | f z ≠ 0} constructor - · - sorry + · have A := h₁f.meromorphicOn.divisor.codiscreteWithin + have : {z | f z ≠ 0} ∩ U = (Function.support h₁f.meromorphicOn.divisor)ᶜ ∩ U := by + rw [← h₁f.support_divisor h₂f h₂U] + ext u + simp; tauto + + rw [codiscreteWithin_congr this] + exact A + · intro z hz nth_rw 1 [h₄g] simp @@ -588,3 +595,46 @@ theorem MeromorphicOn.decompose_log let c := b.1 simp_rw [hCon] at c tauto + + exact 0 + + +theorem MeromorphicOn.decompose_log + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsCompact U) + (h₂U : IsConnected U) + (h₃U : interior U ≠ ∅) + (h₁f : MeromorphicOn f U) + (h₂f : ∃ u : U, (h₁f u u.2).order ≠ ⊤) : + ∃ g : ℂ → ℂ, (AnalyticOnNhd ℂ g U) + ∧ (∀ u : U, g u ≠ 0) + ∧ (fun z ↦ log ‖f z‖) =ᶠ[Filter.codiscreteWithin U] fun z ↦ log ‖g z‖ + ∑ᶠ s, (h₁f.divisor s) * log ‖z - s‖ := by + + let F := h₁f.makeStronglyMeromorphicOn + have h₁F := stronglyMeromorphicOn_of_makeStronglyMeromorphicOn h₁f + have h₂F : ∃ u : U, (h₁F.meromorphicOn u u.2).order ≠ ⊤ := by + obtain ⟨u, hu⟩ := h₂f + use u + rw [makeStronglyMeromorphicOn_changeOrder h₁f u.2] + assumption + + have t₁ : ∃ u : U, F u ≠ 0 := by + let A := h₁F.meromorphicOn.nonvanish_of_order_ne_top h₂F h₂U h₃U + tauto + have t₃ : (fun z ↦ log ‖f z‖) =ᶠ[Filter.codiscreteWithin U] (fun z ↦ log ‖F z‖) := by + -- This would be interesting for a tactic + rw [eventuallyEq_iff_exists_mem] + obtain ⟨s, h₁s, h₂s⟩ := eventuallyEq_iff_exists_mem.1 (makeStronglyMeromorphicOn_changeDiscrete'' h₁f) + use s + tauto + + obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := h₁F.decompose_log h₁U h₂U t₁ + use g + constructor + · exact h₂g + · constructor + · exact h₃g + · apply t₃.trans + rw [h₁f.divisor_of_makeStronglyMeromorphicOn] + exact h₄g