Complex.Hadamard.hadamard_factorization_of_growth

theorem hadamard_factorization_of_growth {f : ℂ → ℂ} {ρ : ℝ} (hρ : 0 ≤ ρ)    (hentire : Differentiable ℂ f)    (hnot : ∃ z : ℂ, f z ≠ 0)    (hgrowth : ∃ C > 0, ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ C * (1 + ‖z‖) ^ ρ) :    ∃ (P : Polynomial ℂ),      P.degree ≤ Nat.floor ρ ∧      ∀ z : ℂ,        f z =          Complex.exp (Polynomial.eval z P) *            z ^ (analyticOrderNatAt f 0) *            divisorCanonicalProduct (Nat.floor ρ) f (Set.univ : Set ℂ) z := by  set m : ℕ := Nat.floor ρ  have h_sum :      Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>        ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)) := by    simpa [m] using      (summable_norm_inv_pow_divisorZeroIndex₀_of_growth (f := f) (ρ := ρ)        hρ hentire hnot hgrowth)  rcases exists_entire_nonzero_hadamardQuotient (m := m) (f := f) hentire hnot h_sum with    ⟨H, hH_entire, hH_ne, hfactor⟩  rcases Real.exists_between_self_and_floor_add_one_same_floor hρ with    ⟨τ, hτ, hτ_lt, hτ_nonneg, hfloorτ'⟩  have hfloorτ : Nat.floor τ = m := by    simpa [m] using hfloorτ'  have hτ_lt_m : τ < (m + 1 : ℝ) := by    simpa [m] using hτ_lt  have hτ_lt_nat : τ < ((m + 1 : ℕ) : ℝ) := by    simpa [Nat.cast_add, Nat.cast_one] using hτ_lt_m  have hmρ : (m : ℝ) ≤ ρ := by    have := Nat.floor_le hρ    simpa [m] using this  have hH_bound_rpow :      ∃ C > 0, ∀ z : ℂ, ‖H z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ τ) :=    hadamardQuotient_norm_le_exp_rpow_of_growth (f := f) (H := H) (ρ := ρ) (τ := τ)      (m := m) hρ hmρ hτ hτ_lt hτ_nonneg hentire hH_entire hnot h_sum hgrowth hfactor  have hH_growth_nat :      ∃ C > 0, ∀ z : ℂ, ‖H z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ (m + 1)) := by    exact Real.exists_norm_le_exp_mul_pow_of_rpow_bound      (f := H) (r := fun z : ℂ => 1 + ‖z‖)      (fun z => by linarith [norm_nonneg z]) hτ_lt_nat hH_bound_rpow  rcases zero_free_polynomial_growth_is_exp_poly (H := H) (n := m + 1)      hH_entire hH_ne hH_growth_nat with    ⟨P, hPn, hHP⟩  have hPnat : P.natDegree ≤ m := by    have hbound :        ∃ C > 0, ∀ z : ℂ,          ‖Complex.exp (Polynomial.eval z P)‖ ≤ Real.exp (C * (1 + ‖z‖) ^ τ) := by      rcases hH_bound_rpow with ⟨C, hCpos, hC⟩      exact ⟨C, hCpos, fun z => by simpa [hHP z] using (hC z)⟩    have := natDegree_le_floor_of_exp_eval_norm_bound hτ_nonneg P hbound    simpa [hfloorτ] using this  refine ⟨P, ?_, ?_⟩  · have : P.degree ≤ m := Polynomial.degree_le_of_natDegree_le hPnat    simpa [m] using this  · intro z    have hH' : H z = Complex.exp (Polynomial.eval z P) := by simpa using (hHP z)    simpa [hH', mul_assoc, mul_left_comm, mul_comm, m] using (hfactor z)