Complex.hasProdUniformlyOn_weierstrassFactor_div_of_bound

lemma hasProdUniformlyOn_weierstrassFactor_div_of_bound {K : Set ℂ} (hK : IsCompact K)    {m : ℕ → ℕ} {a : ℕ → ℂ} {R : ℝ}    (hR : ∀ z ∈ K, ‖z‖ ≤ R) (hsmall : ∀ᶠ n in Filter.atTop, R ≤ ‖a n‖ / 2)    (hsumm : Summable (fun n : ℕ ↦ 4 * R ^ (m n + 1) / ‖a n‖ ^ (m n + 1))) :    HasProdUniformlyOn (fun n z ↦ weierstrassFactor (m n) (z / a n))      (fun z ↦ ∏' n, weierstrassFactor (m n) (z / a n)) K := by  have hbound :      ∀ᶠ n in Filter.atTop,        ∀ z ∈ K,          ‖weierstrassFactor (m n) (z / a n) - 1‖ ≤ 4 * R ^ (m n + 1) / ‖a n‖ ^ (m n + 1) := by    filter_upwards [hsmall] with n hn z hz    refine (norm_weierstrassFactor_div_sub_one_le_pow_div (m := m n) ?_).trans ?_    · exact (hR z hz).trans hn    · have hpow : ‖z‖ ^ (m n + 1) ≤ R ^ (m n + 1) :=        pow_le_pow_left₀ (norm_nonneg z) (hR z hz) (m n + 1)      refine div_le_div_of_nonneg_right ?_ (pow_nonneg (norm_nonneg (a n)) _)      exact mul_le_mul_of_nonneg_left hpow (by positivity)  have hcts :      ∀ n, ContinuousOn (fun z ↦ weierstrassFactor (m n) (z / a n) - 1) K := by    intro n    exact (continuousOn_weierstrassFactor_div (m n) (a n) K).fun_sub continuousOn_const  simpa using hsumm.hasProdUniformlyOn_nat_one_add (K := K)    (f := fun n z ↦ weierstrassFactor (m n) (z / a n) - 1) hK hbound hcts