From 86da08ebc83c107ff25891c109ef05d6a56ae598 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 7 Oct 2024 07:56:42 +0200 Subject: [PATCH] working --- Nevanlinna/analyticOnNhd_divisor.lean | 187 ++++++++++++++++++++++++++ Nevanlinna/divisor.lean | 187 ++------------------------ 2 files changed, 198 insertions(+), 176 deletions(-) create mode 100644 Nevanlinna/analyticOnNhd_divisor.lean diff --git a/Nevanlinna/analyticOnNhd_divisor.lean b/Nevanlinna/analyticOnNhd_divisor.lean new file mode 100644 index 0000000..e55ffaf --- /dev/null +++ b/Nevanlinna/analyticOnNhd_divisor.lean @@ -0,0 +1,187 @@ +import Mathlib.Analysis.SpecialFunctions.Integrals +import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog +import Mathlib.Analysis.Convex.SpecificFunctions.Deriv +import Nevanlinna.analyticAt + +open scoped Interval Topology +open Real Filter MeasureTheory intervalIntegral + + + + +structure Divisor where + toFun : ℂ → ℤ + -- This is not what we want. We want: locally finite + discreteSupport : DiscreteTopology (Function.support toFun) + +instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where +coe := Divisor.toFun +attribute [coe] Divisor.toFun + + + +noncomputable def Divisor.deg + (D : Divisor) : ℤ := ∑ᶠ z, D z + +noncomputable def Divisor.n_trunk + (D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z) + +noncomputable def Divisor.n + (D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z + +noncomputable def Divisor.N_trunk + (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t + + +theorem Divisor.support_cap_closed₁ + {S U : Set ℂ} + (hS : DiscreteTopology S) + (hU : IsClosed U) : + IsClosed (U ∩ S) := by + + rw [← isOpen_compl_iff] + rw [isOpen_iff_forall_mem_open] + intro x hx + by_cases h₁x : x ∈ U + · simp at hx + + + sorry + · use Uᶜ + constructor + · simp + · constructor + · exact IsClosed.isOpen_compl + · assumption + + + +theorem Divisor.support_cap_closed + (D : Divisor) + {U : Set ℂ} + (h₁U : IsClosed U) : + IsClosed (U ∩ D.toFun.support) := by + sorry + + +theorem Divisor.support_cap_compact + (D : Divisor) + {U : Set ℂ} + (h₁U : IsCompact U) : + Set.Finite (U ∩ (Function.support D)) := by + + apply IsCompact.finite + -- Target set is compact + apply h₁U.of_isClosed_subset + apply D.support_cap_closed h₁U.isClosed + exact Set.inter_subset_left + -- Target set is discrete + apply DiscreteTopology.of_subset D.discreteSupport + exact Set.inter_subset_right + + +noncomputable def AnalyticOnNhd.zeroDivisor + {f : ℂ → ℂ} + {U : Set ℂ} + (hf : AnalyticOnNhd ℂ f U) : + Divisor where + + toFun := by + intro z + if hz : z ∈ U then + exact ((hf z hz).order.toNat : ℤ) + else + exact 0 + + discreteSupport := by + simp_rw [← singletons_open_iff_discrete] + simp_rw [Metric.isOpen_singleton_iff] + simp + + -- simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq] + + intro a ha ⟨h₁a, h₂a⟩ + obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a + rw [Metric.eventually_nhds_iff_ball] at h₃g + + have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by + have h₄g : ContinuousAt g a := + AnalyticAt.continuousAt h₁g + have : {0}ᶜ ∈ nhds (g a) := by + exact compl_singleton_mem_nhds_iff.mpr h₂g + let F := h₄g.preimage_mem_nhds this + rw [Metric.mem_nhds_iff] at F + obtain ⟨ε, h₁ε, h₂ε⟩ := F + use ε + constructor; exact h₁ε + intro y hy + let G := h₂ε hy + simp at G + exact G + + obtain ⟨ε₁, h₁ε₁⟩ := this + obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g + use min ε₁ ε₂ + constructor + · have : 0 < min ε₁ ε₂ := by + rw [lt_min_iff] + exact And.imp_right (fun _ => h₁ε₂) h₁ε₁ + exact this + + intro y hy ⟨h₁y, h₂y⟩ h₃ + + have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by + simp + calc dist y a + _ < min ε₁ ε₂ := by assumption + _ ≤ ε₂ := by exact min_le_right ε₁ ε₂ + + have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by + simp + calc dist y a + _ < min ε₁ ε₂ := by assumption + _ ≤ ε₁ := by exact min_le_left ε₁ ε₂ + + have F := h₂ε₂ y h'₂y + have : f y = 0 := by + rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y + tauto + rw [this] at F + simp at F + + have : g y ≠ 0 := by + exact h₁ε₁.2 y h₃y + simp [this] at F + rw [sub_eq_zero] at F + tauto + + +theorem AnalyticOnNhd.support_of_zeroDivisor + {f : ℂ → ℂ} + {U : Set ℂ} + (hf : AnalyticOnNhd ℂ f U) : + Function.support hf.zeroDivisor ⊆ U := by + + intro z + contrapose + intro hz + dsimp [AnalyticOnNhd.zeroDivisor] + simp + tauto + + +theorem AnalyticOnNhd.support_of_zeroDivisor₂ + {f : ℂ → ℂ} + {U : Set ℂ} + (hf : AnalyticOnNhd ℂ f U) : + Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by + + intro z hz + dsimp [AnalyticOnNhd.zeroDivisor] at hz + have t₀ := hf.support_of_zeroDivisor hz + simp [hf.support_of_zeroDivisor hz] at hz + let A := hz.1 + let C := (hf z t₀).order_eq_zero_iff + simp + rw [C] at A + tauto diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean index e55ffaf..aad88e3 100644 --- a/Nevanlinna/divisor.lean +++ b/Nevanlinna/divisor.lean @@ -3,185 +3,20 @@ import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog import Mathlib.Analysis.Convex.SpecificFunctions.Deriv import Nevanlinna.analyticAt -open scoped Interval Topology +open Interval Topology open Real Filter MeasureTheory intervalIntegral - - -structure Divisor where +structure Divisor + (U : Set ℂ) + where toFun : ℂ → ℤ - -- This is not what we want. We want: locally finite - discreteSupport : DiscreteTopology (Function.support toFun) + supportInU : toFun.support ⊆ U + locallyFiniteInU : ∀ x ∈ U, ∃ N ∈ 𝓝 x, (N ∩ toFun.support).Finite + +instance + (U : Set ℂ) : + CoeFun (Divisor U) (fun _ ↦ ℂ → ℤ) where + coe := Divisor.toFun -instance : CoeFun Divisor (fun _ ↦ ℂ → ℤ) where -coe := Divisor.toFun attribute [coe] Divisor.toFun - - - -noncomputable def Divisor.deg - (D : Divisor) : ℤ := ∑ᶠ z, D z - -noncomputable def Divisor.n_trunk - (D : Divisor) : ℤ → ℝ → ℤ := fun k r ↦ ∑ᶠ z ∈ Metric.ball 0 r, min k (D z) - -noncomputable def Divisor.n - (D : Divisor) : ℝ → ℤ := fun r ↦ ∑ᶠ z ∈ Metric.ball 0 r, D z - -noncomputable def Divisor.N_trunk - (D : Divisor) : ℤ → ℝ → ℝ := fun k r ↦ ∫ (t : ℝ) in (1)..r, (D.n_trunk k t) / t - - -theorem Divisor.support_cap_closed₁ - {S U : Set ℂ} - (hS : DiscreteTopology S) - (hU : IsClosed U) : - IsClosed (U ∩ S) := by - - rw [← isOpen_compl_iff] - rw [isOpen_iff_forall_mem_open] - intro x hx - by_cases h₁x : x ∈ U - · simp at hx - - - sorry - · use Uᶜ - constructor - · simp - · constructor - · exact IsClosed.isOpen_compl - · assumption - - - -theorem Divisor.support_cap_closed - (D : Divisor) - {U : Set ℂ} - (h₁U : IsClosed U) : - IsClosed (U ∩ D.toFun.support) := by - sorry - - -theorem Divisor.support_cap_compact - (D : Divisor) - {U : Set ℂ} - (h₁U : IsCompact U) : - Set.Finite (U ∩ (Function.support D)) := by - - apply IsCompact.finite - -- Target set is compact - apply h₁U.of_isClosed_subset - apply D.support_cap_closed h₁U.isClosed - exact Set.inter_subset_left - -- Target set is discrete - apply DiscreteTopology.of_subset D.discreteSupport - exact Set.inter_subset_right - - -noncomputable def AnalyticOnNhd.zeroDivisor - {f : ℂ → ℂ} - {U : Set ℂ} - (hf : AnalyticOnNhd ℂ f U) : - Divisor where - - toFun := by - intro z - if hz : z ∈ U then - exact ((hf z hz).order.toNat : ℤ) - else - exact 0 - - discreteSupport := by - simp_rw [← singletons_open_iff_discrete] - simp_rw [Metric.isOpen_singleton_iff] - simp - - -- simp only [dite_eq_ite, gt_iff_lt, Subtype.forall, Function.mem_support, ne_eq, ite_eq_else, Classical.not_imp, not_or, Subtype.mk.injEq] - - intro a ha ⟨h₁a, h₂a⟩ - obtain ⟨g, h₁g, h₂g, h₃g⟩ := (AnalyticAt.order_neq_top_iff (hf a ha)).1 h₂a - rw [Metric.eventually_nhds_iff_ball] at h₃g - - have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑a) ε, g y ≠ 0 := by - have h₄g : ContinuousAt g a := - AnalyticAt.continuousAt h₁g - have : {0}ᶜ ∈ nhds (g a) := by - exact compl_singleton_mem_nhds_iff.mpr h₂g - let F := h₄g.preimage_mem_nhds this - rw [Metric.mem_nhds_iff] at F - obtain ⟨ε, h₁ε, h₂ε⟩ := F - use ε - constructor; exact h₁ε - intro y hy - let G := h₂ε hy - simp at G - exact G - - obtain ⟨ε₁, h₁ε₁⟩ := this - obtain ⟨ε₂, h₁ε₂, h₂ε₂⟩ := h₃g - use min ε₁ ε₂ - constructor - · have : 0 < min ε₁ ε₂ := by - rw [lt_min_iff] - exact And.imp_right (fun _ => h₁ε₂) h₁ε₁ - exact this - - intro y hy ⟨h₁y, h₂y⟩ h₃ - - have h'₂y : ↑y ∈ Metric.ball (↑a) ε₂ := by - simp - calc dist y a - _ < min ε₁ ε₂ := by assumption - _ ≤ ε₂ := by exact min_le_right ε₁ ε₂ - - have h₃y : ↑y ∈ Metric.ball (↑a) ε₁ := by - simp - calc dist y a - _ < min ε₁ ε₂ := by assumption - _ ≤ ε₁ := by exact min_le_left ε₁ ε₂ - - have F := h₂ε₂ y h'₂y - have : f y = 0 := by - rw [AnalyticAt.order_eq_zero_iff (hf y hy)] at h₁y - tauto - rw [this] at F - simp at F - - have : g y ≠ 0 := by - exact h₁ε₁.2 y h₃y - simp [this] at F - rw [sub_eq_zero] at F - tauto - - -theorem AnalyticOnNhd.support_of_zeroDivisor - {f : ℂ → ℂ} - {U : Set ℂ} - (hf : AnalyticOnNhd ℂ f U) : - Function.support hf.zeroDivisor ⊆ U := by - - intro z - contrapose - intro hz - dsimp [AnalyticOnNhd.zeroDivisor] - simp - tauto - - -theorem AnalyticOnNhd.support_of_zeroDivisor₂ - {f : ℂ → ℂ} - {U : Set ℂ} - (hf : AnalyticOnNhd ℂ f U) : - Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by - - intro z hz - dsimp [AnalyticOnNhd.zeroDivisor] at hz - have t₀ := hf.support_of_zeroDivisor hz - simp [hf.support_of_zeroDivisor hz] at hz - let A := hz.1 - let C := (hf z t₀).order_eq_zero_iff - simp - rw [C] at A - tauto