From c8f4cf12ca1a750d5063ab22565d636513beb83a Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 30 Sep 2024 14:12:33 +0200 Subject: [PATCH] Update to latest version of mathlib --- Nevanlinna/analyticAt.lean | 4 +- Nevanlinna/analyticOn_zeroSet.lean | 66 +++++++++++------------ Nevanlinna/bilinear.lean | 7 ++- Nevanlinna/divisor.lean | 24 ++++++--- Nevanlinna/holomorphic_JensenFormula.lean | 16 +++--- Nevanlinna/holomorphic_zero.lean | 22 ++++---- lake-manifest.json | 12 ++--- 7 files changed, 79 insertions(+), 72 deletions(-) diff --git a/Nevanlinna/analyticAt.lean b/Nevanlinna/analyticAt.lean index 807c463..b9c6693 100644 --- a/Nevanlinna/analyticAt.lean +++ b/Nevanlinna/analyticAt.lean @@ -116,10 +116,10 @@ theorem AnalyticAt.supp_order_toNat intro h₁f simp [hf.order_eq_zero_iff.2 h₁f] - +/- theorem ContinuousLinearEquiv.analyticAt (ℓ : ℂ ≃L[ℂ] ℂ) (z₀ : ℂ) : AnalyticAt ℂ (⇑ℓ) z₀ := ℓ.toContinuousLinearMap.analyticAt z₀ - +-/ theorem eventually_nhds_comp_composition {f₁ f₂ ℓ : ℂ → ℂ} diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean index f903b44..df14a9d 100644 --- a/Nevanlinna/analyticOn_zeroSet.lean +++ b/Nevanlinna/analyticOn_zeroSet.lean @@ -4,17 +4,17 @@ import Mathlib.Analysis.Complex.Basic import Nevanlinna.analyticAt -noncomputable def AnalyticOn.order - {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOn ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order +noncomputable def AnalyticOnNhd.order + {f : ℂ → ℂ} {U : Set ℂ} (hf : AnalyticOnNhd ℂ f U) : U → ℕ∞ := fun u ↦ (hf u u.2).order -theorem AnalyticOn.order_eq_nat_iff +theorem AnalyticOnNhd.order_eq_nat_iff {f : ℂ → ℂ} {U : Set ℂ} {z₀ : U} - (hf : AnalyticOn ℂ f U) + (hf : AnalyticOnNhd ℂ f U) (n : ℕ) : - hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by + hf.order z₀ = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by constructor -- Direction → @@ -91,31 +91,31 @@ theorem AnalyticOn.order_eq_nat_iff -- direction ← intro h obtain ⟨g, h₁g, h₂g, h₃g⟩ := h - dsimp [AnalyticOn.order] + dsimp [AnalyticOnNhd.order] rw [AnalyticAt.order_eq_nat_iff] use g exact ⟨h₁g z₀ z₀.2, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩ -theorem AnalyticOn.support_of_order₁ +theorem AnalyticOnNhd.support_of_order₁ {f : ℂ → ℂ} {U : Set ℂ} - (hf : AnalyticOn ℂ f U) : + (hf : AnalyticOnNhd ℂ f U) : Function.support hf.order = U.restrict f⁻¹' {0} := by ext u - simp [AnalyticOn.order] + simp [AnalyticOnNhd.order] rw [not_iff_comm, (hf u u.2).order_eq_zero_iff] -theorem AnalyticOn.eliminateZeros +theorem AnalyticOnNhd.eliminateZeros {f : ℂ → ℂ} {U : Set ℂ} {A : Finset U} - (hf : AnalyticOn ℂ f U) + (hf : AnalyticOnNhd ℂ f U) (n : U → ℕ) : - (∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by + (∀ a ∈ A, hf.order a = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z := by - apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z) + apply Finset.induction (α := U) (p := fun A ↦ (∀ a ∈ A, (hf a.1 a.2).order = n a) → ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ a ∈ A, g a ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (n a)) • g z) -- case empty simp @@ -146,7 +146,7 @@ theorem AnalyticOn.eliminateZeros intro b _ apply AnalyticAt.pow apply AnalyticAt.sub - apply analyticAt_id ℂ + apply analyticAt_id exact analyticAt_const have h₂φ : h₁φ.order = (0 : ℕ) := by @@ -173,7 +173,7 @@ theorem AnalyticOn.eliminateZeros rw [h₂φ] simp - obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ (n b₀)).1 this + obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOnNhd.order_eq_nat_iff h₁g₀ (n b₀)).1 this use g₁ constructor @@ -203,7 +203,7 @@ theorem XX {f : ℂ → ℂ} {U : Set ℂ} (hU : IsPreconnected U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ u ∈ U, f u ≠ 0) : ∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by @@ -221,7 +221,7 @@ theorem discreteZeros {f : ℂ → ℂ} {U : Set ℂ} (hU : IsPreconnected U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ u ∈ U, f u ≠ 0) : DiscreteTopology ((U.restrict f)⁻¹' {0}) := by @@ -293,7 +293,7 @@ theorem finiteZeros {U : Set ℂ} (h₁U : IsPreconnected U) (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ u ∈ U, f u ≠ 0) : Set.Finite (U.restrict f⁻¹' {0}) := by @@ -310,14 +310,14 @@ theorem finiteZeros exact discreteZeros h₁U h₁f h₂f -theorem AnalyticOnCompact.eliminateZeros +theorem AnalyticOnNhdCompact.eliminateZeros {f : ℂ → ℂ} {U : Set ℂ} (h₁U : IsPreconnected U) (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by + ∃ (g : ℂ → ℂ) (A : Finset U), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ A, (z - a) ^ (h₁f.order a).toNat) • g z := by let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset @@ -325,13 +325,13 @@ theorem AnalyticOnCompact.eliminateZeros have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by intro a _ - dsimp [n, AnalyticOn.order] + dsimp [n, AnalyticOnNhd.order] rw [eq_comm] apply XX h₁U exact h₂f - obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn + obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn use g use A @@ -357,14 +357,14 @@ theorem AnalyticOnCompact.eliminateZeros · exact inter -theorem AnalyticOnCompact.eliminateZeros₂ +theorem AnalyticOnNhdCompact.eliminateZeros₂ {f : ℂ → ℂ} {U : Set ℂ} (h₁U : IsPreconnected U) (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by + ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ a ∈ (finiteZeros h₁U h₂U h₁f h₂f).toFinset, (z - a) ^ (h₁f.order a).toNat) • g z := by let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset @@ -372,12 +372,12 @@ theorem AnalyticOnCompact.eliminateZeros₂ have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by intro a _ - dsimp [n, AnalyticOn.order] + dsimp [n, AnalyticOnNhd.order] rw [eq_comm] apply XX h₁U exact h₂f - obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn + obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn use g have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by @@ -402,14 +402,14 @@ theorem AnalyticOnCompact.eliminateZeros₂ · exact h₃g -theorem AnalyticOnCompact.eliminateZeros₁ +theorem AnalyticOnNhdCompact.eliminateZeros₁ {f : ℂ → ℂ} {U : Set ℂ} (h₁U : IsPreconnected U) (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by + ∃ (g : ℂ → ℂ), AnalyticOnNhd ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a, (z - a) ^ (h₁f.order a).toNat) • g z := by let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset @@ -417,12 +417,12 @@ theorem AnalyticOnCompact.eliminateZeros₁ have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by intro a _ - dsimp [n, AnalyticOn.order] + dsimp [n, AnalyticOnNhd.order] rw [eq_comm] apply XX h₁U exact h₂f - obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOn.eliminateZeros (A := A) h₁f n hn + obtain ⟨g, h₁g, h₂g, h₃g⟩ := AnalyticOnNhd.eliminateZeros (A := A) h₁f n hn use g have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean index dacf4c4..533b209 100644 --- a/Nevanlinna/bilinear.lean +++ b/Nevanlinna/bilinear.lean @@ -28,7 +28,7 @@ orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`. -/ - +open InnerProductSpace open TensorProduct @@ -41,12 +41,11 @@ noncomputable def InnerProductSpace.canonicalCovariantTensor (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i) - theorem InnerProductSpace.canonicalCovariantTensorRepresentation (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [Fintype ι] - (v : OrthonormalBasis ι ℝ E) - : InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by + (v : OrthonormalBasis ι ℝ E) : + InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by let w := stdOrthonormalBasis ℝ E conv => diff --git a/Nevanlinna/divisor.lean b/Nevanlinna/divisor.lean index ee81b3f..e5ddd49 100644 --- a/Nevanlinna/divisor.lean +++ b/Nevanlinna/divisor.lean @@ -1,5 +1,13 @@ +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 : ℂ → ℤ @@ -48,10 +56,10 @@ theorem Divisor.support_cap_compact exact Set.inter_subset_right -noncomputable def AnalyticOn.zeroDivisor +noncomputable def AnalyticOnNhd.zeroDivisor {f : ℂ → ℂ} {U : Set ℂ} - (hf : AnalyticOn ℂ f U) : + (hf : AnalyticOnNhd ℂ f U) : Divisor where toFun := by @@ -124,28 +132,28 @@ noncomputable def AnalyticOn.zeroDivisor tauto -theorem AnalyticOn.support_of_zeroDivisor +theorem AnalyticOnNhd.support_of_zeroDivisor {f : ℂ → ℂ} {U : Set ℂ} - (hf : AnalyticOn ℂ f U) : + (hf : AnalyticOnNhd ℂ f U) : Function.support hf.zeroDivisor ⊆ U := by intro z contrapose intro hz - dsimp [AnalyticOn.zeroDivisor] + dsimp [AnalyticOnNhd.zeroDivisor] simp tauto -theorem AnalyticOn.support_of_zeroDivisor₂ +theorem AnalyticOnNhd.support_of_zeroDivisor₂ {f : ℂ → ℂ} {U : Set ℂ} - (hf : AnalyticOn ℂ f U) : + (hf : AnalyticOnNhd ℂ f U) : Function.support hf.zeroDivisor ⊆ f⁻¹' {0} := by intro z hz - dsimp [AnalyticOn.zeroDivisor] at 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 diff --git a/Nevanlinna/holomorphic_JensenFormula.lean b/Nevanlinna/holomorphic_JensenFormula.lean index 60a3370..9153f04 100644 --- a/Nevanlinna/holomorphic_JensenFormula.lean +++ b/Nevanlinna/holomorphic_JensenFormula.lean @@ -11,7 +11,7 @@ open Real theorem jensen_case_R_eq_one (f : ℂ → ℂ) - (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 1)) + (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 1)) (h₂f : f 0 ≠ 0) : log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by @@ -24,7 +24,7 @@ theorem jensen_case_R_eq_one have h'₂f : ∃ u ∈ (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by use 0; simp; exact h₂f - obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f + obtain ⟨F, h₁F, h₂F, h₃F⟩ := AnalyticOnNhdCompact.eliminateZeros₂ h₁U h₂U h₁f h'₂f have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by intro z h₁z @@ -259,9 +259,9 @@ theorem jensen_case_R_eq_one intro x ⟨h₁x, _⟩ simp - dsimp [AnalyticOn.order] at h₁x + dsimp [AnalyticOnNhd.order] at h₁x simp only [Function.mem_support, ne_eq, Nat.cast_eq_zero, not_or] at h₁x - exact AnalyticAt.supp_order_toNat (AnalyticOn.order.proof_1 h₁f x) h₁x + exact AnalyticAt.supp_order_toNat (AnalyticOnNhd.order.proof_1 h₁f x) h₁x -- intro x hx @@ -297,7 +297,7 @@ theorem jensen {R : ℝ} (hR : 0 < R) (f : ℂ → ℂ) - (h₁f : AnalyticOn ℂ f (Metric.closedBall 0 R)) + (h₁f : AnalyticOnNhd ℂ f (Metric.closedBall 0 R)) (h₂f : f 0 ≠ 0) : log ‖f 0‖ = -∑ᶠ s, (h₁f.order s).toNat * log (R * ‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by @@ -327,8 +327,8 @@ theorem jensen let F := f ∘ ℓ - have h₁F : AnalyticOn ℂ F (Metric.closedBall 0 1) := by - apply AnalyticOn.comp (t := Metric.closedBall 0 R) + have h₁F : AnalyticOnNhd ℂ F (Metric.closedBall 0 1) := by + apply AnalyticOnNhd.comp (t := Metric.closedBall 0 R) exact h₁f intro x _ apply ℓ.toContinuousLinearMap.analyticAt x @@ -430,7 +430,7 @@ theorem jensen left congr 1 - dsimp [AnalyticOn.order] + dsimp [AnalyticOnNhd.order] rw [← AnalyticAt.order_comp_CLE ℓ] -- diff --git a/Nevanlinna/holomorphic_zero.lean b/Nevanlinna/holomorphic_zero.lean index a4017c6..d69e717 100644 --- a/Nevanlinna/holomorphic_zero.lean +++ b/Nevanlinna/holomorphic_zero.lean @@ -134,7 +134,7 @@ theorem topOnPreconnected {f : ℂ → ℂ} {U : Set ℂ} (hU : IsPreconnected U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ z ∈ U, f z ≠ 0) : ∀ (hz : z ∈ U), (h₁f z hz).order ≠ ⊤ := by @@ -143,7 +143,7 @@ theorem topOnPreconnected obtain ⟨z', hz'⟩ := H rw [AnalyticAt.order_eq_top_iff] at hz' rw [← AnalyticAt.frequently_zero_iff_eventually_zero (h₁f z z')] at hz' - have A := AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz' + have A := AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero h₁f hU z' hz' tauto @@ -151,7 +151,7 @@ theorem supportZeroSet {f : ℂ → ℂ} {U : Set ℂ} (hU : IsPreconnected U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ z ∈ U, f z ≠ 0) : U ∩ Function.support (zeroDivisor f) = U ∩ f⁻¹' {0} := by @@ -180,7 +180,7 @@ theorem supportZeroSet refine Eq.symm (ENat.coe_toNat ?h.mpr.right.right.right.a) exact topOnPreconnected hU h₁f h₂f h₁x - +/- theorem discreteZeros {f : ℂ → ℂ} : DiscreteTopology (Function.support (zeroDivisor f)) := by @@ -254,13 +254,13 @@ theorem discreteZeros simp [this] at F ext rwa [sub_eq_zero] at F - +-/ theorem zeroDivisor_finiteOnCompact {f : ℂ → ℂ} {U : Set ℂ} (hU : IsPreconnected U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ z ∈ U, f z ≠ 0) -- not needed! (h₂U : IsCompact U) : Set.Finite (U ∩ Function.support (zeroDivisor f)) := by @@ -289,7 +289,7 @@ noncomputable def zeroDivisorDegree {U : Set ℂ} (h₁U : IsPreconnected U) -- not needed! (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed! ℕ := (zeroDivisor_finiteOnCompact h₁U h₁f h₂f h₂U).toFinset.card @@ -299,7 +299,7 @@ lemma zeroDivisorDegreeZero {U : Set ℂ} (h₁U : IsPreconnected U) -- not needed! (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ f U) + (h₁f : AnalyticOnNhd ℂ f U) (h₂f : ∃ z ∈ U, f z ≠ 0) : -- not needed! 0 = zeroDivisorDegree h₁U h₂U h₁f h₂f ↔ U ∩ (zeroDivisor f).support = ∅ := by sorry @@ -309,9 +309,9 @@ lemma eliminatingZeros₀ {U : Set ℂ} (h₁U : IsPreconnected U) (h₂U : IsCompact U) : - ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOn ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) → + ∀ n : ℕ, ∀ f : ℂ → ℂ, (h₁f : AnalyticOnNhd ℂ f U) → (h₂f : ∃ z ∈ U, f z ≠ 0) → (n = zeroDivisorDegree h₁U h₂U h₁f h₂f) → - ∃ F : ℂ → ℂ, (AnalyticOn ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by + ∃ F : ℂ → ℂ, (AnalyticOnNhd ℂ F U) ∧ (f = F * ∏ᶠ a ∈ (U ∩ (zeroDivisor f).support), fun z ↦ (z - a) ^ (zeroDivisor f a)) := by intro n induction' n with n ih @@ -340,7 +340,7 @@ lemma eliminatingZeros₀ - let A := AnalyticOn.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀) + let A := AnalyticOnNhd.order_eq_nat_iff h₁f hz₀.1 (zeroDivisor f z₀) let B := zeroDivisor_eq_ord_AtZeroDivisorSupport hz₀.2 let B := zeroDivisor_eq_ord_AtZeroDivisorSupport' hz₀.2 rw [eq_comm] at B diff --git a/lake-manifest.json b/lake-manifest.json index 6238b47..b241ad5 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "46fed98b5cac2b1ea64e363b420c382ed1af0d85", + "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "662f986ad3c5ad6ab1a1726b3c04f5ec425aa9f7", + "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -61,11 +61,11 @@ "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, - {"url": "https://github.com/siddhartha-gadgil/LeanSearchClient.git", + {"url": "https://github.com/leanprover-community/LeanSearchClient", "type": "git", "subDir": null, - "scope": "", - "rev": "c260ed920e2ebd23ef9fc8ca3fd24115e04c18b1", + "scope": "leanprover-community", + "rev": "2ba60fa2c384a94735454db11a2d523612eaabff", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "4e40837aec257729b3c38dc3e635fc64a7a8a8c1", + "rev": "eed3300c27c9f168d53e13bb198a92a147b671d0", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,