TileStructure.Forest.integrable_adjointCarleson_interior

lemma integrable_adjointCarleson_interior (hf : BoundedCompactSupport f) :    Integrable (fun y ↦ exp (.I * 𝒬 u x) * (conj (Ks (𝔰 p) y x) * exp (.I * (Q y y - Q y x)) * f y))      (volume.restrict (E p)) := by  have h2f := hf.memLp_top.ae_norm_le  set B := eLpNorm f ∞ volume |>.toReal  refine Integrable.const_mul ?_ _; simp_rw [mul_rotate]  refine Integrable.bdd_mul (c := B) ?_ ?_ ?_  · have bep : IsBounded (E p) := by      rw [isBounded_iff_subset_ball (𝔠 p)]; use 4 * D ^ 𝔰 p      exact E_subset_𝓘.trans Grid_subset_ball    obtain ⟨C, nnC, hC⟩ := IsBounded.exists_bound_of_norm_Ks bep (𝔰 p)    apply Measure.integrableOn_of_bounded (M := C) volume_E_lt_top.ne ?_ ?_    · exact continuous_conj.comp_aestronglyMeasurable        (measurable_Ks.comp measurable_prodMk_right).aestronglyMeasurable    · simp only [RCLike.norm_conj]      exact ae_restrict_of_forall_mem measurableSet_E fun y my ↦ hC y x my  · refine (AEMeasurable.const_mul ?_ I).cexp.mul      hf.restrict.aestronglyMeasurable.aemeasurable |>.aestronglyMeasurable    refine (measurable_ofReal.comp ?_).sub (measurable_ofReal.comp ?_) |>.aemeasurable    · have pair : Measurable fun y : X ↦ (y, y) := by fun_prop      exact measurable_Q₂.comp pair    · exact measurable_Q₂.comp measurable_prodMk_right  · filter_upwards [ae_restrict_of_ae h2f] with x hB    rw [norm_mul, ← one_mul B]    refine mul_le_mul ?_ hB (norm_nonneg _) zero_le_one    rw_mod_cast [mul_comm, norm_exp_ofReal_mul_I]