Weierstrass P q expansion

theorem weierstrassP_q_expansion (τ : ℂ) (hτ : 0 < τ.im) (z : ℂ) (hz : 0 < z.im)    (hzτ : z.im < τ.im) :    ℘[periodPair τ hτ.ne'] z =      (2 * (Real.pi : ℂ) * I) ^ 2 * (1 / 12 + XAn (e z) (e τ)) := by  have hq0 : e τ ≠ 0 := e_ne_zero τ  have hu1 : ‖e z‖ < 1 := norm_e_lt_one hz  have hqu : ‖e τ‖ < ‖e z‖ := norm_e_lt_norm_e hzτ  have hq1 : ‖e τ‖ < 1 := hqu.trans hu1  -- Step 1: reindex the lattice sum by `ℤ × ℤ`  have h0 : HasSum (fun p : ℤ × ℤ ↦      ((z - (p.1 * τ + p.2)) ^ 2)⁻¹ - (((p.1 * τ + p.2 : ℂ)) ^ 2)⁻¹)      (℘[periodPair τ hτ.ne'] z) := by    refine hasSum_lattice_prod hτ.ne' (f := fun w ↦ ((z - w) ^ 2)⁻¹ - (w ^ 2)⁻¹) ?_    simpa only [one_div] using (periodPair τ hτ.ne').hasSum_weierstrassP z  -- Step 2: summability of rows (for Fubini)  have hrowsummA : ∀ n : ℤ, Summable fun m : ℤ ↦ ((z - (n * τ + m)) ^ 2)⁻¹ := fun n ↦    (summable_int_inv_pow_sub (z - n * τ) le_rfl).congr fun m ↦ by congr 1; ring  have hrowsummB : ∀ n : ℤ, Summable fun m : ℤ ↦ (((n * τ + m : ℂ)) ^ 2)⁻¹ := fun n ↦    summable_int_inv_pow (n * τ) le_rfl  -- Step 3: evaluate each row; the corrector row `n = 0` is the Basel problem  have hrowval : ∀ n : ℤ,      ∑' m : ℤ, (((z - (n * τ + m)) ^ 2)⁻¹ - (((n * τ + m : ℂ)) ^ 2)⁻¹)      = (2 * (Real.pi : ℂ) * I) ^ 2 * (e τ ^ (-n) * e z / (1 - e τ ^ (-n) * e z) ^ 2)        - ((2 * (Real.pi : ℂ) * I) ^ 2 * (e τ ^ n / (1 - e τ ^ n) ^ 2)            + if n = 0 then (Real.pi : ℂ) ^ 2 / 3 else 0) := by    intro n    rw [Summable.tsum_sub (hrowsummA n) (hrowsummB n), corrector_row_eval hτ n]    congr 1    rw [show ∑' m : ℤ, ((z - (n * τ + m)) ^ 2)⁻¹ = ∑' m : ℤ, (((z - n * τ) - m) ^ 2)⁻¹ from      tsum_congr fun m ↦ by congr 1; ring, tsum_int_inv_pow_sub,      sum_int_inv_sq' _ (im_sub_int_mul_ne_zero hτ hz hzτ n), e_sub_intCast_mul]  -- Step 4: summability of the row values  have hT1 : Summable fun n : ℤ ↦      (2 * (Real.pi : ℂ) * I) ^ 2 * (e τ ^ (-n) * e z / (1 - e τ ^ (-n) * e z) ^ 2) :=    (summable_comp_neg (summable_V hq0 hqu hu1)).mul_left ((2 * (Real.pi : ℂ) * I) ^ 2)  have hT2 : Summable fun n : ℤ ↦      (2 * (Real.pi : ℂ) * I) ^ 2 * (e τ ^ n / (1 - e τ ^ n) ^ 2) :=    Summable.mul_left _ (summable_corr_int hq0 hq1)  have hT3 : Summable fun n : ℤ ↦ (if n = 0 then (Real.pi : ℂ) ^ 2 / 3 else 0) :=    (hasSum_ite_eq (0 : ℤ) ((Real.pi : ℂ) ^ 2 / 3)).summable  -- Step 5: sum the rows (Fubini), identify the two series, and conclude  rw [← h0.tsum_eq, h0.summable.tsum_prod' fun n ↦ (hrowsummA n).sub (hrowsummB n),    tsum_congr hrowval, Summable.tsum_sub hT1 (hT2.add hT3), Summable.tsum_add hT2 hT3,    tsum_mul_left, tsum_mul_left, tsum_ite_eq,    tsum_comp_neg fun n : ℤ ↦ e τ ^ n * e z / (1 - e τ ^ n * e z) ^ 2,    tsum_corr_int hq0 hq1, XAn,    show (2 * (Real.pi : ℂ) * I) ^ 2 = -4 * (Real.pi : ℂ) ^ 2 by      rw [mul_pow, mul_pow, Complex.I_sq]; ring]  ring