mkComplexCarrierCert

formal source

  65
  66/-- Construct a `ComplexCarrierCert` for any point `σ₀ > 1/2` on the real axis.
  67The disk has center `σ₀` and radius `σ₀ − 1/2`, reaching the critical line. -/
  68noncomputable def mkComplexCarrierCert (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
  69    ComplexCarrierCert where
  70  center := (σ₀ : ℂ)
  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. -/
  95noncomputable def contourWinding (_cert : ComplexCarrierCert) (_r : ℝ) : ℤ := 0
  96
  97/-- The carrier has zero winding around every circle inside the disk.
  98