kappa_le_log2D_inv_mul_K_inv

lemma kappa_le_log2D_inv_mul_K_inv : κ ≤ (Real.logb 2 D * K')⁻¹ := by  have : 2 ≤ a := by linarith [four_le_a X]  have 𝕔_pos : 0 < 𝕔 := by linarith [seven_le_c]  rw [defaultD]  simp only [Nat.cast_pow, Nat.cast_ofNat, mul_inv_rev]  rw [← Real.rpow_natCast,Real.logb_rpow (by norm_num) (by norm_num)]  rw [defaultκ, const_K, neg_mul, Real.rpow_neg (by positivity),    ← mul_inv, inv_le_inv₀ (by positivity) (by positivity)]  simp only [Nat.cast_pow, Nat.cast_ofNat, Nat.cast_mul]  rw [mul_comm, pow_add, pow_one, ← mul_assoc, mul_comm _ 2, ← mul_assoc, ← mul_assoc,    ← Real.rpow_natCast 2]  norm_num  calc    (2 : ℝ) * 𝕔 * a ^ 2 * 2 ^ (4 * a : ℝ)      ≤ 2 ^ 8 * (2 ^ (a : ℝ)) ^ 2 * 2 ^ (4 * a : ℝ) := by      gcongr      · norm_cast        linarith [c_le_100]      · exact (Real.self_lt_two_rpow (a : ℝ)).le    _ ≤ 2 ^ (4 * a : ℝ) * 2 ^ (2 * a : ℝ) * 2 ^ (4 * a : ℝ) := by      gcongr      · rw [← Real.rpow_natCast, Real.rpow_le_rpow_left_iff (by norm_num)]        norm_num        trans 4 * 2        · norm_num        rw [mul_le_mul_iff_right₀ (by norm_num)]        exact Nat.ofNat_le_cast.mpr this      · rw [← Real.rpow_natCast, ← Real.rpow_mul (by norm_num), mul_comm]        simp only [Nat.cast_ofNat, le_refl]    _ ≤ 2 ^ (10 * a : ℝ) := by      simp_rw [← Real.rpow_add (by norm_num : 0 < (2 : ℝ)), ← right_distrib]      norm_num