E1_zero

formal source

  37/-- The genus-one elementary Weierstrass factor `E₁(z) = (1 - z) · exp(z)`. -/
  38def E1 (z : ℂ) : ℂ := (1 - z) * Complex.exp z
  39
  40@[simp] theorem E1_zero : E1 0 = 1 := by simp [E1]
  41
  42theorem E1_one : E1 1 = 0 := by simp [E1]
  43
  44/-- Algebraic identity `E₁(z) - 1 = (exp z - 1 - z) - z (exp z - 1)`. -/
  45theorem E1_sub_one_eq (z : ℂ) :
  46    E1 z - 1 = (Complex.exp z - 1 - z) - z * (Complex.exp z - 1) := by
  47  unfold E1
  48  have hz : Complex.exp z = 1 + (Complex.exp z - 1) := by ring
  49  conv_lhs => rw [hz]
  50  ring
  51
  52/-! ## 2. The per-factor estimate -/
  53
  54/-- `‖exp z - 1‖ ≤ 2 ‖z‖` for `‖z‖ ≤ 1`. -/
  55private theorem norm_exp_sub_one_le_two_mul (z : ℂ) (hz : ‖z‖ ≤ 1) :
  56    ‖Complex.exp z - 1‖ ≤ 2 * ‖z‖ := by
  57  have h1 : ‖Complex.exp z - 1 - z‖ ≤ ‖z‖ ^ 2 :=
  58    Complex.norm_exp_sub_one_sub_id_le hz
  59  have hzn : 0 ≤ ‖z‖ := norm_nonneg z
  60  have hsq : ‖z‖ ^ 2 ≤ ‖z‖ := by
  61    have := mul_le_mul_of_nonneg_left hz hzn
  62    have heq : ‖z‖ * ‖z‖ = ‖z‖ ^ 2 := by ring
  63    rw [heq] at this
  64    have : ‖z‖ * 1 = ‖z‖ := by ring
  65    linarith [this]
  66  calc
  67    ‖Complex.exp z - 1‖
  68        = ‖(Complex.exp z - 1 - z) + z‖ := by ring_nf
  69    _ ≤ ‖Complex.exp z - 1 - z‖ + ‖z‖ := norm_add_le _ _
  70    _ ≤ ‖z‖ ^ 2 + ‖z‖ := by linarith