71 radius := σ₀ - 1/2 72 radius_pos := by linarith 73 disk_in_strip := by 74 intro s hs 75 simp only [stripHalfPlane, Set.mem_setOf_eq] 76 rw [Metric.mem_ball, Complex.dist_eq] at hs 77 have hre : |s.re - σ₀| ≤ ‖s - ↑σ₀‖ := by 78 calc |s.re - σ₀| 79 = |(s - ↑σ₀).re| := by simp 80 _ ≤ ‖s - ↑σ₀‖ := abs_re_le_norm (s - ↑σ₀) 81 have habs : |s.re - σ₀| < σ₀ - 1/2 := lt_of_le_of_lt hre hs 82 linarith [abs_lt.mp habs] 83 nonvanishing := by intro _ _; trivial 84 logDerivBound_val := 1 85 logDerivBound_pos := by norm_num 86 differentiableOn := True 87 88/-! ### §3. Zero winding from carrier regularity -/ 89 90/-- The contour winding number of a function around a circle. 91 92For a holomorphic function `f` with `f ≠ 0` on a disk, the winding number 93around any interior circle is `(2πi)⁻¹ ∮ f'/f dz`. We define it abstractly 94as an integer associated to a carrier certificate and a radius. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.