Prerequisites for nnLpNorm

LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean

@@ -0,0 +1,13 @@
+import Mathlib.MeasureTheory.Function.EssSup
+import LeanAPAP.Mathlib.MeasureTheory.OuterMeasure.AE
+import LeanAPAP.Mathlib.Order.LiminfLimsup
+
+open Filter MeasureTheory
+
+variable {α β : Type*} [CompleteLinearOrder β] {m : MeasurableSpace α} {μ : Measure α}
+
+lemma essSup_eq_iSup (hμ : ∀ a, μ {a} ≠ 0) (f : α → β) : essSup f μ = ⨆ i, f i := by
+  rw [essSup, ae_eq_top.2 hμ, limsup_top]
+
+lemma essInf_eq_iInf (hμ : ∀ a, μ {a} ≠ 0) (f : α → β) : essInf f μ = ⨅ i, f i := by
+  rw [essInf, ae_eq_top.2 hμ, liminf_top]

LeanAPAP/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -0,0 +1,13 @@
+import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+import LeanAPAP.Prereqs.EssSupCount
+
+open TopologicalSpace MeasureTheory Filter
+open scoped NNReal ENNReal Topology
+
+variable {α E : Type*} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E]
+
+lemma snormEssSup_eq_iSup (hμ : ∀ a, μ {a} ≠ 0) (f : α → E) : snormEssSup f μ = ⨆ a, ↑‖f a‖₊ :=
+  essSup_eq_iSup hμ _
+
+@[simp] lemma snormEssSup_count [MeasurableSingletonClass α] (f : α → E) :
+    snormEssSup f .count = ⨆ a, ↑‖f a‖₊ := essSup_count _

LeanAPAP/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -0,0 +1,11 @@
+import Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
+import LeanAPAP.Mathlib.MeasureTheory.OuterMeasure.AE
+
+namespace MeasureTheory
+variable {α β : Type*} [TopologicalSpace β] {m : MeasurableSpace α} [DiscreteMeasurableSpace α]
+  [Finite α] {f : α → β} {μ : Measure α}
+
+-- TODO: Rename `StronglyMeasurable.of_finite` to `StronglyMeasurable.of_discrete`
+lemma AEStronglyMeasurable.of_discrete : AEStronglyMeasurable f μ := ⟨_, .of_finite _, ae_eq_rfl⟩
+
+end MeasureTheory

LeanAPAP/Mathlib/MeasureTheory/Measure/Count.lean

@@ -0,0 +1,5 @@
+import Mathlib.MeasureTheory.Measure.Count
+
+open MeasureTheory
+
+attribute [simp] Measure.count_singleton

LeanAPAP/Mathlib/MeasureTheory/OuterMeasure/AE.lean

@@ -0,0 +1,16 @@
+import Mathlib.MeasureTheory.OuterMeasure.AE
+
+open Filter MeasureTheory ENNReal Set
+
+variable {F α β : Type*} [FunLike F (Set α) ℝ≥0∞] [OuterMeasureClass F α] {μ : F} {f : α → β}
+
+lemma ae_eq_rfl : f =ᵐ[μ] f := ae_eq_refl _
+
+@[simp] lemma ae_eq_top  : ae μ = ⊤ ↔ ∀ a, μ {a} ≠ 0 := by
+  simp only [Filter.ext_iff, mem_ae_iff, mem_top, ne_eq]
+  refine ⟨fun h a ha ↦ by simpa [ha] using (h {a}ᶜ).1, fun h s ↦ ⟨fun hs ↦ ?_, ?_⟩⟩
+  · rw [← compl_empty_iff, ← not_nonempty_iff_eq_empty]
+    rintro ⟨a, ha⟩
+    exact h _ $ measure_mono_null (singleton_subset_iff.2 ha) hs
+  · rintro rfl
+    simp

LeanAPAP/Mathlib/Order/LiminfLimsup.lean

@@ -0,0 +1,9 @@
+import Mathlib.Order.LiminfLimsup
+
+namespace Filter
+variable {α β : Type*} [CompleteLattice α]
+
+@[simp] lemma limsup_top (u : β → α) : limsup u ⊤ = ⨆ i, u i := by simp [limsup_eq_iInf_iSup]
+@[simp] lemma liminf_top (u : β → α) : liminf u ⊤ = ⨅ i, u i := by simp [liminf_eq_iSup_iInf]
+
+end Filter

LeanAPAP/Prereqs/EssSupCount.lean

@@ -0,0 +1,15 @@
+import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
+import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
+import LeanAPAP.Mathlib.MeasureTheory.OuterMeasure.AE
+import LeanAPAP.Mathlib.Order.LiminfLimsup
+
+open Filter MeasureTheory
+
+variable {α β : Type*} [CompleteLinearOrder β] {m : MeasurableSpace α} [MeasurableSingletonClass α]
+  {μ : Measure α}
+
+@[simp] lemma essSup_count (f : α → β) : essSup f .count = ⨆ i, f i :=
+  essSup_eq_iSup (by simp) _
+
+@[simp] lemma essInf_count (f : α → β) : essInf f .count = ⨅ i, f i :=
+  essInf_eq_iInf (by simp) _