∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {r : NNReal},
  MeasureTheory.Integrable f μ →
    0 ≤ ∫ (x : α), f x ∂μ → (∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r) → MeasureTheory.eLpNorm f 1 μ ≤ 2 * μ Set.univ * ↑r