TileStructure.Forest.forest_operator_g_prelude

lemma forest_operator_g_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 f 2 * eLpNorm (∑ u with u ∈ t, adjointCarlesonSum (t u) g ·) 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    _ = ‖∑ u with u ∈ t, ∫ x, conj (g x) * carlesonSum (t u) f x‖ₑ := by      congr; rw [← integral_finsetSum]; swap      · fun_prop      simp_rw [Finset.mul_sum]    _ = ‖∑ u with u ∈ t, ∫ x, conj (adjointCarlesonSum (t u) g x) * f x‖ₑ := by      congr! 2 with u mu; exact adjointCarlesonSum_adjoint bf bg _    _ = ‖∫ x, f x * ∑ u with u ∈ t, conj (adjointCarlesonSum (t u) g x)‖ₑ := by      congr; rw [← integral_finsetSum]; swap      · intro _ _        fun_prop      simp_rw [Finset.mul_sum, mul_comm (f _)]    _ ≤ ∫⁻ x, ‖f x‖ₑ * ‖∑ u with u ∈ t, conj (adjointCarlesonSum (t u) g x)‖ₑ := by      simp_rw [← enorm_mul]; exact enorm_integral_le_lintegral_enorm _    _ ≤ _ := by      simp_rw [← map_sum, RCLike.enorm_conj]      conv_rhs => rw [← eLpNorm_enorm]; enter [2]; rw [← eLpNorm_enorm]      exact ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance (by fun_prop) (by fun_prop)