Kadiri.zetaCountingDyadic_abs_N_le_geometric

lemma zetaCountingDyadic_abs_N_le_geometric :    ∃ E : ℝ, 0 < E ∧ ∀ k : ℕ,      |riemannZeta.N ((2 : ℝ) ^ (k + 1))| ≤ E * 3 ^ k := by  obtain ⟨A, hA0, hA⟩ := Backlund.zetaCounting_crude_majorant  refine ⟨3 * A, by linarith, fun k => ?_⟩  have hT2 : (2 : ℝ) ≤ (2 : ℝ) ^ (k + 1) := by    calc (2 : ℝ) = 2 ^ 1 := (pow_one 2).symm    _ ≤ 2 ^ (k + 1) := pow_le_pow_right₀ one_le_two (by omega)  have hpow32 : ((2 : ℝ) ^ (k + 1)) ^ (3 / 2 : ℝ) =      ((2 : ℝ) ^ (3 / 2 : ℝ)) ^ (k + 1) := by    rw [← Real.rpow_natCast (2 : ℝ) (k + 1),      ← Real.rpow_mul (by norm_num : (0 : ℝ) ≤ 2), mul_comm,      Real.rpow_mul (by norm_num : (0 : ℝ) ≤ 2), Real.rpow_natCast]  have hbase : (2 : ℝ) ^ (3 / 2 : ℝ) ≤ 3 := by    rw [show (3 / 2 : ℝ) = 1 + 1 / 2 by norm_num,      Real.rpow_add (by norm_num : (0 : ℝ) < 2), Real.rpow_one,      ← Real.sqrt_eq_rpow]    nlinarith [Real.sq_sqrt (show (0 : ℝ) ≤ 2 by norm_num), Real.sqrt_nonneg 2]  have hbase0 : (0 : ℝ) ≤ (2 : ℝ) ^ (3 / 2 : ℝ) :=    Real.rpow_nonneg (by norm_num) _  calc |riemannZeta.N ((2 : ℝ) ^ (k + 1))|      ≤ A * ((2 : ℝ) ^ (k + 1)) ^ (3 / 2 : ℝ) := hA ((2 : ℝ) ^ (k + 1)) hT2    _ = A * ((2 : ℝ) ^ (3 / 2 : ℝ)) ^ (k + 1) := by rw [hpow32]    _ ≤ A * 3 ^ (k + 1) :=        mul_le_mul_of_nonneg_left (pow_le_pow_left₀ hbase0 hbase (k + 1)) hA0.le    _ = 3 * A * 3 ^ k := by ring