From 1c02007e1eff33a645cc6a160914fa98027c91a9 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 13 Dec 2024 16:03:00 +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/meromorphicOn_integrability.lean | 90 ++++++------------- .../stronglyMeromorphicOn_eliminate.lean | 59 ++++++++++++ .../stronglyMeromorphic_JensenFormula.lean | 39 ++++++++ 3 files changed, 126 insertions(+), 62 deletions(-) diff --git a/Nevanlinna/meromorphicOn_integrability.lean b/Nevanlinna/meromorphicOn_integrability.lean index 628726b..4d07d91 100644 --- a/Nevanlinna/meromorphicOn_integrability.lean +++ b/Nevanlinna/meromorphicOn_integrability.lean @@ -1,64 +1,42 @@ import Mathlib.Analysis.Analytic.Meromorphic +import Mathlib.MeasureTheory.Integral.CircleIntegral +import Mathlib.MeasureTheory.Integral.IntervalIntegral 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 ℂ} + {c : ℂ} {r : ℝ} - (hU : Metric.sphere 0 |r| ⊆ U) + (hr : r ≠ 0) + (hU : Metric.sphere c |r| ⊆ U) (hS : S ∈ Filter.codiscreteWithin U) : - Countable ((circleMap 0 r)⁻¹' (S ∪ Uᶜ)ᶜ) := by + Countable ((circleMap c r)⁻¹' Sᶜ) := by - have : (circleMap 0 r)⁻¹' U = ⊤ := by - simpa - simp [this] + have : (circleMap c r)⁻¹' (S ∪ Uᶜ)ᶜ = (circleMap c r)⁻¹' Sᶜ := by + simp [(by simpa : (circleMap c r)⁻¹' U = ⊤)] + rw [← this] + apply Set.Countable.preimage_circleMap _ c hr + have : DiscreteTopology ((S ∪ Uᶜ)ᶜ : Set ℂ) := by + rw [discreteTopology_subtype_iff] + rw [mem_codiscreteWithin] at hS; simp at hS + intro x hx + rw [← mem_iff_inf_principal_compl, (by ext z; simp; tauto : S ∪ Uᶜ = (U \ S)ᶜ)] + rw [Set.compl_union, compl_compl] at hx + exact hS x hx.2 - sorry + apply TopologicalSpace.separableSpace_iff_countable.1 + exact TopologicalSpace.SecondCountableTopology.to_separableSpace theorem integrability_congr_changeDiscrete₀ @@ -81,24 +59,11 @@ theorem integrability_congr_changeDiscrete₀ · apply IntervalIntegrable.congr hf₁ rw [Filter.eventuallyEq_iff_exists_mem] - use (circleMap 0 r)⁻¹' ({z | f₁ z = f₂ z} ∪ Uᶜ) + use (circleMap 0 r)⁻¹' {z | f₁ z = f₂ z} 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 + · apply Set.Countable.measure_zero (d hr hU hf) + · tauto + theorem integrability_congr_changeDiscrete {f₁ f₂ : ℂ → ℂ} @@ -117,13 +82,14 @@ theorem integral_congr_changeDiscrete {f₁ f₂ : ℂ → ℂ} {U : Set ℂ} {r : ℝ} + (hr : r ≠ 0) (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 + use (circleMap 0 r)⁻¹' {z | f₁ z = f₂ z} + constructor + · apply Set.Countable.measure_zero (d hr hU hf) + · tauto diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean index 4e04751..c45bbcb 100644 --- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean +++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean @@ -490,3 +490,62 @@ theorem MeromorphicOn.decompose₃' rw [sub_eq_zero] at H rw [H] at this tauto + + + +theorem MeromorphicOn.decompose_log + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsCompact U) + (h₂U : IsConnected U) + (h₁f : StronglyMeromorphicOn f U) + (h₂f : ∃ u : U, f u ≠ 0) : + ∃ g : ℂ → ℂ, (MeromorphicOn g U) + ∧ (AnalyticOnNhd ℂ g U) + ∧ (∀ u : U, g u ≠ 0) + ∧ (fun z ↦ log ‖f z‖) =ᶠ[Filter.codiscreteWithin U] fun z ↦ log ‖g z‖ + ∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log ‖z - s‖ := by + + have h₃f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by + exact Divisor.finiteSupport h₁U (StronglyMeromorphicOn.meromorphicOn h₁f).divisor + + have hSupp₁ {z : ℂ} : (fun s ↦ (h₁f.meromorphicOn.divisor s) * log ‖z - s‖).support ⊆ h₃f.toFinset := by + intro x + contrapose + simp; tauto + simp_rw [finsum_eq_sum_of_support_subset _ hSupp₁] + + obtain ⟨g, h₁g, h₂g, h₃g, h₄g⟩ := MeromorphicOn.decompose₃' h₁U h₂U h₁f h₂f + have hSupp₂ {z : ℂ} : ( fun (u : ℂ) ↦ (fun (z : ℂ) ↦ (z - u) ^ (h₁f.meromorphicOn.divisor u)) ).mulSupport ⊆ h₃f.toFinset := by + intro x + contrapose + simp + intro hx + rw [hx] + simp; tauto + rw [finprod_eq_prod_of_mulSupport_subset _ hSupp₂] at h₄g + + use g + simp only [h₁g, h₂g, h₃g, ne_eq, true_and, not_false_eq_true, implies_true] + rw [Filter.eventuallyEq_iff_exists_mem] + use {z | f z ≠ 0} + constructor + · sorry + · intro z hz + nth_rw 1 [h₄g] + simp + rw [log_mul, log_prod] + congr + ext u + rw [log_zpow] + intro x hx + simp at hx + simp + apply zpow_ne_zero + simp + simp at hz + contrapose + simp + + + repeat + sorry diff --git a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean index 8023bf4..9d4c52e 100644 --- a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean +++ b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean @@ -3,6 +3,45 @@ import Nevanlinna.stronglyMeromorphicOn_eliminate open Real +lemma jensen₀ + {R : ℝ} + (hR : 0 < R) + (f : ℂ → ℂ) + (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 R)) + (h₂f : f 0 ≠ 0) : + ∃ F : ℂ → ℂ, + AnalyticOnNhd ℂ F (Metric.closedBall (0 : ℂ) R) + ∧ (∀ (u : (Metric.closedBall (0 : ℂ) R)), F u ≠ 0) + ∧ (fun z ↦ log ‖f z‖) =ᶠ[Filter.codiscreteWithin (Metric.closedBall (0 : ℂ) R)] (fun z ↦ log ‖F z‖ + ∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log ‖z - s‖) := by + + have h₁U : IsConnected (Metric.closedBall (0 : ℂ) R) := by + constructor + · apply Metric.nonempty_closedBall.mpr + exact le_of_lt hR + · exact (convex_closedBall (0 : ℂ) R).isPreconnected + + have h₂U : IsCompact (Metric.closedBall (0 : ℂ) R) := isCompact_closedBall (0 : ℂ) R + + + obtain ⟨F, h₁F, h₂F, h₃F, h₄F⟩ := MeromorphicOn.decompose₃' h₂U h₁U h₁f (by use ⟨0, Metric.mem_closedBall_self (le_of_lt hR)⟩) + + use F + constructor + · exact h₂F + · constructor + · exact fun u ↦ h₃F u + · rw [Filter.eventuallyEq_iff_exists_mem] + use {z | f z ≠ 0} + constructor + · sorry + · intro z hz + simp at hz + nth_rw 1 [h₄F] + simp only [Pi.mul_apply, norm_mul] + + + sorry + theorem jensen {R : ℝ}