From 745e614016ad4f656d4e02999bd3c5de0257d34a Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Tue, 10 Sep 2024 15:29:30 +0200 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/analyticOn_zeroSet.lean | 50 ++- Nevanlinna/analyticOn_zeroSet2.lean | 449 --------------------- Nevanlinna/holomorphic_JensenFormula2.lean | 35 +- 3 files changed, 74 insertions(+), 460 deletions(-) delete mode 100644 Nevanlinna/analyticOn_zeroSet2.lean diff --git a/Nevanlinna/analyticOn_zeroSet.lean b/Nevanlinna/analyticOn_zeroSet.lean index 80d95bf..24aa461 100644 --- a/Nevanlinna/analyticOn_zeroSet.lean +++ b/Nevanlinna/analyticOn_zeroSet.lean @@ -357,6 +357,53 @@ theorem AnalyticOnCompact.eliminateZeros · exact inter + + +theorem AnalyticOnCompact.eliminateZeros₂ + {f : ℂ → ℂ} + {U : Set ℂ} + (h₁U : IsPreconnected U) + (h₂U : IsCompact U) + (h₁f : AnalyticOn ℂ 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 + + let A := (finiteZeros h₁U h₂U h₁f h₂f).toFinset + + let n : U → ℕ := fun z ↦ (h₁f z z.2).order.toNat + + have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by + intro a _ + dsimp [n, AnalyticOn.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 + use g + + have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by + intro z + rw [h₃g z] + + constructor + · exact h₁g + · constructor + · intro z h₁z + by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet + · exact h₂g ⟨z, h₁z⟩ h₂z + · have : f z ≠ 0 := by + by_contra C + have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by + dsimp [A] + simp + exact C + tauto + rw [inter z] at this + exact right_ne_zero_of_smul this + · exact h₃g + + theorem AnalyticOnCompact.eliminateZeros₁ {f : ℂ → ℂ} {U : Set ℂ} @@ -364,8 +411,7 @@ theorem AnalyticOnCompact.eliminateZeros₁ (h₂U : IsCompact U) (h₁f : AnalyticOn ℂ f U) (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ a : U, (z - a) ^ (h₁f.order a).toNat) • g z := by - + ∃ (g : ℂ → ℂ), AnalyticOn ℂ 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 diff --git a/Nevanlinna/analyticOn_zeroSet2.lean b/Nevanlinna/analyticOn_zeroSet2.lean deleted file mode 100644 index 94c65bf..0000000 --- a/Nevanlinna/analyticOn_zeroSet2.lean +++ /dev/null @@ -1,449 +0,0 @@ -import Mathlib.Analysis.Analytic.Constructions -import Mathlib.Analysis.Analytic.IsolatedZeros -import Mathlib.Analysis.Complex.Basic - - -theorem AnalyticOn.order_eq_nat_iff - {f : ℂ → ℂ} - {U : Set ℂ} - {z₀ : ℂ} - (hf : AnalyticOn ℂ f U) - (hz₀ : z₀ ∈ U) - (n : ℕ) : - (hf z₀ hz₀).order = ↑n ↔ ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ g z₀ ≠ 0 ∧ ∀ z, f z = (z - z₀) ^ n • g z := by - - constructor - -- Direction → - intro hn - obtain ⟨gloc, h₁gloc, h₂gloc, h₃gloc⟩ := (AnalyticAt.order_eq_nat_iff (hf z₀ hz₀) n).1 hn - - -- Define a candidate function; this is (f z) / (z - z₀) ^ n with the - -- removable singularity removed - let g : ℂ → ℂ := fun z ↦ if z = z₀ then gloc z₀ else (f z) / (z - z₀) ^ n - - -- Describe g near z₀ - have g_near_z₀ : ∀ᶠ (z : ℂ) in nhds z₀, g z = gloc z := by - rw [eventually_nhds_iff] - obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 h₃gloc - use t - constructor - · intro y h₁y - by_cases h₂y : y = z₀ - · dsimp [g]; simp [h₂y] - · dsimp [g]; simp [h₂y] - rw [div_eq_iff_mul_eq, eq_comm, mul_comm] - exact h₁t y h₁y - norm_num - rw [sub_eq_zero] - tauto - · constructor - · assumption - · assumption - - -- Describe g near points z₁ that are different from z₀ - have g_near_z₁ {z₁ : ℂ} : z₁ ≠ z₀ → ∀ᶠ (z : ℂ) in nhds z₁, g z = f z / (z - z₀) ^ n := by - intro hz₁ - rw [eventually_nhds_iff] - use {z₀}ᶜ - constructor - · intro y hy - simp at hy - simp [g, hy] - · exact ⟨isOpen_compl_singleton, hz₁⟩ - - -- Use g and show that it has all required properties - use g - constructor - · -- AnalyticOn ℂ g U - intro z h₁z - by_cases h₂z : z = z₀ - · rw [h₂z] - apply AnalyticAt.congr h₁gloc - exact Filter.EventuallyEq.symm g_near_z₀ - · simp_rw [eq_comm] at g_near_z₁ - apply AnalyticAt.congr _ (g_near_z₁ h₂z) - apply AnalyticAt.div - exact hf z h₁z - apply AnalyticAt.pow - apply AnalyticAt.sub - apply analyticAt_id - apply analyticAt_const - simp - rw [sub_eq_zero] - tauto - · constructor - · simp [g]; tauto - · intro z - by_cases h₂z : z = z₀ - · rw [h₂z, g_near_z₀.self_of_nhds] - exact h₃gloc.self_of_nhds - · rw [(g_near_z₁ h₂z).self_of_nhds] - simp [h₂z] - rw [div_eq_mul_inv, mul_comm, mul_assoc, inv_mul_cancel₀] - simp; norm_num - rw [sub_eq_zero] - tauto - - -- direction ← - intro h - obtain ⟨g, h₁g, h₂g, h₃g⟩ := h - rw [AnalyticAt.order_eq_nat_iff] - use g - exact ⟨h₁g z₀ hz₀, ⟨h₂g, Filter.Eventually.of_forall h₃g⟩⟩ - - -theorem AnalyticAt.order_mul - {f₁ f₂ : ℂ → ℂ} - {z₀ : ℂ} - (hf₁ : AnalyticAt ℂ f₁ z₀) - (hf₂ : AnalyticAt ℂ f₂ z₀) : - (AnalyticAt.mul hf₁ hf₂).order = hf₁.order + hf₂.order := by - by_cases h₂f₁ : hf₁.order = ⊤ - · simp [h₂f₁] - rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] - rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₁ - obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₁ - use t - constructor - · intro y hy - rw [h₁t y hy] - ring - · exact ⟨h₂t, h₃t⟩ - · by_cases h₂f₂ : hf₂.order = ⊤ - · simp [h₂f₂] - rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] - rw [AnalyticAt.order_eq_top_iff, eventually_nhds_iff] at h₂f₂ - obtain ⟨t, h₁t, h₂t, h₃t⟩ := h₂f₂ - use t - constructor - · intro y hy - rw [h₁t y hy] - ring - · exact ⟨h₂t, h₃t⟩ - · obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticAt.order_eq_nat_iff hf₁ ↑hf₁.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₁)) - obtain ⟨g₂, h₁g₂, h₂g₂, h₃g₂⟩ := (AnalyticAt.order_eq_nat_iff hf₂ ↑hf₂.order.toNat).1 (eq_comm.1 (ENat.coe_toNat h₂f₂)) - rw [← ENat.coe_toNat h₂f₁, ← ENat.coe_toNat h₂f₂, ← ENat.coe_add] - rw [AnalyticAt.order_eq_nat_iff (AnalyticAt.mul hf₁ hf₂) ↑(hf₁.order.toNat + hf₂.order.toNat)] - use g₁ * g₂ - constructor - · exact AnalyticAt.mul h₁g₁ h₁g₂ - · constructor - · simp; tauto - · obtain ⟨t₁, h₁t₁, h₂t₁, h₃t₁⟩ := eventually_nhds_iff.1 h₃g₁ - obtain ⟨t₂, h₁t₂, h₂t₂, h₃t₂⟩ := eventually_nhds_iff.1 h₃g₂ - rw [eventually_nhds_iff] - use t₁ ∩ t₂ - constructor - · intro y hy - rw [h₁t₁ y hy.1, h₁t₂ y hy.2] - simp; ring - · constructor - · exact IsOpen.inter h₂t₁ h₂t₂ - · exact Set.mem_inter h₃t₁ h₃t₂ - - -theorem AnalyticOn.eliminateZeros - {f : ℂ → ℂ} - {U : Set ℂ} - {A : Finset U} - (hf : AnalyticOn ℂ f U) - (n : ℂ → ℕ) : - (∀ 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 := 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) - - -- case empty - simp - use f - simp - exact hf - - -- case insert - intro b₀ B hb iHyp - intro hBinsert - obtain ⟨g₀, h₁g₀, h₂g₀, h₃g₀⟩ := iHyp (fun a ha ↦ hBinsert a (Finset.mem_insert_of_mem ha)) - - have : (h₁g₀ b₀ b₀.2).order = n b₀ := by - - rw [← hBinsert b₀ (Finset.mem_insert_self b₀ B)] - - let φ := fun z ↦ (∏ a ∈ B, (z - a.1) ^ n a.1) - - have : f = fun z ↦ φ z * g₀ z := by - funext z - rw [h₃g₀ z] - rfl - simp_rw [this] - - have h₁φ : AnalyticAt ℂ φ b₀ := by - dsimp [φ] - apply Finset.analyticAt_prod - intro b _ - apply AnalyticAt.pow - apply AnalyticAt.sub - apply analyticAt_id ℂ - exact analyticAt_const - - have h₂φ : h₁φ.order = (0 : ℕ) := by - rw [AnalyticAt.order_eq_nat_iff h₁φ 0] - use φ - constructor - · assumption - · constructor - · dsimp [φ] - push_neg - rw [Finset.prod_ne_zero_iff] - intro a ha - simp - have : ¬ (b₀.1 - a.1 = 0) := by - by_contra C - rw [sub_eq_zero] at C - rw [SetCoe.ext C] at hb - tauto - tauto - · simp - - rw [AnalyticAt.order_mul h₁φ (h₁g₀ b₀ b₀.2)] - - rw [h₂φ] - simp - - - obtain ⟨g₁, h₁g₁, h₂g₁, h₃g₁⟩ := (AnalyticOn.order_eq_nat_iff h₁g₀ b₀.2 (n b₀)).1 this - - use g₁ - constructor - · exact h₁g₁ - · constructor - · intro a h₁a - by_cases h₂a : a = b₀ - · rwa [h₂a] - · let A' := Finset.mem_of_mem_insert_of_ne h₁a h₂a - let B' := h₃g₁ a - let C' := h₂g₀ a A' - rw [B'] at C' - exact right_ne_zero_of_smul C' - · intro z - let A' := h₃g₀ z - rw [h₃g₁ z] at A' - rw [A'] - rw [← smul_assoc] - congr - simp - rw [Finset.prod_insert] - ring - exact hb - - -theorem XX - {f : ℂ → ℂ} - {U : Set ℂ} - (hU : IsPreconnected U) - (h₁f : AnalyticOn ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∀ (hu : u ∈ U), (h₁f u hu).order.toNat = (h₁f u hu).order := by - - intro hu - apply ENat.coe_toNat - by_contra C - rw [(h₁f u hu).order_eq_top_iff] at C - rw [← (h₁f u hu).frequently_zero_iff_eventually_zero] at C - obtain ⟨u₁, h₁u₁, h₂u₁⟩ := h₂f - rw [(h₁f.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hu C) h₁u₁] at h₂u₁ - tauto - - -theorem discreteZeros - {f : ℂ → ℂ} - {U : Set ℂ} - (hU : IsPreconnected U) - (h₁f : AnalyticOn ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - DiscreteTopology ↑(U ∩ f⁻¹' {0}) := by - - simp_rw [← singletons_open_iff_discrete] - simp_rw [Metric.isOpen_singleton_iff] - - intro z - - let A := XX hU h₁f h₂f z.2.1 - rw [eq_comm] at A - rw [AnalyticAt.order_eq_nat_iff] at A - obtain ⟨g, h₁g, h₂g, h₃g⟩ := A - - rw [Metric.eventually_nhds_iff_ball] at h₃g - have : ∃ ε > 0, ∀ y ∈ Metric.ball (↑z) ε, g y ≠ 0 := by - have h₄g : ContinuousAt g z := AnalyticAt.continuousAt h₁g - have : {0}ᶜ ∈ nhds (g z) := 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 - intro h₁y - - have h₂y : ↑y ∈ Metric.ball (↑z) ε₂ := by - simp - calc dist y z - _ < min ε₁ ε₂ := by assumption - _ ≤ ε₂ := by exact min_le_right ε₁ ε₂ - - have h₃y : ↑y ∈ Metric.ball (↑z) ε₁ := by - simp - calc dist y z - _ < min ε₁ ε₂ := by assumption - _ ≤ ε₁ := by exact min_le_left ε₁ ε₂ - - - have F := h₂ε₂ y.1 h₂y - rw [y.2.2] at F - simp at F - - have : g y.1 ≠ 0 := by - exact h₁ε₁.2 y h₃y - simp [this] at F - ext - rw [sub_eq_zero] at F - tauto - - -theorem finiteZeros - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) - (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - Set.Finite ↑(U ∩ f⁻¹' {0}) := by - - have hinter : IsCompact ↑(U ∩ f⁻¹' {0}) := by - apply IsCompact.of_isClosed_subset h₂U - apply h₁f.continuousOn.preimage_isClosed_of_isClosed - exact IsCompact.isClosed h₂U - exact isClosed_singleton - exact Set.inter_subset_left - - apply hinter.finite - apply DiscreteTopology.of_subset (s := ↑(U ∩ f⁻¹' {0})) - exact discreteZeros h₁U h₁f h₂f - rfl - - -theorem AnalyticOnCompact.eliminateZeros - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) - (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ 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 a a.2).order.toNat) • g z := by - - let ι : U → ℂ := Subtype.val - - let A₁ := ι⁻¹' (U ∩ f⁻¹' {0}) - - have : A₁.Finite := by - apply Set.Finite.preimage - exact Set.injOn_subtype_val - exact finiteZeros h₁U h₂U h₁f h₂f - let A := this.toFinset - - let n : ℂ → ℕ := by - intro z - by_cases hz : z ∈ U - · exact (h₁f z hz).order.toNat - · exact 0 - - have hn : ∀ a ∈ A, (h₁f a a.2).order = n a := by - intro a _ - dsimp [n] - simp - 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 - use g - use A - - have inter : ∀ (z : ℂ), f z = (∏ a ∈ A, (z - ↑a) ^ (h₁f (↑a) a.property).order.toNat) • g z := by - intro z - rw [h₃g z] - congr - funext a - congr - dsimp [n] - simp [a.2] - - constructor - · exact h₁g - · constructor - · intro z h₁z - by_cases h₂z : ⟨z, h₁z⟩ ∈ ↑A.toSet - · exact h₂g ⟨z, h₁z⟩ h₂z - · have : f z ≠ 0 := by - by_contra C - have : ⟨z, h₁z⟩ ∈ ↑A₁ := by - dsimp [A₁, ι] - simp - exact C - have : ⟨z, h₁z⟩ ∈ ↑A.toSet := by - dsimp [A] - simp - exact this - tauto - rw [inter z] at this - exact right_ne_zero_of_smul this - · exact inter - - -noncomputable def AnalyticOn.order - {f : ℂ → ℂ} - {U : Set ℂ} - (hf : AnalyticOn ℂ f U) : - ℂ → ℕ∞ := by - intro z - if hz : z ∈ U then - exact (hf z hz).order - else - exact 0 - - -theorem AnalyticOnCompact.eliminateZeros₁ - {f : ℂ → ℂ} - {U : Set ℂ} - (h₁U : IsPreconnected U) - (h₂U : IsCompact U) - (h₁f : AnalyticOn ℂ f U) - (h₂f : ∃ u ∈ U, f u ≠ 0) : - ∃ (g : ℂ → ℂ), AnalyticOn ℂ g U ∧ (∀ z ∈ U, g z ≠ 0) ∧ ∀ z, f z = (∏ᶠ u, (z - u) ^ (h₁f.order u).toNat) • g z := by - - obtain ⟨g, A, h₁g, h₂g, h₃g⟩ := AnalyticOnCompact.eliminateZeros h₁U h₂U h₁f h₂f - - use g - constructor - · exact h₁g - · constructor - · exact h₂g - · intro z - rw [h₃g z] - congr - - sorry diff --git a/Nevanlinna/holomorphic_JensenFormula2.lean b/Nevanlinna/holomorphic_JensenFormula2.lean index a267992..79959d0 100644 --- a/Nevanlinna/holomorphic_JensenFormula2.lean +++ b/Nevanlinna/holomorphic_JensenFormula2.lean @@ -77,16 +77,29 @@ noncomputable def order theorem jensen_case_R_eq_one (f : ℂ → ℂ) (h₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt f z) - (h'₁f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, AnalyticAt ℂ f z) + (h'₁f : AnalyticOn ℂ f (Metric.closedBall (0 : ℂ) 1)) (h₂f : f 0 ≠ 0) : - log ‖f 0‖ = -∑ s : (ZeroFinset h₁f h₂f), order s * log (‖s.1‖⁻¹) + (2 * π )⁻¹ * ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ := by + log ‖f 0‖ = -∑ᶠ s, (h'₁f.order s).toNat * log (‖s.1‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by - have F : ℂ → ℂ := by sorry - have h₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by sorry - have h₂F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, F z ≠ 0 := by sorry - have h₃F : f = fun z ↦ (F z) * ∏ s : ZeroFinset h₁f h₂f, (z - s) ^ (order s) := by sorry + have h₁U : IsPreconnected (Metric.closedBall (0 : ℂ) 1) := by + apply IsConnected.isPreconnected + apply Convex.isConnected + exact convex_closedBall 0 1 + exact Set.nonempty_of_nonempty_subtype - let G := fun z ↦ log ‖F z‖ + ∑ s : ZeroFinset h₁f h₂f, (order s) * log ‖z - s‖ + have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) := isCompact_closedBall 0 1 + + 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 + + have h'₁F : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, HolomorphicAt F z := by + sorry + + let G := fun z ↦ log ‖F z‖ + ∑ s ∈ (finiteZeros h₁U h₂U h'₁f h'₂f).toFinset, (h'₁f.order s).toNat * log ‖z - s‖ have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by intro z h₁z h₂z @@ -95,9 +108,10 @@ theorem jensen_case_R_eq_one left arg 1 rw [h₃F] + rw [smul_eq_mul] rw [norm_mul] rw [norm_prod] - right + left arg 2 intro b rw [norm_pow] @@ -106,13 +120,15 @@ theorem jensen_case_R_eq_one rw [Real.log_prod] conv => left - right + left arg 2 intro s rw [Real.log_pow] dsimp [G] + abel -- ∀ x ∈ (ZeroFinset h₁f).attach, Complex.abs (z - ↑x) ^ order x ≠ 0 + simp intro s hs rw [ZeroFinset_mem_iff h₁f s] at hs @@ -153,6 +169,7 @@ theorem jensen_case_R_eq_one apply finiteZeros -- IsPreconnected (Metric.closedBall (0 : ℂ) 1) + apply IsConnected.isPreconnected apply Convex.isConnected exact convex_closedBall 0 1