Complex.Hadamard.hasProdUniformlyOn_divisorComplementCanonicalProduct_univ

theorem hasProdUniformlyOn_divisorComplementCanonicalProduct_univ    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) {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 : ℂ) =>        divisorComplementFactor m f z₀ p z) (divisorComplementCanonicalProduct m f z₀)      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 term : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℂ → ℂ := fun p z =>    divisorComplementFactor m f z₀ p z  let g : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℂ → ℂ := fun p z => term p z - 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    by_cases hpF : p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀    · have hval : divisorZeroIndex₀_val p = z₀ :=        (mem_divisorZeroIndex₀_fiberFinset (f := f) (z₀ := z₀) p).1 hpF      have hu0 : 0 ≤ u p := by        dsimp [u]        refine mul_nonneg ?_ ?_        · nlinarith [pow_nonneg (show 0 ≤ R from le_of_lt hRpos) (m + 1)]        · exact pow_nonneg (inv_nonneg.2 (norm_nonneg _)) (m + 1)      simp [g, term, divisorComplementFactor, hval, hu0, sub_eq_add_neg]    · have hzle : ‖z‖ ≤ R := hnormK z hzK      have hz_div : ‖z / divisorZeroIndex₀_val p‖ ≤ (1 / 2 : ℝ) := by        have h2R_pos : 0 < (2 * R : ℝ) := by nlinarith [hRpos]        have hinv : ‖divisorZeroIndex₀_val p‖⁻¹ < (2 * R)⁻¹ := by          simpa [one_div] using (one_div_lt_one_div_of_lt h2R_pos hp)        have hmul_le : ‖z‖ * ‖divisorZeroIndex₀_val p‖⁻¹ ≤ R * ‖divisorZeroIndex₀_val p‖⁻¹ := by          refine mul_le_mul_of_nonneg_right hzle ?_          exact inv_nonneg.2 (norm_nonneg _)        have hmul_lt : R * ‖divisorZeroIndex₀_val p‖⁻¹ < R * (2 * R)⁻¹ :=          mul_lt_mul_of_pos_left hinv hRpos        have hlt : ‖z‖ * ‖divisorZeroIndex₀_val p‖⁻¹ < R * (2 * R)⁻¹ :=          lt_of_le_of_lt hmul_le hmul_lt        have hRhalf : R * (2 * R)⁻¹ = (1 / 2 : ℝ) := by          have hRne : (R : ℝ) ≠ 0 := hRpos.ne'          have : R * (2 * R)⁻¹ = R / (2 * R) := by simp [div_eq_mul_inv]          rw [this]          field_simp [hRne]        have hnorm : ‖z / divisorZeroIndex₀_val p‖ = ‖z‖ * ‖divisorZeroIndex₀_val p‖⁻¹ := by          simp [div_eq_mul_inv]        have hzlt : ‖z / divisorZeroIndex₀_val p‖ < (1 / 2 : ℝ) := by          calc            ‖z / divisorZeroIndex₀_val p‖ = ‖z‖ * ‖divisorZeroIndex₀_val p‖⁻¹ := hnorm            _ < R * (2 * R)⁻¹ := hlt            _ = (1 / 2 : ℝ) := hRhalf        exact le_of_lt hzlt      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, term, u]      simp [divisorComplementFactor, hpF] at *      nlinarith [hE, hz_pow]  have hcts : ∀ p, ContinuousOn (g p) K := by    intro p    by_cases hpF : p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀    · have hval : divisorZeroIndex₀_val p = z₀ :=        (mem_divisorZeroIndex₀_fiberFinset (f := f) (z₀ := z₀) p).1 hpF      simpa [g, term, divisorComplementFactor, hval, sub_eq_add_neg, add_assoc, add_left_comm,        add_comm] using        (continuousOn_const : ContinuousOn (fun _ : ℂ => (0 : ℂ)) K)    · have hvalne : divisorZeroIndex₀_val p ≠ z₀ :=        (not_mem_divisorZeroIndex₀_fiberFinset_iff_val_ne (f := f) z₀ p).1 hpF      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      have : ContinuousOn (fun z : ℂ => weierstrassFactor m (z / divisorZeroIndex₀_val p) - 1) K :=        (hcont.continuousOn.sub continuous_const.continuousOn)      simpa [g, term, divisorComplementFactor, mem_divisorZeroIndex₀_fiberFinset, hvalne] using this  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  have hterm :      HasProdUniformlyOn (fun p z ↦ term p z) (fun z ↦ ∏' p, term p z) K := by    simpa [g, sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using hprod  refine hterm.congr_right ?_  intro z hz  simp [term, divisorComplementCanonicalProduct, divisorComplementFactor]