Interactions between the Lebesgue integral and norms

theorem MeasureTheory.lintegral_ofReal_le_lintegral_enorm {α : Type u_1} [MeasurableSpace α] {μ : Measure α} (f : α → ℝ) : ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂μ

theorem MeasureTheory.lintegral_enorm_of_ae_nonneg {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ℝ} (h_nonneg : 0 ≤ᶠ[ae μ] f) : ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

theorem MeasureTheory.lintegral_enorm_of_nonneg {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {f : α → ℝ} (h_nonneg : 0 ≤ f) : ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ