Complex.Hadamard.hasProdUniformlyOn_divisorCanonicalProduct_univ

theorem hasProdUniformlyOn_divisorCanonicalProduct_univ    (m : ℕ) (f : ℂ → ℂ) {K : Set ℂ} (hK : IsCompact K)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) :    HasProdUniformlyOn      (fun (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) (z : ℂ) =>        weierstrassFactor m (z / divisorZeroIndex₀_val p))      (divisorCanonicalProduct m f (Set.univ : Set ℂ)) K := by  rcases (isBounded_iff_forall_norm_le.1 hK.isBounded) with ⟨R0, hR0⟩  set R : ℝ := max R0 1  have hRpos : 0 < R := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_max_right _ _)  have hnormK : ∀ z ∈ K, ‖z‖ ≤ R := fun z hzK => le_trans (hR0 z hzK) (le_max_left _ _)  let g : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℂ → ℂ :=    fun p z => weierstrassFactor m (z / divisorZeroIndex₀_val p) - 1  let u : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ :=    fun p => (4 * R ^ (m + 1)) * (‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))  have hu : Summable u := h_sum.mul_left (4 * R ^ (m + 1))  have h_big :      ∀ᶠ p : divisorZeroIndex₀ f (Set.univ : Set ℂ) in Filter.cofinite,        (2 * R : ℝ) < ‖divisorZeroIndex₀_val p‖ := by    have hfin :        ({p : divisorZeroIndex₀ f (Set.univ : Set ℂ) | ‖divisorZeroIndex₀_val p‖ ≤ 2 * R} :            Set _).Finite := by      have : Metric.closedBall (0 : ℂ) (2 * R) ⊆ (Set.univ : Set ℂ) := by simp      exact divisorZeroIndex₀_norm_le_finite (f := f) (U := (Set.univ : Set ℂ)) (B := 2 * R) this    have := hfin.eventually_cofinite_notMem    filter_upwards [this] with p hp    have : ¬ ‖divisorZeroIndex₀_val p‖ ≤ 2 * R := by simpa using hp    exact lt_of_not_ge this  have hBound :      ∀ᶠ p in Filter.cofinite, ∀ z ∈ K, ‖g p z‖ ≤ u p := by    filter_upwards [h_big] with p hp z hzK    have hzle : ‖z‖ ≤ R := hnormK z hzK    have hz_div : ‖z / divisorZeroIndex₀_val p‖ ≤ (1 / 2 : ℝ) := by      exact norm_div_le_half_of_norm_le_of_two_mul_lt hRpos hzle hp    have hE :        ‖weierstrassFactor m (z / divisorZeroIndex₀_val p) - 1‖ ≤          4 * ‖z / divisorZeroIndex₀_val p‖ ^ (m + 1) :=      weierstrassFactor_sub_one_pow_bound (m := m) (z := z / divisorZeroIndex₀_val p) hz_div    have hz_pow :        ‖z / divisorZeroIndex₀_val p‖ ^ (m + 1) ≤          (R ^ (m + 1)) * (‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)) := by      have : ‖z / divisorZeroIndex₀_val p‖ = ‖z‖ * ‖divisorZeroIndex₀_val p‖⁻¹ := by        simp [div_eq_mul_inv]      rw [this]      have : (‖z‖ * ‖divisorZeroIndex₀_val p‖⁻¹) ^ (m + 1) =          ‖z‖ ^ (m + 1) * (‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)) := by        simp [mul_pow]      rw [this]      have hzle_pow : ‖z‖ ^ (m + 1) ≤ R ^ (m + 1) :=        pow_le_pow_left₀ (norm_nonneg z) hzle (m + 1)      gcongr    dsimp [g, u]    nlinarith [hE, hz_pow]  have hcts : ∀ p, ContinuousOn (g p) K := by    intro p    have hcontE : Continuous (fun z : ℂ => weierstrassFactor m z) :=      (differentiable_weierstrassFactor m).continuous    have hdiv : Continuous fun z : ℂ => z / divisorZeroIndex₀_val p := by      simpa [div_eq_mul_inv] using! (continuous_id.mul continuous_const)    have hcont : Continuous fun z : ℂ => weierstrassFactor m (z / divisorZeroIndex₀_val p) :=      hcontE.comp hdiv    simpa only [g] using hcont.continuousOn.fun_sub continuous_const.continuousOn  have hprod :      HasProdUniformlyOn (fun p z ↦ 1 + g p z) (fun z ↦ ∏' p, (1 + g p z)) K := by    simpa using      Summable.hasProdUniformlyOn_one_add (f := g) (u := u) (K := K) hK hu hBound hcts  simpa [g, divisorCanonicalProduct, sub_eq_add_neg, add_assoc, add_left_comm, add_comm]    using! hprod