Complex.Hadamard.max_one_norm_div_pow_le_one_add_rpow

lemma max_one_norm_div_pow_le_one_add_rpow    {m : ℕ} {τ r : ℝ} {u a : ℂ}    (hur : ‖u‖ = r)    (hmτ : (m : ℝ) ≤ τ) :    max 1 (‖u / a‖ ^ m) ≤ 1 + (r / ‖a‖) ^ τ := by  by_cases hx : ‖u / a‖ ≤ 1  · have hpowm_le1 : ‖u / a‖ ^ m ≤ 1 := pow_le_one₀ (norm_nonneg (u / a)) hx    have hr0 : 0 ≤ r := by simpa [hur] using (norm_nonneg u)    have hbase : 0 ≤ r / ‖a‖ := div_nonneg hr0 (norm_nonneg a)    have hnonneg : 0 ≤ (r / ‖a‖) ^ τ := Real.rpow_nonneg hbase τ    have hle1 : (1 : ℝ) ≤ 1 + (r / ‖a‖) ^ τ := le_add_of_nonneg_right hnonneg    have hle2 : ‖u / a‖ ^ m ≤ 1 + (r / ‖a‖) ^ τ := hpowm_le1.trans hle1    exact (max_le_iff).2 ⟨hle1, hle2⟩  · have hx1 : 1 < ‖u / a‖ := lt_of_not_ge hx    have hpow :        (‖u / a‖ : ℝ) ^ (m : ℝ) ≤ (‖u / a‖ : ℝ) ^ τ :=      Real.rpow_le_rpow_of_exponent_le (le_of_lt hx1) hmτ    have hpow' : ‖u / a‖ ^ m ≤ (‖u / a‖ : ℝ) ^ τ := by      simpa [Real.rpow_natCast] using hpow    have hmax_add : max 1 (‖u / a‖ ^ m) ≤ 1 + ‖u / a‖ ^ m := by      refine max_le (le_add_of_nonneg_right (by positivity)) (le_add_of_nonneg_left (by positivity))    have : max 1 (‖u / a‖ ^ m) ≤ 1 + (‖u / a‖ : ℝ) ^ τ :=      hmax_add.trans (by nlinarith [hpow'])    simpa [norm_div, hur] using this