MeasureTheory.BoundedCompactSupport.bddAbove_norm_carlesonOn

theorem BoundedCompactSupport.bddAbove_norm_carlesonOn    {f : X → ℂ} (hf : BoundedCompactSupport f) : BddAbove (range (‖carlesonOn p f ·‖)) := by  let x₀ : X := Classical.choice inferInstance  obtain ⟨r₀, hr₀, hfr₀⟩ := hf.hasCompactSupport.isBounded.subset_closedBall_lt 0 x₀  let r₁ := (↑D ^ 𝔰 p / 2) + r₀  have hcf : support (_root_.carlesonOn p f) ⊆ closedBall x₀ r₁ := by    simp_rw [carlesonOn_def']    intro x hx    simp only [mem_support] at hx    apply indicator_apply_ne_zero.mp at hx    replace hx := hx.2    simp only [mem_support] at hx    have : ∃ y, Ks (𝔰 p) x y * f y * cexp (I * (Q x y - Q x x)) ≠ 0 := by      by_contra! hc      apply hx      simp_rw [hc, integral_zero]    obtain ⟨y, hy⟩ := this    simp only [ne_eq, mul_eq_zero, exp_ne_zero, or_false, not_or] at hy    apply le_trans <| dist_triangle _ y _    unfold r₁    gcongr    exacts [(dist_mem_Icc_of_Ks_ne_zero hy.1).2, hfr₀ (subset_tsupport _ hy.2)]  obtain ⟨CK, nnCK, hCK⟩ :=    Metric.isBounded_closedBall (x := x₀) (r := r₁) |>.exists_bound_of_norm_Ks (𝔰 p)  let C := volume.real (closedBall x₀ r₀) * (CK * (eLpNorm f ⊤).toReal)  rw [bddAbove_def]  use C; simp_rw [mem_range, forall_exists_index, forall_apply_eq_imp_iff]; intro x  by_cases hx : x ∈ support (_root_.carlesonOn p f); swap  · simp only [mem_support, ne_eq, not_not] at hx    rw [hx, norm_zero]    positivity  · simp_rw [carlesonOn_def']    apply le_trans <| norm_indicator_le_norm_self ..    let g := (closedBall x₀ r₀).indicator (fun _ ↦ CK * (eLpNorm f ⊤).toReal)    have hK : ∀ᵐ y, ‖Ks (𝔰 p) x y * f y * cexp (I * (Q x y - Q x x))‖ ≤ g y := by      filter_upwards [hf.memLp_top.ae_norm_le] with y hy      by_cases hy' : y ∈ support f      · simp_rw [norm_mul, ← ofReal_sub, norm_exp_I_mul_ofReal, mul_one, g,          indicator_of_mem (hfr₀ <|subset_tsupport _ hy' ) _]        gcongr        exact hCK x y (hcf hx)      · simp_rw [notMem_support.mp hy', mul_zero, zero_mul, norm_zero, g]        unfold indicator        split_ifs <;> positivity    calc      _ ≤ ∫ y, g y := by        refine norm_integral_le_of_norm_le ?_ hK        exact Integrable.indicator_const measurableSet_closedBall measure_closedBall_lt_top      _ = volume.real (closedBall x₀ r₀) * (CK * (eLpNorm f ⊤ volume).toReal) :=        integral_indicator_const _ measurableSet_closedBall