Kadiri.abs_log_dyadic_div_two_pi_le

lemma abs_log_dyadic_div_two_pi_le (k : ℕ) :    |Real.log (((2 : ℝ) ^ (k + 1)) / (2 * Real.pi))| ≤      (1 + |Real.log (2 * Real.pi)|) * ((k + 1 : ℕ) : ℝ) := by  have hT_pos : 0 < (2 : ℝ) ^ (k + 1) := pow_pos (by norm_num) _  have hden_pos : 0 < 2 * Real.pi := by positivity  have hTge1 : (1 : ℝ) ≤ (2 : ℝ) ^ (k + 1) :=    one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2)  have hlog_nonneg : 0 ≤ Real.log ((2 : ℝ) ^ (k + 1)) :=    Real.log_nonneg hTge1  have hlog_le : Real.log ((2 : ℝ) ^ (k + 1)) ≤ ((k + 1 : ℕ) : ℝ) :=    log_dyadic_le_nat_succ k  have hk1 : (1 : ℝ) ≤ ((k + 1 : ℕ) : ℝ) := by    exact_mod_cast Nat.succ_pos k  have hL_nonneg : 0 ≤ |Real.log (2 * Real.pi)| := abs_nonneg _  rw [Real.log_div hT_pos.ne' hden_pos.ne']  calc    |Real.log ((2 : ℝ) ^ (k + 1)) - Real.log (2 * Real.pi)|        ≤ |Real.log ((2 : ℝ) ^ (k + 1))| + |Real.log (2 * Real.pi)| :=          abs_sub _ _    _ = Real.log ((2 : ℝ) ^ (k + 1)) + |Real.log (2 * Real.pi)| := by          rw [abs_of_nonneg hlog_nonneg]    _ ≤ ((k + 1 : ℕ) : ℝ) + |Real.log (2 * Real.pi)| := by          exact add_le_add_left hlog_le _    _ ≤ (1 + |Real.log (2 * Real.pi)|) * ((k + 1 : ℕ) : ℝ) := by          nlinarith