Tile.bound_6_2_26

lemma bound_6_2_26 {p p' : 𝔓 X} {g : X → ℂ}    (hg : Measurable g) (hg1 : ∀ x, ‖g x‖ ≤ G.indicator 1 x) :    ‖∫ y, adjointCarleson p' g y * conj (adjointCarleson p g y)‖ₑ ≤    ∫⁻ z in E p' ×ˢ E p, I12 p p' g z.1 z.2 := by  have haux : ∀ y,      conj (∫ y1 in E p, conj (Ks (𝔰 p) y1 y) * exp (I * (Q y1 y1 - Q y1 y)) * g y1) =      ∫ y1 in E p, Ks (𝔰 p) y1 y * exp (I * (-Q y1 y1 + Q y1 y)) * conj (g y1) :=    complex_exp_lintegral  simp_rw [adjointCarleson, haux, ← setIntegral_prod_mul]  rw [← setIntegral_univ]  let f := fun (x, z1, z2) ↦    conj (Ks (𝔰 p') z1 x) * exp (I * (Q z1 z1 - Q z1 x)) * g z1 *    (Ks (𝔰 p) z2 x * exp (I * (-Q z2 z2 + Q z2 x)) * conj (g z2))  have hf : IntegrableOn f (univ ×ˢ E p' ×ˢ E p) (volume.prod (volume.prod volume)) :=    (boundedCompactSupport_aux_6_2_26 hg hg1).integrable.integrableOn  erw [← setIntegral_prod _ hf, ← setIntegral_prod_swap, setIntegral_prod _ (hf.swap), restrict_univ]  simp_rw [← bound_6_2_26_aux]  exact enorm_integral_le_lintegral_enorm _