feat(MeasureTheory/LpSeminorm): add HasCompactSupport.memLp_of_enorm_bound (#37559)

Add `HasCompactSupport.memLp_of_enorm_bound`: a bounded measurable function with compact support is in L^p. This is the `ENNReal`-valued version of `HasCompactSupport.memLp_of_bound`.

Upstreamed from the [Carleson](https://github.com/fpvandoorn/carleson) project.

Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: pitmonticone

Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean

@@ -69,6 +69,16 @@ theorem _root_.HasCompactSupport.memLp_of_bound {f : X → E} (hf : HasCompactSu
   exact this.mono_exponent_of_measure_support_ne_top
     (fun x ↦ image_eq_zero_of_notMem_tsupport) (hf.measure_lt_top.ne) le_top
 
+/-- A bounded measurable function with compact support is in L^p.
+This is the `ENNReal`-valued version of `HasCompactSupport.memLp_of_bound`. -/
+theorem _root_.HasCompactSupport.memLp_of_enorm_bound {f : X → E} (hf : HasCompactSupport f)
+    (h2f : AEStronglyMeasurable f μ) {C : ℝ≥0∞} (hfC : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ C) (hC : C ≠ ⊤) :
+      MemLp f p μ := by
+  have : MemLp f ∞ μ :=
+    ⟨h2f, eLpNormEssSup_le_of_ae_enorm_bound hfC |>.trans_lt hC.lt_top⟩
+  exact this.mono_exponent_of_measure_support_ne_top
+    (fun x ↦ image_eq_zero_of_notMem_tsupport) hf.measure_ne_top le_top
+
 /-- A continuous function with compact support is in L^p. -/
 theorem _root_.Continuous.memLp_of_hasCompactSupport [OpensMeasurableSpace X]
     {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) : MemLp f p μ := by