Complex.Hadamard.natDegree_le_floor_of_growth_exp_eval

theorem natDegree_le_floor_of_growth_exp_eval    {ρ : ℝ} (hρ : 0 ≤ ρ) (P : Polynomial ℂ)    (hgrowth :      ∃ C > 0, ∀ z : ℂ,        Real.log (1 + ‖Complex.exp (Polynomial.eval z P)‖) ≤ C * (1 + ‖z‖) ^ ρ) :    P.natDegree ≤ Nat.floor ρ := by  classical  by_cases hdeg : P.natDegree = 0  · simp [hdeg]  · have hnpos : 0 < P.natDegree := Nat.pos_of_ne_zero hdeg    rcases exists_z_norm_eq_re_eval_ge (P := P) hnpos with ⟨R0, hR0pos, hray⟩    rcases hgrowth with ⟨C, hCpos, hC⟩    have hLCpos : 0 < ‖P.leadingCoeff‖ := by      have hP0 : P ≠ 0 := by        intro h0        simp [h0] at hdeg      have : P.leadingCoeff ≠ 0 := (Polynomial.leadingCoeff_ne_zero).2 hP0      exact norm_pos_iff.2 this    let c : ℝ := ‖P.leadingCoeff‖ / 2    have hcpos : 0 < c := by      have : (0 : ℝ) < (2 : ℝ) := by norm_num      exact (div_pos hLCpos this)    have hn_le_real : (P.natDegree : ℝ) ≤ ρ := by      by_contra hnlt      have hnlt' : ρ < (P.natDegree : ℝ) := lt_of_not_ge hnlt      let δ : ℝ := (P.natDegree : ℝ) - ρ      have hδ : 0 < δ := sub_pos.2 hnlt'      let K0 : ℝ := (C * (2 : ℝ) ^ ρ) / c      have hK0 : ∃ R1, ∀ R ≥ R1, K0 + 1 ≤ R ^ δ := by        have h : ∀ᶠ R in (atTop : Filter ℝ), K0 + 1 ≤ R ^ δ :=          (tendsto_atTop.mp (tendsto_rpow_atTop hδ)) (K0 + 1)        rcases (eventually_atTop.1 h) with ⟨R1, hR1⟩        exact ⟨R1, hR1⟩      rcases hK0 with ⟨R1, hR1⟩      set R : ℝ := max (max R0 1) R1      have hR_ge_R0 : R0 ≤ R := le_trans (le_max_left _ _) (le_max_left _ _)      have hR_ge1 : (1 : ℝ) ≤ R := le_trans (le_max_right _ _) (le_max_left _ _)      have hR_ge_R1 : R1 ≤ R := le_max_right _ _      have hR_pos : 0 < R := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) hR_ge1      have hRδ : K0 + 1 ≤ R ^ δ := hR1 R hR_ge_R1      rcases hray R hR_ge_R0 with ⟨z, hz_norm, hz_re⟩      have hlog_lower :          (P.eval z).re ≤ Real.log (1 + ‖Complex.exp (Polynomial.eval z P)‖) := by        have hpos : 0 < ‖Complex.exp (Polynomial.eval z P)‖ := by          simp        have hle :            ‖Complex.exp (Polynomial.eval z P)‖ ≤              1 + ‖Complex.exp (Polynomial.eval z P)‖ := by          linarith [norm_nonneg (Complex.exp (Polynomial.eval z P))]        have hlog_le : Real.log ‖Complex.exp (Polynomial.eval z P)‖            ≤ Real.log (1 + ‖Complex.exp (Polynomial.eval z P)‖) :=          Real.log_le_log hpos hle        have hlog_eq : Real.log ‖Complex.exp (Polynomial.eval z P)‖ = (P.eval z).re := by          simp [Complex.norm_exp]        simpa [hlog_eq] using hlog_le      have hlog_upper :          Real.log (1 + ‖Complex.exp (Polynomial.eval z P)‖) ≤ C * (1 + ‖z‖) ^ ρ :=        hC z      have hmain : c * R ^ (P.natDegree : ℝ) ≤ C * (1 + R) ^ ρ := by        have hz_re' : c * R ^ P.natDegree ≤ (P.eval z).re := by          simpa [c] using hz_re        have hz_re'' : c * R ^ (P.natDegree : ℝ) ≤ (P.eval z).re := by          simpa [Real.rpow_natCast, c] using hz_re'        have : c * R ^ (P.natDegree : ℝ) ≤ Real.log (1 + ‖Complex.exp (Polynomial.eval z P)‖) :=          hz_re''.trans hlog_lower        have : c * R ^ (P.natDegree : ℝ) ≤ C * (1 + ‖z‖) ^ ρ :=          this.trans hlog_upper        simpa [hz_norm] using this      have h1R_le : (1 + R : ℝ) ≤ R * 2 := by linarith      have hpow1 : (1 + R : ℝ) ^ ρ ≤ (R * 2) ^ ρ :=        Real.rpow_le_rpow (by linarith [hR_pos.le]) h1R_le hρ      have hR2 : (R * 2) ^ ρ = R ^ ρ * (2 : ℝ) ^ ρ := by        have hRnonneg : 0 ≤ R := le_of_lt hR_pos        have h2nonneg : 0 ≤ (2 : ℝ) := by norm_num        simpa [mul_assoc] using (Real.mul_rpow hRnonneg h2nonneg (z := ρ))      have hmain' : c * R ^ (P.natDegree : ℝ) ≤ C * (R ^ ρ * (2 : ℝ) ^ ρ) := by        have := le_trans hmain (mul_le_mul_of_nonneg_left hpow1 (le_of_lt hCpos))        simpa [hR2, mul_assoc, mul_left_comm, mul_comm] using this      have hRρ_pos : 0 < R ^ ρ := Real.rpow_pos_of_pos hR_pos _      have hRρ_ne : (R ^ ρ : ℝ) ≠ 0 := ne_of_gt hRρ_pos      have hdiv :          (c * R ^ (P.natDegree : ℝ)) / (R ^ ρ) ≤ C * (2 : ℝ) ^ ρ := by        have h :=            div_le_div_of_nonneg_right hmain' (le_of_lt hRρ_pos)        have hRhs : (C * (R ^ ρ * (2 : ℝ) ^ ρ)) / (R ^ ρ) = C * (2 : ℝ) ^ ρ := by          field_simp [hRρ_ne]        simpa [hRhs, mul_assoc, mul_left_comm, mul_comm] using h      have hRsub : R ^ δ = R ^ (P.natDegree : ℝ) / R ^ ρ := by        simpa [δ] using (Real.rpow_sub hR_pos (P.natDegree : ℝ) ρ)      have hRδ_le : c * (R ^ δ) ≤ C * (2 : ℝ) ^ ρ := by        have hLhs : c * (R ^ δ) = (c * R ^ (P.natDegree : ℝ)) / (R ^ ρ) := by          simp [hRsub, div_eq_mul_inv, mul_left_comm, mul_comm]        simpa [hLhs] using hdiv      have hRδ_le' : R ^ δ ≤ K0 := by        have : R ^ δ ≤ (C * (2 : ℝ) ^ ρ) / c := by          refine (le_div_iff₀ hcpos).2 ?_          simpa [mul_assoc, mul_left_comm, mul_comm] using hRδ_le        simpa [K0] using this      have : K0 + 1 ≤ K0 := le_trans hRδ (le_trans hRδ_le' (le_rfl))      exact (not_lt_of_ge this) (lt_add_of_pos_right _ (by norm_num : (0 : ℝ) < 1))    exact (Nat.le_floor_iff hρ).2 hn_le_real