CH2.B_affine_periodic

@[blueprint  "B-affine-periodic"  (title := "$B^\\pm$ affine periodic")  (statement := /-- For any integer $m$,$$ B^\pm(w(z-m)) = B^\pm(w(z) + 2\pi i m) = B^\pm(w(z)) + 2\pi i m\, \Phi^{\pm,\circ}_{\nu}(z). $$    -/)  (proof := /-- This follows from the $\pi i$-periodicity of coth. -/)  (latexEnv := "sublemma")  (discussion := 1081)]theorem B_affine_periodic (ν ε : ℝ) (_hν : ν > 0) (z : ℂ) (m : ℤ)    (hw : -2 * π * I * z + ν ≠ 0)    (hwm : -2 * π * I * (z - m) + ν ≠ 0) :    B ε (-2 * π * I * (z - m) + ν) =      B ε (-2 * π * I * z + ν) + 2 * π * I * m * Phi_circ ν ε z := by  unfold B Phi_circ coth  have h_tanh_periodic :      Complex.tanh ((-2 * Real.pi * I * (z - m) + ν) / 2) =        Complex.tanh ((-2 * Real.pi * I * z + ν) / 2) := by    rw [show (-2 * π * I * (z - m) + ν) / 2 =      (-2 * π * I * z + ν) / 2 + π * I * m by ring]    exact tanh_add_int_mul_pi_I _ m  grind