From 9cd36cd774da04cb6959068cc5b2b19626d0fffd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 15 Nov 2024 16:15:25 +0000
Subject: [PATCH] Fill in API sorries for `eLpNorm`

---
 .../Function/LpSeminorm/Basic.lean              | 17 ++++++++---------
 LeanAPAP/Mathlib/Order/LiminfLimsup.lean        | 14 ++++++++++++++
 2 files changed, 22 insertions(+), 9 deletions(-)
 create mode 100644 LeanAPAP/Mathlib/Order/LiminfLimsup.lean

diff --git a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
index 44f27cc0b2..d9b45fca64 100644
--- a/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
+++ b/LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@@ -1,4 +1,6 @@
+import Mathlib.Data.Fintype.Order
 import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import LeanAPAP.Mathlib.Order.LiminfLimsup
 
 noncomputable section
 
@@ -21,19 +23,16 @@ lemma eLpNorm_lt_top_of_finite [Finite α] [IsFiniteMeasure μ] : eLpNorm f p μ
   · simp
   obtain rfl | hp := eq_or_ne p ∞
   · simp only [eLpNorm_exponent_top, eLpNormEssSup_lt_top_iff_isBoundedUnder]
-    sorry
+    exact .le_of_finite
   rw [eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top hp₀ hp]
   refine IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal μ ?_
-  sorry
+  simp_rw [← ENNReal.coe_rpow_of_nonneg _ ENNReal.toReal_nonneg]
+  norm_cast
+  exact Finite.exists_le _
 
 @[simp] lemma Memℒp.of_discrete [DiscreteMeasurableSpace α] [Finite α] [IsFiniteMeasure μ] :
-    Memℒp f p μ := by
-  refine ⟨.of_finite, ?_⟩
-  rw [eLpNorm_lt_top_iff_lintegral_rpow_nnnorm_lt_top]
-  refine IsFiniteMeasure.lintegral_lt_top_of_bounded_to_ennreal μ ?f_bdd
-  sorry
-  sorry
-  sorry
+    Memℒp f p μ :=
+  let ⟨C, hC⟩ := Finite.exists_le (‖f ·‖₊); .of_bound .of_finite C <| .of_forall hC
 
 @[simp] lemma eLpNorm_of_isEmpty [IsEmpty α] (f : α → E) (p : ℝ≥0∞) : eLpNorm f p μ = 0 := by
   simp [Subsingleton.elim f 0]
diff --git a/LeanAPAP/Mathlib/Order/LiminfLimsup.lean b/LeanAPAP/Mathlib/Order/LiminfLimsup.lean
new file mode 100644
index 0000000000..ea5f83d383
--- /dev/null
+++ b/LeanAPAP/Mathlib/Order/LiminfLimsup.lean
@@ -0,0 +1,14 @@
+import Mathlib.Order.LiminfLimsup
+
+namespace Filter
+variable {α β γ ι ι' : Type*}
+
+lemma IsBoundedUnder.le_of_finite [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)] [Finite β]
+    {f : Filter β} {u : β → α} : IsBoundedUnder (· ≤ ·) f u :=
+  (Set.toFinite _).bddAbove.isBoundedUnder univ_mem
+
+lemma IsBoundedUnder.ge_of_finite [Nonempty α] [Preorder α] [IsDirected α (· ≥ ·)] [Finite β]
+    {f : Filter β} {u : β → α} : IsBoundedUnder (· ≥ ·) f u :=
+  (Set.toFinite _).bddBelow.isBoundedUnder univ_mem
+
+end Filter