Forest operator

theorem forest_operator' {n : ℕ} (𝔉 : Forest X n) {f : X → ℂ} {A : Set X}    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) (hA : MeasurableSet A) (sA : A ⊆ G) :    ∫⁻ x in A, ‖∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f x‖ₑ ≤    C2_0_4 a q n * (dens₂ (⋃ u ∈ 𝔉, 𝔉 u)) ^ (q⁻¹ - 2⁻¹) *    eLpNorm f 2 volume * (volume A) ^ (1/2 : ℝ) := by  /- This follows from the other version by taking for the test function `g` the argument of  the sum to be controlled. -/  have bf := bcs_of_measurable_of_le_indicator_f hf h2f  rw [← enorm_integral_starRingEnd_mul_eq_lintegral_enorm]; swap  · exact (BoundedCompactSupport.finset_sum (fun i hi ↦ by fun_prop)).integrable  rw [← integral_indicator hA]  simp_rw [indicator_mul_left, ← comp_def,    Set.indicator_comp_of_zero (g := starRingEnd ℂ) (by simp)]  have bAi (x : X) : ‖A.indicator (fun y ↦ (∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f y) /      ‖∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f y‖) x‖ ≤ A.indicator 1 x := by    rw [norm_indicator_eq_indicator_norm]; apply indicator_le_indicator    rw [Complex.norm_div, norm_real, norm_norm, Pi.one_apply]    rcases eq_or_ne ‖∑ u with u ∈ 𝔉, carlesonSum (𝔉 u) f x‖ 0 with hnorm | hnorm    · rw [hnorm]; norm_num    · rw [div_self hnorm]  apply (forest_operator 𝔉 hf h2f ?_ fun x ↦ ?_).trans; rotate_left  · exact Measurable.indicator (by fun_prop) hA  · exact (bAi _).trans (indicator_le_indicator_apply_of_subset sA (by simp))  gcongr  · simp only [sub_nonneg, inv_le_inv₀ zero_lt_two (q_pos X)]    exact (q_mem_Ioc (X := X)).2  · exact le_rfl  calc  _ ≤ eLpNorm (A.indicator (fun x ↦ 1) : X → ℝ) 2 volume := by    apply eLpNorm_mono (fun x ↦ ?_)    simp only [indicator, coe_algebraMap, Real.norm_eq_abs]    split_ifs    · simpa using div_self_le_one _    · simp  _ ≤ _ := by    rw [eLpNorm_indicator_const hA (by norm_num) (by norm_num)]    simp