calculation_150

lemma calculation_150 [PseudoMetricSpace X] [ProofData a q K σ₁ σ₂ F G] :    𝕔 * (3/2) * a ^ 2 * κ ≤ 1 := by  rw [defaultκ, neg_mul, Real.rpow_neg zero_le_two]  refine mul_inv_le_one_of_le₀ ?_ (by positivity); norm_cast  rw [show 2 ^ (10 * a) = 2 ^ (8 * a) * (2 ^ a) ^ 2 by ring]  simp only [Nat.cast_pow, Nat.cast_mul, Nat.cast_ofNat]  gcongr  · calc      _ ≤ (2 : ℝ) ^ (8 * 4) := by        have : (𝕔 : ℝ) * (3/2) ≤ 100 * (3/2) := by gcongr; exact_mod_cast c_le_100        linarith      _ ≤ _ := by gcongr; exacts [one_le_two, four_le_a X]  · norm_cast    exact Nat.lt_two_pow_self.le