theorem laverage_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal} (h : ∀ᵐ (a : α) ∂μ, f a ≤ g a) : ⨍⁻ (a : α), f a ∂μ ≤ ⨍⁻ (a : α), g a ∂μ

theorem setLAverage_mono_ae {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal} (h : ∀ᵐ (a : α) ∂μ, f a ≤ g a) : ⨍⁻ (a : α) in s, f a ∂μ ≤ ⨍⁻ (a : α) in s, g a ∂μ

theorem setLAverage_le_essSup {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (f : α → ENNReal) : ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

theorem laverage_le_essSup {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) : ⨍⁻ (x : α), f x ∂μ ≤ essSup f μ