TileStructure.Forest.forest_operator_f_prelude

lemma forest_operator_f_prelude    (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x)    (hg : Measurable g) (h2g : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    ‖∫ x, conj (g x) * ∑ u with u ∈ t, carlesonSum (t u) f x‖ₑ ≤    eLpNorm g 2 * eLpNorm (fun x ↦ G.indicator (∑ u with u ∈ t, carlesonSum (t u) f ·) x) 2 := by  have bf := bcs_of_measurable_of_le_indicator_f hf h2f  have bg := bcs_of_measurable_of_le_indicator_g hg h2g  calc    _ ≤ ∫⁻ x, ‖g x‖ₑ * ‖∑ u with u ∈ t, carlesonSum (t u) f x‖ₑ := by      conv_rhs => enter [2, x]; rw [← RCLike.enorm_conj, ← enorm_mul]      exact enorm_integral_le_lintegral_enorm _    _ = ∫⁻ x, ‖g x‖ₑ * ‖G.indicator (∑ u with u ∈ t, carlesonSum (t u) f ·) x‖ₑ := by      congr! 2 with x; rw [indicator_eq_indicator_one_mul, enorm_mul, ← mul_assoc]      nth_rw 2 [← enorm_mul]; congr 2      by_cases hx : x ∈ G      · simp [indicator_of_mem hx]      · specialize h2g x        rw [indicator_of_notMem hx, norm_le_zero_iff] at h2g        rw [h2g, zero_mul]    _ ≤ _ :=      ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance (by fun_prop)        ((BoundedCompactSupport.finset_sum fun _ _ ↦          bf.carlesonSum).indicator measurableSet_G).enorm.aestronglyMeasurable.aemeasurable