CH2.Phi_circ.poles

@[blueprint  "Phi-circ-poles"  (title := "$\\Phi^{\\pm,\\circ}_\\nu$ poles")  (statement := /--  The poles of $$\Phi^{\pm,\circ}_\nu(z)$$ are of the form $n - i \nu/2\pi$ for $n \in \mathbb{Z}$.  -/)  (proof := /-- This follows from the definition of $\Phi^{\pm,\circ}_\nu$ and the properties of the $\coth$ function. -/)  (latexEnv := "lemma")  (discussion := 1069)]theorem Phi_circ.poles (ν ε : ℝ) (_hν : ν > 0) (z : ℂ) :    meromorphicOrderAt (Phi_circ ν ε) z < 0 ↔ ∃ n : ℤ, z = n - I * ν / (2 * π) := by  -- Step 1: Reduce Phi_circ to coth (w/2)  let w : ℂ → ℂ := fun z ↦ -2 * π * I * z + ν  have h_ord_eq : meromorphicOrderAt (Phi_circ ν ε) z < 0 ↔ meromorphicOrderAt (fun z ↦ coth (w z / 2)) z < 0 := by    rw [show Phi_circ ν ε = (fun _ ↦ (1 / 2 : ℂ)) * (fun z ↦ coth (w z / 2) + ε) from rfl]    rw [meromorphicOrderAt_mul_of_ne_zero (analyticAt_const (v := (1/2 : ℂ)) (x := z)) (by norm_num : (1/2 : ℂ) ≠ 0)]    have h_coth_mero : MeromorphicAt (fun z ↦ coth (w z / 2)) z := by fun_prop    constructor    · intro h      contrapose! h      have h_sum := meromorphicOrderAt_add h_coth_mero (MeromorphicAt.const (ε : ℂ) z)      rw [meromorphicOrderAt_const] at h_sum      split_ifs at h_sum with h_eps      · simp_all [gt_iff_lt, add_zero, le_top, inf_of_le_left]      · exact (le_min (by simpa using h) le_rfl).trans h_sum    · intro h      have h_ne : meromorphicOrderAt (fun z ↦ coth (w z / 2)) z ≠ meromorphicOrderAt (fun _ ↦ (ε : ℂ)) z := by        rw [meromorphicOrderAt_const]; split_ifs <;> simp [h.ne_top, h.ne]      rw [show (fun z ↦ coth (w z / 2) + ε) = (fun z ↦ coth (w z / 2)) + (fun _ ↦ (ε : ℂ)) from rfl]      rw [meromorphicOrderAt_add_of_ne h_coth_mero (by fun_prop) h_ne]      simp [h]  -- Step 2: Apply "pole of coth iff zero of sinh" via composition  have h_pole_iff : meromorphicOrderAt (fun z ↦ coth (w z / 2)) z < 0 ↔ (Complex.sinh (w z / 2) = 0) := by    have h_mero_w : AnalyticAt ℂ (fun z => w z / 2) z := by dsimp [w]; fun_prop    have h_deriv_w : deriv (fun z => w z / 2) z ≠ 0 := by      have hd : HasDerivAt (fun z : ℂ ↦ w z / 2) (-π * I) z := by        convert! (((hasDerivAt_id z).const_mul (-2 * π * I)).add (hasDerivAt_const z (ν:ℂ))).div_const 2 using 1        ring      rw [hd.deriv]; simp [pi_ne_zero, I_ne_zero]    have h_comp : meromorphicOrderAt (fun z ↦ coth (w z / 2)) z = meromorphicOrderAt coth (w z / 2) :=      meromorphicOrderAt_comp_of_deriv_ne_zero (f := coth) h_mero_w h_deriv_w    rw [h_comp]    exact meromorphicOrderAt_coth_lt_zero_iff _  -- Step 3: Rewrite with sinh_zero_iff and solve the linear equation  rw [h_ord_eq, h_pole_iff, sinh_zero_iff]  constructor  · rintro ⟨k, hk⟩    use -k    apply (mul_left_inj' (show (2 * π * I : ℂ) ≠ 0 by simp [pi_ne_zero])).mp    field_simp [pi_ne_zero, I_ne_zero] at hk ⊢    have h1 : 2 * π * I * z = ν - 2 * k * π * I := by rw [← hk]; dsimp [w]; ring    calc      (2 * π * z : ℂ) = (2 * π * I * z) * (-I) := by ring_nf; simp      _ = (ν - 2 * k * π * I) * (-I) := by rw [h1]      _ = 2 * k * π * Complex.I^2 - I * ν := by ring      _ = 2 * π * ↑(-k) - I * ν := by simp; ring  · rintro ⟨n, rfl⟩    use -n    dsimp [w]    field_simp [pi_ne_zero, I_ne_zero]    ring_nf    simp