lintegral_carlesonSum_𝔓₁_compl_le_sum_aux2

lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_aux2 {N : ℕ} :    ∑ x ≤ N, (((12 + 8 * Z) + (19 + 20 * Z) * x + (7 + 16 * Z) * x ^ 2 + (4 * Z) * x ^ 3) *        (2 : ℝ≥0∞) ^ (-((q - 1) / (8 * ↑a ^ 4) * x : ℝ)))    ≤ (2 : ℝ≥0∞) ^ (28 * a + 20) / (nnq - 1) ^ 4 := by  have : 0 < q - 1 := by linarith [one_lt_q X]  have A : (2 : ℝ≥0∞) = ENNReal.ofReal (2 : ℝ) := by simp  simp_rw [A, ENNReal.ofReal_rpow_of_pos zero_lt_two]  calc  ∑ x ≤ N, (((12 + 8 * ↑Z) + (19 + 20 * ↑Z) * x + (7 + 16 * ↑Z) * x ^ 2 + (4 * ↑Z) * x ^ 3)      * ENNReal.ofReal (2 ^ (-((q - 1) / (8 * ↑a ^ 4) * x : ℝ))))  _ = ∑ x ≤ N, ENNReal.ofReal      (((12 + 8 * Z) + (19 + 20 * Z) * x + (7 + 16 * Z) * x ^ 2 + (4 * Z) * x ^ 3) *        2 ^ (-((q - 1) / (8 * ↑a ^ 4) * x : ℝ))) := by    congr with i    rw [ENNReal.ofReal_mul (by positivity)]    congr    norm_cast  _ = ENNReal.ofReal (∑ x ≤ N,      (((12 + 8 * Z) + (19 + 20 * Z) * x + (7 + 16 * Z) * x ^ 2 + (4 * Z) * x ^ 3) *        2 ^ (-((q - 1) / (8 * ↑a ^ 4) * x : ℝ)))) := by    rw [ENNReal.ofReal_sum_of_nonneg]    intro i hi    positivity  _ ≤ ENNReal.ofReal (2 ^ (28 * a + 20) / (q - 1) ^ 4) := by    apply ENNReal.ofReal_le_ofReal    simpa using lintegral_carlesonSum_𝔓₁_compl_le_sum_aux1 (X := X)  _ = 2 ^ (28 * a + 20) / (ENNReal.ofReal (q - 1)) ^ 4 := by    rw [ENNReal.ofReal_div_of_pos (by positivity)]    congr    · norm_cast    · rw [ENNReal.ofReal_pow]      linarith  _ = (ENNReal.ofReal 2) ^ (28 * a + 20) / (nnq - 1) ^ 4 := by    rw [← A]    rfl