From 6e9cb9e62be33d62eba60783d43c41741ed015a8 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 20 Dec 2024 08:16:22 +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/firstMain.lean | 101 +++++++++++++------- Nevanlinna/meromorphicAt.lean | 70 ++++++++++++++ Nevanlinna/meromorphicOn_divisor.lean | 23 +++++ Nevanlinna/meromorphicOn_integrability.lean | 14 +-- 4 files changed, 166 insertions(+), 42 deletions(-) diff --git a/Nevanlinna/firstMain.lean b/Nevanlinna/firstMain.lean index 202482a..a441d8f 100644 --- a/Nevanlinna/firstMain.lean +++ b/Nevanlinna/firstMain.lean @@ -16,6 +16,15 @@ theorem MeromorphicOn.restrict MeromorphicOn f (Metric.closedBall 0 r) := by exact fun x a => h₁f x trivial +theorem MeromorphicOn.restrict_inv + {f : ℂ → ℂ} + (h₁f : MeromorphicOn f ⊤) + (r : ℝ) : + h₁f.inv.restrict r = (h₁f.restrict r).inv := by + funext x + simp + + noncomputable def MeromorphicOn.N_zero {f : ℂ → ℂ} (hf : MeromorphicOn f ⊤) : @@ -28,6 +37,43 @@ noncomputable def MeromorphicOn.N_infty ℝ → ℝ := fun r ↦ ∑ᶠ z, (max 0 (-((hf.restrict r).divisor z))) * log (r * ‖z‖⁻¹) +theorem Nevanlinna_counting₀ + {f : ℂ → ℂ} + (hf : MeromorphicOn f ⊤) : + hf.inv.N_infty = hf.N_zero := by + funext r + unfold MeromorphicOn.N_zero MeromorphicOn.N_infty + let A := (hf.restrict r).divisor.finiteSupport (isCompact_closedBall 0 r) + repeat + rw [finsum_eq_sum_of_support_subset (s := A.toFinset)] + apply Finset.sum_congr rfl + intro x hx + congr + rw [hf.restrict_inv r] + rw [MeromorphicOn.divisor_inv] + simp + -- + exact fun x a => hf x trivial + -- + intro x + contrapose + simp + intro hx + rw [hx] + tauto + -- + intro x + contrapose + simp + intro hx h₁x + rw [hf.restrict_inv r] at h₁x + have hh : MeromorphicOn f (Metric.closedBall 0 r) := hf.restrict r + rw [hh.divisor_inv] at h₁x + simp at h₁x + rw [hx] at h₁x + tauto + + theorem Nevanlinna_counting {f : ℂ → ℂ} (hf : MeromorphicOn f ⊤) : @@ -73,27 +119,6 @@ noncomputable def MeromorphicOn.m_infty ℝ → ℝ := fun r ↦ (2 * π)⁻¹ * ∫ x in (0)..(2 * π), logpos ‖f (circleMap 0 r x)‖ -theorem Nevanlinna_proximity₀ - {f : ℂ → ℂ} - {r : ℝ} - (h₁f : MeromorphicOn f ⊤) - (hr : 0 < r) : - (2 * π)⁻¹ * ∫ x in (0)..(2 * π), log ‖f (circleMap 0 r x)‖ = (h₁f.m_infty r) - (h₁f.inv.m_infty r) := by - - unfold MeromorphicOn.m_infty - rw [← mul_sub]; congr - rw [← intervalIntegral.integral_sub]; congr - funext x - simp_rw [loglogpos]; congr - exact Eq.symm (IsAbsoluteValue.abv_inv Norm.norm (f (circleMap 0 r x))) - -- - apply MeromorphicOn.integrable_logpos_abs_f hr - intro z hx - exact h₁f z trivial - -- - apply MeromorphicOn.integrable_logpos_abs_f hr - exact MeromorphicOn.inv_iff.mpr fun x a => h₁f x trivial - theorem Nevanlinna_proximity {f : ℂ → ℂ} @@ -101,16 +126,6 @@ theorem Nevanlinna_proximity (h₁f : MeromorphicOn f ⊤) : (2 * π)⁻¹ * ∫ x in (0)..(2 * π), log ‖f (circleMap 0 r x)‖ = (h₁f.m_infty r) - (h₁f.inv.m_infty r) := by - by_cases h₁r : r = 0 - · unfold MeromorphicOn.m_infty - rw [← mul_sub]; congr - simp only [h₁r, circleMap_zero_radius, Function.const_apply, intervalIntegral.integral_const, sub_zero, smul_eq_mul, Pi.inv_apply, norm_inv] - rw [← mul_sub]; congr - exact loglogpos - - by_cases h₂r : 0 < r - · exact Nevanlinna_proximity₀ h₁f h₂r - unfold MeromorphicOn.m_infty rw [← mul_sub]; congr rw [← intervalIntegral.integral_sub]; congr @@ -119,30 +134,44 @@ theorem Nevanlinna_proximity exact Eq.symm (IsAbsoluteValue.abv_inv Norm.norm (f (circleMap 0 r x))) -- apply MeromorphicOn.integrable_logpos_abs_f + intro z hx + exact h₁f z trivial + -- + apply MeromorphicOn.integrable_logpos_abs_f + exact MeromorphicOn.inv_iff.mpr fun x a => h₁f x trivial - sorry - sorry - noncomputable def MeromorphicOn.T_infty {f : ℂ → ℂ} (hf : MeromorphicOn f ⊤) : ℝ → ℝ := hf.m_infty + hf.N_infty + theorem Nevanlinna_firstMain₁ {f : ℂ → ℂ} (h₁f : MeromorphicOn f ⊤) (h₂f : StronglyMeromorphicAt f 0) (h₃f : f 0 ≠ 0) : (fun r ↦ log ‖f 0‖) + h₁f.inv.T_infty = h₁f.T_infty := by + + rw [add_eq_of_eq_sub] + unfold MeromorphicOn.T_infty + + have {A B C D : ℝ → ℝ} : A + B - (C + D) = A - C + (B - D) := by + ring + rw [this] + clear this + funext r simp - unfold MeromorphicOn.T_infty + rw [← Nevanlinna_proximity h₁f] + + + unfold MeromorphicOn.N_infty unfold MeromorphicOn.m_infty simp - sorry theorem Nevanlinna_firstMain₂ diff --git a/Nevanlinna/meromorphicAt.lean b/Nevanlinna/meromorphicAt.lean index 516f4bf..f940e3f 100644 --- a/Nevanlinna/meromorphicAt.lean +++ b/Nevanlinna/meromorphicAt.lean @@ -147,4 +147,74 @@ theorem MeromorphicAt.order_mul · exact Set.mem_inter h₃t₁ h₃t₂ +theorem MeromorphicAt.order_neg_zero_iff + {f : ℂ → ℂ} + {z₀ : ℂ} + (hf : MeromorphicAt f z₀) : + hf.order ≠ ⊤ ↔ ∃ (g : ℂ → ℂ), AnalyticAt ℂ g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z = (z - z₀) ^ (hf.order.untop' 0) • g z := by + + constructor + · intro h + exact (hf.order_eq_int_iff (hf.order.untop' 0)).1 (Eq.symm (untop'_of_ne_top h)) + · rw [← hf.order_eq_int_iff] + intro h + exact Option.ne_none_iff_exists'.mpr ⟨hf.order.untop' 0, h⟩ + + +theorem MeromorphicAt.order_inv + {f : ℂ → ℂ} + {z₀ : ℂ} + (hf : MeromorphicAt f z₀) : + hf.order = -hf.inv.order := by + + by_cases h₂f : hf.order = ⊤ + · simp [h₂f] + have : hf.inv.order = ⊤ := by + rw [hf.inv.order_eq_top_iff] + rw [eventually_nhdsWithin_iff] + rw [eventually_nhds_iff] + + rw [hf.order_eq_top_iff] at h₂f + rw [eventually_nhdsWithin_iff] at h₂f + rw [eventually_nhds_iff] at h₂f + obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f + use t + constructor + · intro y h₁y h₂y + simp + rw [h₁t y h₁y h₂y] + · exact ⟨h₂t, h₃t⟩ + rw [this] + simp + + · have : hf.order = hf.order.untop' 0 := by + simp [h₂f, untop'_of_ne_top] + rw [this] + rw [eq_comm] + rw [neg_eq_iff_eq_neg] + apply (hf.inv.order_eq_int_iff (-hf.order.untop' 0)).2 + rw [hf.order_eq_int_iff] at this + obtain ⟨g, h₁g, h₂g, h₃g⟩ := this + use g⁻¹ + constructor + · exact AnalyticAt.inv h₁g h₂g + · constructor + · simp [h₂g] + · rw [eventually_nhdsWithin_iff] + rw [eventually_nhds_iff] + rw [eventually_nhdsWithin_iff] at h₃g + rw [eventually_nhds_iff] at h₃g + obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₃g + use t + constructor + · intro y h₁y h₂y + simp + let A := h₁t y h₁y h₂y + rw [A] + simp + rw [mul_comm] + · exact ⟨h₂t, h₃t⟩ + + + -- might want theorem MeromorphicAt.order_zpow diff --git a/Nevanlinna/meromorphicOn_divisor.lean b/Nevanlinna/meromorphicOn_divisor.lean index 671e90f..3a0bcbd 100644 --- a/Nevanlinna/meromorphicOn_divisor.lean +++ b/Nevanlinna/meromorphicOn_divisor.lean @@ -146,6 +146,29 @@ theorem MeromorphicOn.divisor_mul simp +theorem MeromorphicOn.divisor_inv + {f: ℂ → ℂ} + {U : Set ℂ} + (h₁f : MeromorphicOn f U) : + h₁f.inv.divisor.toFun = -h₁f.divisor.toFun := by + funext z + + by_cases hz : z ∈ U + · rw [MeromorphicOn.divisor_def₁] + simp + rw [MeromorphicOn.divisor_def₁] + rw [MeromorphicAt.order_inv] + simp + by_cases h₂f : (h₁f z hz).order = ⊤ + · simp [h₂f] + · let A := untop'_of_ne_top (d := 0) h₂f + rw [← A] + exact rfl + repeat exact hz + · unfold MeromorphicOn.divisor + simp [hz] + + theorem MeromorphicOn.divisor_of_makeStronglyMeromorphicOn {f : ℂ → ℂ} {U : Set ℂ} diff --git a/Nevanlinna/meromorphicOn_integrability.lean b/Nevanlinna/meromorphicOn_integrability.lean index f0053d1..39e4405 100644 --- a/Nevanlinna/meromorphicOn_integrability.lean +++ b/Nevanlinna/meromorphicOn_integrability.lean @@ -144,7 +144,11 @@ theorem MeromorphicOn.integrable_log_abs_f rw [this] at h₁f exact MeromorphicOn.integrable_log_abs_f₀ h₂r h₁f · have t₀ : 0 < -r := by - sorry + have hr_neg : r < 0 := by + apply lt_of_le_of_ne + exact le_of_not_lt h₂r + exact h₁r + linarith have : |r| = -r := by apply abs_of_neg exact Left.neg_pos_iff.mp t₀ @@ -157,13 +161,11 @@ theorem MeromorphicOn.integrable_log_abs_f simpa - theorem MeromorphicOn.integrable_logpos_abs_f {f : ℂ → ℂ} {r : ℝ} - (hr : 0 < r) -- WARNING: Not optimal. It suffices to be meromorphic on the Sphere - (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) r)) : + (h₁f : MeromorphicOn f (Metric.closedBall (0 : ℂ) |r|)) : IntervalIntegrable (fun z ↦ logpos ‖f (circleMap 0 r z)‖) MeasureTheory.volume 0 (2 * π) := by simp_rw [logpos_norm] @@ -171,8 +173,8 @@ theorem MeromorphicOn.integrable_logpos_abs_f apply IntervalIntegrable.add apply IntervalIntegrable.const_mul - exact MeromorphicOn.integrable_log_abs_f hr h₁f + exact MeromorphicOn.integrable_log_abs_f h₁f apply IntervalIntegrable.const_mul apply IntervalIntegrable.norm - exact MeromorphicOn.integrable_log_abs_f hr h₁f + exact MeromorphicOn.integrable_log_abs_f h₁f