TileStructure.Forest.forest_operator_f_inner

lemma forest_operator_f_inner (hf : Measurable f) (h2f : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :    eLpNorm (G.indicator (carlesonRowSum t j f)) 2 ≤    C7_7_2_2 a n * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 := by  have bf := bcs_of_measurable_of_le_indicator_f hf h2f  set IGTf := G.indicator (carlesonRowSum t j f)  have bIGTf : BoundedCompactSupport IGTf :=    (BoundedCompactSupport.finset_sum fun _ _ ↦ bf.carlesonSum).indicator measurableSet_G  suffices eLpNorm IGTf 2 ^ 2 ≤      C7_7_2_2 a n * dens₂ (⋃ u ∈ t, t u) ^ (2 : ℝ)⁻¹ * eLpNorm IGTf 2 * eLpNorm f 2 by    rcases eq_or_ne (eLpNorm IGTf 2) 0 with he | he    · simp [he]    · have nt : eLpNorm IGTf 2 ≠ ⊤ := (bIGTf.memLp _).eLpNorm_ne_top      rwa [mul_assoc _ (eLpNorm IGTf 2 volume), mul_comm (eLpNorm IGTf 2 volume), ← mul_assoc, sq,        ENNReal.mul_le_mul_iff_left he nt] at this  calc    _ = ‖∫ x, conj (IGTf x) * carlesonRowSum t j f x‖ₑ := by      rw [eLpNorm_two_eq_enorm_integral_mul_conj (bIGTf.memLp _)]; congr! 3 with x      unfold IGTf      rw [indicator_eq_indicator_one_mul, map_mul, conj_indicator, map_one, mul_mul_mul_comm,        ← inter_indicator_mul, inter_self, mul_comm (carlesonRowSum ..), ← mul_assoc]      simp_rw [Pi.one_apply, mul_one]; rfl    _ = ‖∫ x, conj (F.indicator (adjointCarlesonRowSum t j IGTf) x) * f x‖ₑ := by      rw [adjointCarlesonRowSum_adjoint bf bIGTf]; congr! 3 with x      rw [indicator_eq_indicator_one_mul, map_mul, conj_indicator, map_one, mul_rotate, mul_assoc]      congr 1      by_cases hx : x ∈ F      · simp [indicator_of_mem hx]      · specialize h2f x        rw [indicator_of_notMem hx, norm_le_zero_iff] at h2f        rw [h2f, zero_mul]    _ ≤ ∫⁻ x, ‖F.indicator (adjointCarlesonRowSum t j IGTf) x‖ₑ * ‖f x‖ₑ := by      conv_rhs => enter [2, x]; rw [← RCLike.enorm_conj, ← enorm_mul]      exact enorm_integral_le_lintegral_enorm _    _ ≤ eLpNorm (F.indicator (adjointCarlesonRowSum t j IGTf)) 2 * eLpNorm f 2 := by      apply ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm inferInstance      · exact ((BoundedCompactSupport.finset_sum fun _ _ ↦ bIGTf.adjointCarlesonSum).indicator          measurableSet_F).enorm.aestronglyMeasurable.aemeasurable      · fun_prop    _ ≤ _ := by gcongr; exact indicator_row_bound bIGTf support_indicator_subset