MeasureTheory.BoundedCompactSupport.bddAbove_norm_adjointCarleson

theorem BoundedCompactSupport.bddAbove_norm_adjointCarleson (hf : BoundedCompactSupport f) :    BddAbove (range (‖adjointCarleson p f ·‖)) := by  obtain ⟨CKf, hCKf, hCKf⟩ := hf.hasCompactSupport.isBounded.exists_bound_of_norm_Ks (𝔰 p)  let C : ℝ := CKf * (eLpNorm f ⊤).toReal * volume.real (E p)  use C  simp only [mem_upperBounds, mem_range, forall_exists_index, forall_apply_eq_imp_iff]  intro x  apply norm_setIntegral_le_of_norm_le_const_ae volume_E_lt_top <| ae_restrict_of_ae _  filter_upwards [hf.memLp_top.ae_norm_le] with y hy  suffices ‖Ks (𝔰 p) y x‖ * ‖f y‖ ≤ ?C by    simp_rw [norm_mul, ← ofReal_sub, norm_exp_I_mul_ofReal, mul_one, RCLike.norm_conj]    exact this  by_cases hy : y ∈ tsupport f  · specialize hCKf y x hy; gcongr  · simp_rw [image_eq_zero_of_notMem_tsupport hy, norm_zero, mul_zero]    positivity