CH2.phi_star_affine_periodic

@[blueprint  "phi_star-affine-periodic"  (title := "$\\Phi^{\\pm,\\ast}_\\nu$ affine periodic")  (statement := /-- For any integer $m$,$$ \Phi^{\pm,\star}_{\nu}(z-m) = \Phi^{\pm,\star}_{\nu}(z) + m\, \Phi^{\pm,\circ}_{\nu}(z). $$    -/)  (proof := /-- Follows from previous lemma. -/)  (latexEnv := "sublemma")  (discussion := 1082)]theorem phi_star_affine_periodic (ν ε : ℝ) (hν : ν > 0) (z : ℂ) (m : ℤ)    (hw : -2 * π * I * z + ν ≠ 0)    (hwm : -2 * π * I * (z - m) + ν ≠ 0) :    Phi_star ν ε (z - m) = Phi_star ν ε z + m * Phi_circ ν ε z := by  have hB := B_affine_periodic ν ε hν z m hw hwm  have h_sub : Phi_star ν ε (z - m) =      (B ε (-2 * Real.pi * I * z + ν) +        2 * Real.pi * I * m * Phi_circ ν ε z - B ε ν) /      (2 * Real.pi * I) := by    rw [Phi_star, hB]  have h_def : Phi_star ν ε z =      (B ε (-2 * Real.pi * I * z + ν) - B ε ν) /      (2 * Real.pi * I) := by    simp [Phi_star]  rw [h_sub, h_def]  field_simp  ring