Kadiri.zetaCountingMainTermDyadicGrowthSource_of_elementary

theorem zetaCountingMainTermDyadicGrowthSource_of_elementary :    zetaCountingMainTermDyadicGrowthSource := by  let B : ℝ := 2 * |(2 * Real.pi)⁻¹|  let L : ℝ := |Real.log (2 * Real.pi)|  refine ⟨B * (1 + L) + B + 1, by positivity, ?_⟩  intro k  let scale : ℝ := ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)  let A : ℝ := ((2 : ℝ) ^ (k + 1)) / (2 * Real.pi)  have hscale_ge_one : (1 : ℝ) ≤ scale := dyadicCountScale_ge_one k  have hpow_nonneg : 0 ≤ (2 : ℝ) ^ k := pow_nonneg (by norm_num) _  have hpow_le_scale : (2 : ℝ) ^ k ≤ scale := by    have hk1 : (1 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by      exact_mod_cast Nat.succ_pos k    nlinarith  have hB_nonneg : 0 ≤ B := by positivity  have hA_abs_eq : |A| = B * (2 : ℝ) ^ k := by    dsimp [A, B]    exact dyadic_div_two_pi_abs_eq k  have hA_abs_le_scale : |A| ≤ B * scale := by    calc      |A| = B * (2 : ℝ) ^ k := hA_abs_eq      _ ≤ B * scale := mul_le_mul_of_nonneg_left hpow_le_scale hB_nonneg  have hlog_abs_le : |Real.log A| ≤ (1 + L) * ((k + 1 : ℕ) : ℝ) := by    dsimp [A, L]    exact abs_log_dyadic_div_two_pi_le k  have hprod_le : |A * Real.log A| ≤ B * (1 + L) * scale := by    rw [abs_mul]    have hmul := mul_le_mul (show |A| ≤ B * (2 : ℝ) ^ k from hA_abs_eq.le)      hlog_abs_le (abs_nonneg _) (mul_nonneg hB_nonneg hpow_nonneg)    calc      |A| * |Real.log A| ≤          (B * (2 : ℝ) ^ k) * ((1 + L) * ((k + 1 : ℕ) : ℝ)) := hmul      _ = B * (1 + L) * scale := by ring  have htri := abs_zetaCountingMainTerm_core_le A  unfold zetaCountingMainTerm  dsimp [A] at htri hA_abs_le_scale hprod_le  calc    |(2 ^ (k + 1)) / (2 * Real.pi) *          Real.log ((2 ^ (k + 1)) / (2 * Real.pi)) -        (2 ^ (k + 1)) / (2 * Real.pi) + 7 / 8|        ≤ |(2 ^ (k + 1)) / (2 * Real.pi) *            Real.log ((2 ^ (k + 1)) / (2 * Real.pi))| +          |(2 ^ (k + 1)) / (2 * Real.pi)| + 1 := htri    _ ≤ B * (1 + L) * scale + B * scale + 1 := by          exact add_le_add (add_le_add hprod_le hA_abs_le_scale) le_rfl    _ ≤ B * (1 + L) * scale + B * scale + scale := by          exact add_le_add_right hscale_ge_one _    _ = (B * (1 + L) + B + 1) * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := by          dsimp [scale]          ring