L^p-seminorms on count and dirac

@[simp]

theorem MeasureTheory.eLpNorm_dirac {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace ε] [ContinuousENorm ε] {p : ENNReal} (f : α → ε) (i : α) (hp : p ≠ 0) : eLpNorm f p (Measure.dirac i) = ‖f i‖ₑ

theorem MeasureTheory.enorm_le_eLpNorm_count {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace ε] [ContinuousENorm ε] {p : ENNReal} (f : α → ε) (i : α) (hp : p ≠ 0) : ‖f i‖ₑ ≤ eLpNorm f p Measure.count

theorem MeasureTheory.eLpNorm_count_lt_top_of_lt {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {p : ENNReal} [Finite α] (h : ∀ (i : α), ‖f i‖ₑ < ⊤) : eLpNorm f p Measure.count < ⊤

theorem MeasureTheory.eLpNorm_count_lt_top {α : Type u_1} {ε : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} {p : ENNReal} [Finite α] (hp : p ≠ 0) : eLpNorm f p Measure.count < ⊤ ↔ ∀ (i : α), ‖f i‖ₑ < ⊤