forest_union_optimized

lemma forest_union_optimized {f : X → ℂ} (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (h'f : Measurable f) :    ∫⁻ x in G \ G', ‖carlesonSum 𝔓₁ f x‖ₑ ≤    C5_1_2_optimized a nnq * (volume G) ^ (1 - q⁻¹) * (volume F) ^ (q⁻¹) := by  apply (forest_union_aux hf h'f).trans  calc  C2_0_4_base a * 2 ^ (a + 5 / 2 : ℝ) * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ *    ∑ n ∈ Finset.Iic (maxℭ X),      ∑ _k ∈ Finset.Iic n, ∑ _j ∈ Finset.Iic (2 * n + 3), ∑ _l ∈ Finset.Iio (4 * n + 12),        2 ^ (-(q - 1) / q * ↑n)  _ ≤ C2_0_4_base a * 2 ^ (a + 5 / 2 : ℝ) * volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹ *      (13009 / (ENNReal.ofReal (q - 1)) ^ 4) := by    gcongr    have A n : (2 : ℝ≥0∞) ^ (-(q - 1) / q * n) = 2 ^ (- ((q - 1) / q * n)) := by      congr; ring    simp_rw [A]    exact forest_union_sum_aux2 (maxℭ X) q (one_lt_q X) (q_le_two X)  _ = C5_1_2_optimized a nnq * (volume G) ^ (1 - q⁻¹) * (volume F) ^ (q⁻¹) := by    have : ENNReal.ofReal (q - 1) = (nnq - 1 : ℝ≥0) := rfl    rw [this]    simp only [ENNReal.div_eq_inv_mul, C5_1_2_optimized, div_eq_inv_mul _ ((nnq - 1) ^ 4),      ENNReal.coe_sub, ENNReal.coe_one, ENNReal.coe_mul, ENNReal.coe_ofNat]    rw [ENNReal.coe_inv, ENNReal.coe_rpow_of_ne_zero two_ne_zero]; swap    · have : 0 < nnq - 1 := tsub_pos_of_lt (one_lt_nnq X)      apply ne_of_gt      positivity    simp only [ENNReal.coe_pow, ENNReal.coe_sub, ENNReal.coe_one, ENNReal.coe_ofNat]    ring