MeasureTheory.BoundedCompactSupport.adjointCarleson

@[fun_prop]theorem BoundedCompactSupport.adjointCarleson (hf : BoundedCompactSupport f) :    BoundedCompactSupport (adjointCarleson p f) where  memLp_top := by    obtain ⟨C, hC⟩ := hf.bddAbove_norm_adjointCarleson p    simp only [mem_upperBounds, mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hC    apply MeasureTheory.memLp_top_of_bound (by fun_prop) C (.of_forall hC)  hasCompactSupport := by    obtain x₀ : X := Classical.choice (by infer_instance)    obtain ⟨r₀, h⟩ := hf.isBoundedSupport.subset_ball x₀    let C : ℝ := (D ^ 𝔰 p / 2) + r₀    apply HasCompactSupport.of_support_subset_closedBall (x := x₀) (r := C)    intro x hx    apply mem_support.mp at hx    have : ∃ y, conj (Ks (𝔰 p) y x) * exp (.I * (Q y y - Q y x)) * f y ≠ 0 := by      by_contra! hc      exact hx <| setIntegral_eq_zero_of_forall_eq_zero fun x _ ↦ hc x    simp only [ne_eq, mul_eq_zero, map_eq_zero, exp_ne_zero, or_false, not_or] at this    obtain ⟨y, hKy, hfy⟩ := this    rw [mem_closedBall]    apply le_trans <| dist_triangle _ y _    unfold C    gcongr    · rw [dist_comm]; exact dist_mem_Icc_of_Ks_ne_zero hKy |>.2    · exact le_of_lt <| h hfy