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‖ₑ ∂μ

@[deprecated MeasureTheory.lintegral_ofReal_le_lintegral_enorm (since := "2025-01-17")]

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

Alias of MeasureTheory.lintegral_ofReal_le_lintegral_enorm.

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) ∂μ

@[deprecated MeasureTheory.lintegral_enorm_of_ae_nonneg (since := "2025-01-17")]

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

Alias of MeasureTheory.lintegral_enorm_of_ae_nonneg.

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

@[deprecated MeasureTheory.lintegral_enorm_of_nonneg (since := "2025-01-17")]

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

Alias of MeasureTheory.lintegral_enorm_of_nonneg.