Complex.Hadamard.hadamardQuotient_norm_le_exp_rpow_of_growth

theorem hadamardQuotient_norm_le_exp_rpow_of_growth {f H : ℂ → ℂ} {ρ τ : ℝ} {m : ℕ}    (hρ : 0 ≤ ρ) (hmρ : (m : ℝ) ≤ ρ) (hτ : ρ < τ) (hτ_lt : τ < (m + 1 : ℝ))    (hτ_nonneg : 0 ≤ τ) (hentire : Differentiable ℂ f) (hH_entire : Differentiable ℂ H)    (hnot : ∃ z : ℂ, f z ≠ 0)    (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>      ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1)))    (hgrowth : ∃ C > 0, ∀ z : ℂ, Real.log (1 + ‖f z‖) ≤ C * (1 + ‖z‖) ^ ρ)    (hfactor : ∀ z : ℂ,      f z =        H z * z ^ analyticOrderNatAt f 0 *          divisorCanonicalProduct m f (Set.univ : Set ℂ) z) :    ∃ C > 0, ∀ z : ℂ, ‖H z‖ ≤ Real.exp (C * (1 + ‖z‖) ^ τ) := by  rcases hgrowth with ⟨Cf, hCfpos, hCf⟩  have hsumτ :      Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) =>        ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ) :=    summable_norm_inv_rpow_divisorZeroIndex₀_of_growth (f := f) (ρ := ρ) (τ := τ)      hρ hτ hentire hnot ⟨Cf, hCfpos, hCf⟩  let Sτ : ℝ := ∑' p : divisorZeroIndex₀ f (Set.univ : Set ℂ), ‖divisorZeroIndex₀_val p‖⁻¹ ^ τ  have hSτ_nonneg : 0 ≤ Sτ := tsum_nonneg fun _ =>    Real.rpow_nonneg (inv_nonneg.2 (norm_nonneg _)) _  let Cprod : ℝ := cartanProductConstant m τ Sτ  have hCprod_nonneg : 0 ≤ Cprod := by    simpa [Cprod] using cartanProductConstant_nonneg (m := m) (τ := τ) hSτ_nonneg  have hf_boundτ : ∀ z : ℂ, ‖f z‖ ≤ Real.exp (Cf * (1 + ‖z‖) ^ τ) :=    Real.norm_le_exp_mul_rpow_of_log_growth      (f := f) (r := fun z : ℂ => 1 + ‖z‖) (C := Cf) (ρ := ρ) (τ := τ)      hCfpos.le (fun z => by linarith [norm_nonneg z]) (le_of_lt hτ) hCf  refine ⟨(Cf + Cprod + 10) * (3 : ℝ) ^ τ, by    have h3τ : 0 < (3 : ℝ) ^ τ := by positivity    nlinarith [hCfpos, hCprod_nonneg, h3τ], ?_⟩  intro z  let R : ℝ := max ‖z‖ 1  have hRpos : 0 < R := lt_of_lt_of_le (by norm_num) (le_max_right _ _)  have hRle : (1 : ℝ) ≤ R := le_max_right _ _  let smallSet : Set (divisorZeroIndex₀ f (Set.univ : Set ℂ)) :=    {p | ‖divisorZeroIndex₀_val p‖ ≤ 4 * R}  have hsmall_fin : smallSet.Finite := by    have : Metric.closedBall (0 : ℂ) (4 * R) ⊆ (Set.univ : Set ℂ) := by simp    simpa [smallSet] using      (divisorZeroIndex₀_norm_le_finite (f := f) (U := (Set.univ : Set ℂ))        (B := 4 * R) this)  let small : Finset (divisorZeroIndex₀ f (Set.univ : Set ℂ)) := hsmall_fin.toFinset  let a : divisorZeroIndex₀ f (Set.univ : Set ℂ) → ℝ := fun p => ‖divisorZeroIndex₀_val p‖  have ha_pos : ∀ p ∈ small, 0 < a p := by    intro p hp    exact norm_pos_iff.2 (divisorZeroIndex₀_val_ne_zero p)  let bad : Finset ℝ := small.image a  rcases CartanBound.exists_radius_Ioc_sum_mul_phi_div_le_Cφ_mul_sum_avoid      (s := small) (w := fun _ => (1 : ℝ)) (a := a)      (hw := by intro _ _; norm_num) (ha := ha_pos) (bad := bad) (R := R) hRpos with    ⟨r, hr_mem, hr_not_bad, hr_phi⟩  have hR_le_r : R ≤ r := le_of_lt hr_mem.1  have hr_le_2R : r ≤ 2 * R := hr_mem.2  have hrpos : 0 < r := lt_of_lt_of_le hRpos hR_le_r  have hcircle :      ∀ u : ℂ, ‖u‖ = r → ‖H u‖ ≤ Real.exp ((Cf + Cprod + 10) * (1 + r) ^ τ) := by    simpa [Sτ, Cprod] using      (hadamardQuotient_norm_le_exp_on_cartan_circle        (f := f) (H := H) (ρ := ρ) (τ := τ) (m := m) (Cf := Cf)        hmρ hτ hτ_lt hτ_nonneg hentire hnot h_sum hsumτ hf_boundτ hfactor        (R := R) (r := r) hRpos hRle hR_le_r hr_le_2R hrpos        smallSet hsmall_fin (by rfl)        (by simpa [small, a, bad] using hr_not_bad)        (by simpa [small, a, one_mul, Finset.sum_const, nsmul_eq_mul] using hr_phi))  have hz_ball : z ∈ Metric.ball (0 : ℂ) r := by    rw [Metric.mem_ball, dist_zero_right]    exact lt_of_le_of_lt (le_max_left _ _) hr_mem.1  have hball :      ‖H z‖ ≤ Real.exp ((Cf + Cprod + 10) * (1 + r) ^ τ) := by    exact Complex.norm_le_of_mem_ball_of_forall_sphere_norm_le hH_entire hrpos hz_ball hcircle  have hr_le_3 : 1 + r ≤ 3 * (1 + ‖z‖) := by    exact Real.one_add_le_three_mul_one_add_of_le_two_mul_max (norm_nonneg z)      (by simpa [R] using hr_le_2R)  have hmain :      Real.exp ((Cf + Cprod + 10) * (1 + r) ^ τ)        ≤ Real.exp (((Cf + Cprod + 10) * (3 : ℝ) ^ τ) * (1 + ‖z‖) ^ τ) := by    have hnn : 0 ≤ (Cf + Cprod + 10) := by nlinarith [le_of_lt hCfpos, hCprod_nonneg]    exact Real.exp_mul_rpow_le_exp_mul_rpow_of_le_mul hnn (by norm_num)      (by linarith [le_of_lt hrpos]) (by positivity) hτ_nonneg hr_le_3  simpa [mul_assoc] using hball.trans hmain