lintegral_carlesonSum_𝔓₁_compl_le_sum_aux1

lemma lintegral_carlesonSum_𝔓₁_compl_le_sum_aux1 [ProofData a q K σ₁ σ₂ F G] {N : ℕ} :    ∑ x ≤ N,      (((12 + 8 * Z) * x ^ 0 + (19 + 20 * Z) * x ^ 1 + (7 + 16 * Z) * x ^ 2 + (4 * Z) * x ^ 3) *        (2 : ℝ) ^ (-((q - 1) / (8 * ↑a ^ 4) * x : ℝ))) ≤ 2 ^ (28 * a + 20) / (q - 1) ^ 4 := by  simp only [add_mul _ _ ((2 : ℝ) ^ (_ : ℝ)), Finset.sum_add_distrib]  simp only [mul_assoc, ← Finset.mul_sum]  simp only [← mul_assoc]  have : 0 < q - 1 := by linarith [one_lt_q X]  have : 0 < a := a_pos X  have : q ≤ 2 := q_le_two X  have : (4 : ℝ) ≤ a := mod_cast (four_le_a X)  have P : 0 < (q - 1) / (8 * ↑a ^ 4) := by positivity  have : 0.69 ≤ Real.log 2 := le_trans (by norm_num) Real.log_two_gt_d9.le  have : (1 : ℝ) ≤ Z / 2 ^ 48 := by    rw [one_le_div (by positivity)]    simp only [defaultZ, Nat.cast_pow, Nat.cast_ofNat]    gcongr    · exact one_le_two    · linarith [four_le_a X]  calc  (12 + 8 * ↑Z) * ∑ i ≤ N, ↑i ^ 0 * (2 : ℝ) ^ (-((q - 1) / (8 * a ^ 4) * i)) +      (19 + 20 * ↑Z) * ∑ i ≤ N, ↑i ^ 1 * 2 ^ (-((q - 1) / (8 * a ^ 4) * i)) +      (7 + 16 * ↑Z) * ∑ i ≤ N, ↑i ^ 2 * 2 ^ (-((q - 1) / (8 * a ^ 4) * i)) +      (4 * ↑Z) * ∑ i ≤ N, ↑i ^ 3 * 2 ^ (-((q - 1) / (8 * a ^ 4) * i))  _ ≤ (12 + 8 * ↑Z) * ((2 : ℝ) ^ ((q - 1) / (8 * a ^ 4)) *        0 ! / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ (0 + 1)) +      (19 + 20 * ↑Z) * ((2 : ℝ) ^ ((q - 1) / (8 * a ^ 4)) *        1 ! / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ (1 + 1)) +      (7 + 16 * ↑Z) * ((2 : ℝ) ^ ((q - 1) / (8 * a ^ 4)) *        2 ! / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ (2 + 1)) +      (4 * ↑Z) * ((2 : ℝ) ^ ((q - 1) / (8 * a ^ 4)) *        3 ! / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ (3 + 1)) := by    gcongr <;> apply sum_Iic_pow_mul_two_pow_neg_le P  _ = (2 : ℝ) ^ ((q - 1) / (8 * a ^ 4)) *      ( (12 + 8 * ↑Z) / (Real.log 2 * ((q - 1) / (8 * a ^ 4)))      + (19 + 20 * ↑Z)  / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 2      + (14 + 32 * ↑Z) / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 3      + (24 * ↑Z) /  (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 4) := by    simp only [Nat.cast_ofNat, Nat.factorial, Nat.cast_one, mul_one, zero_add, pow_one,      Nat.succ_eq_add_one, Nat.reduceAdd, Nat.reduceMul]    ring  _ ≤ (2 : ℝ) ^ (1 : ℝ) *      ( (12 + 8 * ↑Z) / (Real.log 2 * ((q - 1) / (8 * a ^ 4)))      + (19 + 20 * ↑Z)  / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 2      + (14 + 32 * ↑Z) / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 3      + (24 * ↑Z) /  (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 4) := by    gcongr    · exact one_le_two    · apply div_le_one_of_le₀ _ (by positivity)      have : 8 * (4 : ℝ) ^ 4 ≤ 8 * a ^ 4 := by gcongr      linarith  _ = (24 + 16 * ↑Z) / (Real.log 2 * ((q - 1) / (8 * a ^ 4)))      + (38 + 40 * ↑Z)  / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 2      + (28 + 64 * ↑Z) / (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 3      + (48 * ↑Z) /  (Real.log 2 * ((q - 1) / (8 * a ^ 4))) ^ 4 := by    simp only [Real.rpow_one]    ring  _ = ((8 * a ^ 4) / (q - 1)) ^ 4 *     (((q - 1) / (8 * a ^ 4)) ^ 3 * (24 * 1 + 16 * ↑Z) / Real.log 2      + ((q - 1) / (8 * a ^ 4)) ^ 2 * (38 * 1 + 40 * ↑Z)  / (Real.log 2) ^ 2      + ((q - 1) / (8 * a ^ 4)) * (28 * 1 + 64 * ↑Z) / (Real.log 2) ^ 3      + (48 * ↑Z) /  (Real.log 2) ^ 4) := by    field_simp  _ ≤ ((8 * a ^ 4) / (q - 1)) ^ 4 *     (((2 - 1) / (8 * 4 ^ 4)) ^ 3 * (24 * (Z / 2 ^ 48) + 16 * ↑Z) / 0.69      + ((2 - 1) / (8 * 4 ^ 4)) ^ 2 * (38 * (Z / 2 ^ 48) + 40 * ↑Z)  / 0.69 ^ 2      + ((2 - 1) / (8 * 4 ^ 4)) * (28 * (Z / 2 ^ 48) + 64 * ↑Z) / 0.69 ^ 3      + (48 * ↑Z) / 0.69 ^ 4) := by gcongr  _ = a ^ 16 / (q - 1) ^ 4 * Z * (8 ^ 4 *      (((2 - 1) / (8 * 4 ^ 4)) ^ 3 * (24 * (1 / 2 ^ 48) + 16) / 0.69      + ((2 - 1) / (8 * 4 ^ 4)) ^ 2 * (38 * (1 / 2 ^ 48) + 40)  / 0.69 ^ 2      + ((2 - 1) / (8 * 4 ^ 4)) * (28 * (1 / 2 ^ 48) + 64) / 0.69 ^ 3      + 48 / 0.69 ^ 4)) := by    rw [div_pow]; ring  _ ≤ a ^ 16 / (q - 1) ^ 4 * Z * 2 ^ 20 := by gcongr; norm_num  _ ≤ (2 ^ a) ^ 16 / (q - 1) ^ 4 * Z * 2 ^ 20 := by    gcongr    exact_mod_cast (Nat.lt_pow_self one_lt_two).le  _ = (2 ^ (16 * a) * 2 ^ (12 * a) * 2 ^ 20) / (q - 1) ^ 4 := by    simp [← pow_mul, mul_comm a]    ring  _ = 2 ^ (28 * a + 20) / (q - 1) ^ 4 := by    simp only [← pow_add]    congr    lia