forest_union_sum_aux2

lemma forest_union_sum_aux2 (M : ℕ) (q : ℝ) (hq : 1 < q) (h'q : q ≤ 2) :    (∑ n ≤ M, ∑ _k ≤ n, ∑ _j ≤ 2 * n + 3, ∑ _l < 4 * n + 12,      (2 : ℝ≥0∞) ^ (- ((q - 1) / q * n))) ≤ 13009 / (ENNReal.ofReal (q - 1)) ^ 4 := by  have : (2 : ℝ≥0∞) = ENNReal.ofReal (2 : ℝ) := by simp  simp_rw [this, ENNReal.ofReal_rpow_of_pos zero_lt_two]  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, ge_iff_le]  calc  ∑ x ∈ Finset.Iic M, (↑x + 1) * ((2 * ↑x + 3 + 1) * ((4 * ↑x + 12)      * ENNReal.ofReal (2 ^ (-((q - 1) / q * ↑x)))))  _ = ∑ x ∈ Finset.Iic M, ENNReal.ofReal      ((↑x + 1) * ((2 * ↑x + 3 + 1) * ((4 * ↑x + 12) * 2 ^ (-((q - 1) / q * ↑x))))) := by    congr with i    rw [ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_mul (by positivity),      ENNReal.ofReal_mul (by positivity)]    congr <;> norm_cast  _ = ENNReal.ofReal (∑ x ∈ Finset.Iic M,      (↑x + 1) * ((2 * ↑x + 3 + 1) * ((4 * ↑x + 12) * 2 ^ (-((q - 1) / q * ↑x))))) := by    rw [ENNReal.ofReal_sum_of_nonneg]    intro i hi    positivity  _ = ENNReal.ofReal (∑ n ≤ M, ∑ _k ≤ n, ∑ _j ≤ 2 * n + 3, ∑ _l < 4 * n + 12,      (2 : ℝ) ^ (- ((q - 1) / q * n))) := by simp  _ ≤ ENNReal.ofReal (13009 / (q - 1) ^ 4) := by    apply ENNReal.ofReal_le_ofReal    exact forest_union_sum_aux1 M q hq h'q  _ = 13009 / (ENNReal.ofReal (q - 1)) ^ 4 := by    rw [ENNReal.ofReal_div_of_pos]; swap    · have : 0 < q - 1 := by linarith      positivity    congr    · norm_cast    · rw [ENNReal.ofReal_pow]      linarith