forest_union_sum_aux1

lemma forest_union_sum_aux1 (M : ℕ) (q : ℝ) (hq : 1 < q) (h'q : q ≤ 2) :    ∑ n ≤ M, ∑ _k ≤ n, ∑ _j ≤ 2 * n + 3, ∑ _l < 4 * n + 12,      (2 : ℝ) ^ (- ((q - 1) / q * n)) ≤ 13009 / (q - 1) ^ 4 := by  have A (x : ℝ) : (x + 1) * (2 * x + 3 + 1) * (4 * x + 12)      = 8 * x ^ 3 + 48 * x ^ 2 + 88 * x + 48:= by ring  simp only [Finset.sum_const, Nat.card_Iio, nsmul_eq_mul, Nat.cast_add, Nat.cast_mul,    Nat.cast_ofNat, Nat.card_Iic, Nat.cast_one, ← mul_assoc, A, ge_iff_le]  simp only [add_mul, Finset.sum_add_distrib, mul_assoc, ← Finset.mul_sum]  have : 0 ≤ q - 1 := by linarith  have : q - 1 ≤ 1 := by linarith  have : 0.6931471803 ≤ Real.log 2 := Real.log_two_gt_d9.le  let c := (q - 1) / q  have hc : 0 < c := div_pos (by linarith) (by linarith)  calc  8 * ∑ i ∈ Finset.Iic M, i ^ 3 * (2 : ℝ) ^ (-(c * i))    + 48 * ∑ i ∈ Finset.Iic M, i ^ 2 * (2 : ℝ) ^ (-(c * i))    + 88 * ∑ i ∈ Finset.Iic M, i * (2 : ℝ) ^ (-(c * i))    + 48 * ∑ i ∈ Finset.Iic M, (2 : ℝ) ^ (-(c * i))  _ = 8 * ∑ i ∈ Finset.Iic M, i ^ 3 * (2 : ℝ) ^ (-(c * i))      + 48 * ∑ i ∈ Finset.Iic M, i ^ 2 * (2 : ℝ) ^ (-(c * i))      + 88 * ∑ i ∈ Finset.Iic M, i ^ 1  * (2 : ℝ) ^ (-(c * i))      + 48 * ∑ i ∈ Finset.Iic M, i ^ 0 * (2 : ℝ) ^ (-(c * i)) := by simp  _ ≤ 8 * (2 ^ c * 3 ! / (Real.log 2 * c) ^ (3 + 1))      + 48 * (2 ^ c * 2 ! / (Real.log 2 * c) ^ (2 + 1))      + 88 * (2 ^ c * 1 ! / (Real.log 2 * c) ^ (1 + 1))      + 48 * (2 ^ c * 0! / (Real.log 2 * c) ^ (0 + 1)) := by    gcongr <;> exact sum_Iic_pow_mul_two_pow_neg_le hc  _ = (2 ^ c * (48 * q ^ 4 / (Real.log 2) ^ 4 + 96 * q^3 * (q - 1) / (Real.log 2) ^ 3      + 88 * q ^ 2 * (q - 1) ^ 2 / (Real.log 2) ^ 2      + 48 * q * (q - 1) ^ 3/ (Real.log 2))) / (q - 1) ^ 4 := by    simp only [Nat.factorial, Nat.succ_eq_add_one, Nat.reduceAdd, zero_add, mul_one, Nat.reduceMul,      Nat.cast_ofNat, mul_pow, div_pow, Nat.cast_one, pow_one, c]    have : q - 1 ≠ 0 := by linarith    field_simp    ring  _ ≤ (2 ^ (1 : ℝ) * (48 * 2 ^ 4 / (Real.log 2) ^ 4 + 96 * 2 ^ 3 * 1 / (Real.log 2) ^ 3      + 88 * 2 ^ 2 * 1 ^ 2 / (Real.log 2) ^ 2 + 48 * 2 * 1 ^ 3 / (Real.log 2))) / (q - 1) ^ 4 := by    gcongr    · exact one_le_two    · rw [div_le_one (by linarith)]      linarith  _ ≤ (2 ^ (1 : ℝ) * (48 * 2 ^ 4 / 0.6931471803 ^ 4 + 96 * 2 ^ 3 * 1 / 0.6931471803 ^ 3      + 88 * 2 ^ 2 * 1 ^ 2 / 0.6931471803 ^ 2 + 48 * 2 * 1 ^ 3 / 0.6931471803)) / (q - 1) ^ 4 := by    gcongr  _ ≤ 13009 / (q - 1) ^ 4 := by    gcongr    norm_num