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 := "2026-11-06")]

theorem MeasureTheory.lintegral_ofReal_le_lintegral_enorm {α : 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 ≤ᵐ[μ] f) : ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ

@[deprecated MeasureTheory.lintegral_eNorm_of_ae_nonneg (since := "2026-11-06")]

theorem MeasureTheory.lintegral_enorm_of_ae_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_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 := "2026-11-06")]

theorem MeasureTheory.lintegral_enorm_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.