BKLNW.sum_gt.aux

lemma sum_gt.aux (k : ℕ) (a b : ℝ) (hk : 3 < k := by decide) (hb1 : 0 ≤ b - 1 := by norm_num only)    (ha : a ^ k ≤ 1024 := by norm_num only) (hb : b ^ (3 * k) ≤ 2 ^ (k - 3) := by norm_num only) :    a * (b - 1) ≤ summand k 9 := by  have ha_bound : a ≤ 2 ^ (10 / k : ℝ) := calc    a ≤ (1024 : ℝ) ^ (1 / k : ℝ) := by      contrapose! ha      calc        _ ≤ ((1024 : ℝ) ^ (1 / k : ℝ)) ^ k := by          rw [← rpow_mul_natCast (by positivity), one_div_mul_cancel (by positivity), rpow_one]        _ < _ := pow_lt_pow_left₀ ha (by positivity) (by positivity)    _ = _ := by norm_num [div_eq_mul_inv, rpow_mul]  have hb_bound : b - 1 ≤ 2 ^ (1 / 3 - 1 / k : ℝ) - 1 := calc    _ ≤ ((2 : ℝ) ^ (k - 3 : ℝ)) ^ (1 / (3 * k : ℝ)) - 1 := by      gcongr      contrapose! hb      calc        _ ≤ (((2 : ℝ) ^ (k - 3 : ℝ)) ^ (1 / (3 * k : ℝ))) ^ (3 * k) := by          rw [← rpow_mul_natCast (by positivity), ← Real.rpow_natCast, Nat.cast_sub hk.le]          simp          field_simp          simp        _ < _ := pow_lt_pow_left₀ hb (by positivity) (by positivity)    _ = _ := by rw [← Real.rpow_mul (by positivity), mul_one_div]; field_simp  grw [ha_bound, hb_bound]  norm_num [summand]