From 9498d9f2038b8509eb5529846f522709d6fe466c Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 7 Oct 2024 13:06:55 +0200 Subject: [PATCH] Update mathlib --- Nevanlinna/analyticOnNhd_divisor.lean | 92 ++++------------------- Nevanlinna/holomorphic_JensenFormula.lean | 2 +- Nevanlinna/holomorphic_primitive.lean | 2 +- Nevanlinna/holomorphic_zero.lean | 2 +- lake-manifest.json | 12 +-- lean-toolchain | 2 +- 6 files changed, 24 insertions(+), 88 deletions(-) diff --git a/Nevanlinna/analyticOnNhd_divisor.lean b/Nevanlinna/analyticOnNhd_divisor.lean index e55ffaf..42d00cb 100644 --- a/Nevanlinna/analyticOnNhd_divisor.lean +++ b/Nevanlinna/analyticOnNhd_divisor.lean @@ -2,6 +2,7 @@ import Mathlib.Analysis.SpecialFunctions.Integrals import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog import Mathlib.Analysis.Convex.SpecificFunctions.Deriv import Nevanlinna.analyticAt +import Nevanlinna.divisor open scoped Interval Topology open Real Filter MeasureTheory intervalIntegral @@ -9,89 +10,24 @@ 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 + Divisor U where + + toFun := by + intro z + if hz : z ∈ U then + exact ((hf z hz).order.toNat : ℤ) + else + exact 0 + + supportInU := by + intro z hz + simp only [Function.mem_support] at hz + simp only [Function.mem_support, ne_eq, dite_eq_else, Nat.cast_eq_zero, ENat.toNat_eq_zero, not_forall, not_or] at hz - 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] diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean index 9153f04..63e02a7 100644 --- a/Nevanlinna/holomorphic_JensenFormula.lean +++ b/Nevanlinna/holomorphic_JensenFormula.lean @@ -1,6 +1,6 @@ import Mathlib.Analysis.Complex.CauchyIntegral import Mathlib.Analysis.Analytic.IsolatedZeros -import Nevanlinna.analyticOn_zeroSet +import Nevanlinna.analyticOnNhd_zeroSet import Nevanlinna.harmonicAt_examples import Nevanlinna.harmonicAt_meanValue import Nevanlinna.specialFunctions_CircleIntegral_affine diff --git a/Nevanlinna/holomorphic_primitive.lean b/Nevanlinna/holomorphic_primitive.lean index c132007..b134449 100644 --- a/Nevanlinna/holomorphic_primitive.lean +++ b/Nevanlinna/holomorphic_primitive.lean @@ -666,7 +666,7 @@ theorem primitive_additivity' dsimp [ε']; simp have : |ε| = ε := by apply abs_of_pos h₁ε rw [this] - apply (inv_mul_lt_iff zero_lt_two).mpr + apply (inv_mul_lt_iff₀ zero_lt_two).mpr linarith have h₁ε' : 0 < ε' := by apply mul_pos _ h₁ε diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean index d69e717..6252f52 100644 --- a/Nevanlinna/holomorphic_zero.lean +++ b/Nevanlinna/holomorphic_zero.lean @@ -3,7 +3,7 @@ import Mathlib.Analysis.Analytic.Meromorphic import Mathlib.Topology.ContinuousOn import Mathlib.Analysis.Analytic.IsolatedZeros import Nevanlinna.holomorphic -import Nevanlinna.analyticOn_zeroSet +import Nevanlinna.analyticOnNhd_zeroSet noncomputable def zeroDivisor diff --git a/lake-manifest.json b/lake-manifest.json index b241ad5..7a13544 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd", + "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", + "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a", + "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c", + "rev": "63a7d4a353f48f6c5f1bc19d0f018b0513cb370a", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ba60fa2c384a94735454db11a2d523612eaabff", + "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "eed3300c27c9f168d53e13bb198a92a147b671d0", + "rev": "cbe02ad0a6243d7688e60d69fd7ee0387d6f8059", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 98556ba..eff86fd 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0-rc1 +leanprover/lean4:v4.13.0-rc3