lintegral_carlesonSum_forest'

lemma lintegral_carlesonSum_forest'    {f : X → ℂ} (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :    ∫⁻ x in G \ G', ‖carlesonSum (⋃ u ∈ 𝔘₄ k n j l, 𝔗₂ k n j u) f x‖ₑ ≤    C2_0_4 a q n * 2 ^ (a + 5/2 : ℝ) * (volume G) ^ (1 - q⁻¹) * (volume F) ^ (q⁻¹) := by  apply (lintegral_carlesonSum_forest hf h2f).trans  simp only [mul_assoc]  apply mul_le_mul_right  simp only [div_eq_mul_inv, one_mul, ENNReal.mul_rpow_of_nonneg _ _ (inv_q_sub_half_nonneg X),    ← ENNReal.rpow_natCast, ← ENNReal.rpow_mul]  calc  2 ^ ((2 * a + 5 : ℕ) * (q⁻¹ - 2⁻¹)) * volume F ^ (q⁻¹ - 2⁻¹) * (volume G)⁻¹ ^ (q⁻¹ - 2⁻¹) *    (volume F ^ (2⁻¹ : ℝ) * volume G ^ (2⁻¹ : ℝ))  _ ≤ 2 ^ (a + 5/2 : ℝ) * volume F ^ (q⁻¹ - 2⁻¹) * (volume G)⁻¹ ^ (q⁻¹ - 2⁻¹) *    ((volume F) ^ (2⁻¹ : ℝ) * volume G ^ (2⁻¹ : ℝ)) := by    gcongr    · exact one_le_two    have : 1 ≤ q := (one_lt_q X).le    have : (2 * a + 5 : ℕ) * (q⁻¹ - 2⁻¹) ≤ (2 * a + 5 : ℕ) * (1⁻¹ - 2⁻¹) := by gcongr    apply this.trans_eq    norm_num    simp [add_mul, div_eq_mul_inv]    ring  _ = 2 ^ (a + 5/2 : ℝ) * (volume G ^ (1 - q⁻¹) * volume F ^ q⁻¹) := by    rcases eq_or_ne (volume G) 0 with vG | vG    · have : 0 < 1 - q⁻¹ := by rw [sub_pos, inv_lt_one_iff₀]; exact .inr (one_lt_q X)      rw [vG, ENNReal.zero_rpow_of_pos (by positivity), ENNReal.zero_rpow_of_pos this]      simp only [zero_mul, mul_zero]    · have IF : (volume F) ^ (q⁻¹) = (volume F) ^ ((q ⁻¹ - 2⁻¹) + 2⁻¹) := by congr; abel      have IG : (volume G) ^ (1 - q⁻¹) = (volume G) ^ (2⁻¹ - (q⁻¹ - 2⁻¹)) := by        congr 1        simp only [sub_sub_eq_add_sub, sub_left_inj]        norm_num      rw [IF, IG, ENNReal.rpow_sub _ _ vG volume_G_ne_top,        ENNReal.rpow_add_of_nonneg (x := volume F) _ _ (inv_q_sub_half_nonneg X) (by norm_num),        ENNReal.div_eq_inv_mul, ENNReal.inv_rpow]      ring