CH2.CH2_lemma_4_2a

@[blueprint  "CH2-lemma-4-2a"  (title := "CH2 Lemma 4.2(a)")  (statement := /--If $|\Im z| \leq \frac{\pi}{4}$, then $|(z \coth z)'| < 1$.  -/)  (proof := /-- Since $z\coth(z)$ is regular at $0$ and an even function, we see that $f(z) := (z \coth z)'$ and $f(z)/z$ are regular at $0$, and hence analytic on the strip $|\Im z| \leq \frac{\pi}{2}$. We see from $f(z) = \coth z - z\operatorname{csch}^2 z$ that $f(z)$ has at most exponential growth as $\Re z \to \pm\infty$ within the strip. Hence, by Phragm\'{e}n--Lindel\"{o}f, it is enough to verify the inequalities $|f(z)/z| \leq 1$ for $\Im z = \pm\frac{\pi}{2}$ and $|f(z)| \leq 1$ for $\Im z = \pm\frac{\pi}{4}$; by complex conjugation, it suffices to check them for $\Im z = \frac{\pi}{2}$ and $\Im z = \frac{\pi}{4}$. By the above, $f(z) = \frac{(\sinh 2z)/2 - z}{\sinh^2 z}$. Now, for $z = x + i\frac{\pi}{4}$ with $x \in \mathbb{R}$, we have $\sinh 2z = i\cosh 2x$ and $\sinh^2 z = -\frac{1}{2} + \frac{i}{2}\sinh 2x$, and so $|f(z)|^2 = \frac{(\cosh 2x - \pi/2)^2 + 4x^2}{1 + \sinh^2 2x}$. By $1 + \sinh^2 2x = \cosh^2 2x$,\[|f(z)|^2 = 1 - \frac{\pi \cosh 2x - \pi^2/4 - 4x^2}{\cosh^2 2x}.\]Since $\cosh 2x = 1 + 2\sinh^2 x \geq 1 + 2x^2$, $\pi > \frac{\pi^2}{4}$ and $2\pi > 4$, the numerator here is positive. We conclude that $|f(z)|^2 < 1$ for $z = x + i\frac{\pi}{4}$, as was desired. For $z = x + i\frac{\pi}{2}$ with $x \in \mathbb{R}$, we have $\coth z = \tanh x$ and $\operatorname{csch}^2 z = -\operatorname{sech}^2 x$. Then $|f(z)|^2 = (\tanh x + x\operatorname{sech}^2 x)^2 + \left(\frac{\pi}{2}\operatorname{sech}^2 x\right)^2$. Since $\operatorname{sech}^2 x - 1 = -\tanh^2 x$, this is equal to\[\tanh^2 x \operatorname{sech} x\!\left(\cosh x + 2x\operatorname{csch} x - |z|^2(\operatorname{sech} x + \cosh x)\right) + |z|^2.\]Since $|z|^2 \geq \frac{\pi^2}{4} > 2$, it suffices to show that $2x\operatorname{csch} x - 2\operatorname{sech} x - \cosh x \leq 0$ for all $x \in \mathbb{R}$; by parity, it is enough to check all $x \geq 0$. The statement is then equivalent to $g(x) = 2x - 2\tanh x - \sinh x \cosh x \leq 0$, since $\sinh x \geq 0$. That follows from $g'(x) = 2\tanh^2 x - \cosh^2 x - \sinh^2 x = -2\sinh^2 x \tanh^2 x - 1 \leq 0$ (by $1 - \cosh^2 x = -\sinh^2 x$) and $g(0) = 0$.-/)  (latexEnv := "sublemma")  (discussion := 1233)]theorem CH2_lemma_4_2a (z : ℂ) (hz : |z.im| ≤ π / 4) : ‖deriv (fun z:ℂ ↦ z * coth z) z‖ < 1 := by  set f := fun w : ℂ ↦ deriv (fun z : ℂ ↦ z * coth z) w  have h_at_zero : f 0 = 0 := deriv_z_coth_z_at_zero  have h_le_one : ‖f z‖ ≤ 1 := deriv_z_coth_z_le_one z hz  have h_ne_one : ‖f z‖ ≠ 1 := by    intro h_eq    by_cases h_bdy : |z.im| = π / 4    · linarith [deriv_z_coth_z_lt_one_of_abs_im_eq z h_bdy]    · have h_int : |z.im| < π / 4 := lt_of_le_of_ne hz h_bdy      let U := Complex.im ⁻¹' Set.Ioo (-π / 4) (π / 4)      have hU_conn : IsPreconnected U := isPreconnected_im_preimage_Ioo _ _      have hU_open : IsOpen U := isOpen_Ioo.preimage Complex.continuous_im      have hf_diff : DifferentiableOn ℂ f U := differentiableOn_deriv_z_coth_z_strip      have hzU : z ∈ U := by        simp only [U, Set.mem_preimage, Set.mem_Ioo, abs_lt] at *        constructor <;> linarith      have hf_max : IsMaxOn (norm ∘ f) U z := by        intro w hw; dsimp [Function.comp]; rw [h_eq]        apply deriv_z_coth_z_le_one w        simp only [U, Set.mem_preimage, Set.mem_Ioo] at hw        rw [abs_le]; constructor <;> linarith      have hf_const : Set.EqOn f (fun _ ↦ f z) U :=        eqOn_of_isPreconnected_of_isMaxOn_norm hU_conn hU_open hf_diff hzU hf_max      have h_0_in_U : (0 : ℂ) ∈ U := by simp [U]; constructor <;> linarith [Real.pi_pos]      have h_norm_zero : ‖f 0‖ = 1 := by rw [hf_const h_0_in_U, h_eq]      rw [h_at_zero, norm_zero] at h_norm_zero; norm_num at h_norm_zero  exact lt_of_le_of_ne h_le_one h_ne_one