theorem MeasureTheory.average_add {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) : ⨍ (a : α), (f + g) a ∂μ = ⨍ (a : α), f a ∂μ + ⨍ (a : α), g a ∂μ

theorem MeasureTheory.average_fun_add {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f g : α → E} (hf : Integrable f μ) (hg : Integrable g μ) : ⨍ (a : α), f a + g a ∂μ = ⨍ (a : α), f a ∂μ + ⨍ (a : α), g a ∂μ

Eta-expanded form of MeasureTheory.average_add

theorem MeasureTheory.setAverage_add {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {s : Set α} {f g : α → E} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) : ⨍ (a : α) in s, (f + g) a ∂μ = ⨍ (a : α) in s, f a ∂μ + ⨍ (a : α) in s, g a ∂μ

theorem MeasureTheory.setAverage_fun_add {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {s : Set α} {f g : α → E} (hf : IntegrableOn f s μ) (hg : IntegrableOn g s μ) : ⨍ (a : α) in s, f a + g a ∂μ = ⨍ (a : α) in s, f a ∂μ + ⨍ (a : α) in s, g a ∂μ

Eta-expanded form of MeasureTheory.setAverage_add

theorem MeasureTheory.average_const_mul {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} {L : Type u_3} [RCLike L] (r : L) (f : α → L) : ⨍ (a : α), r * f a ∂μ = r * ⨍ (a : α), f a ∂μ

@[simp]

theorem MeasureTheory.average_count {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] [Module ℚ≥0 E] [CompleteSpace E] [MeasurableSingletonClass α] [Fintype α] (f : α → E) : ⨍ (a : α), f a ∂Measure.count = Finset.univ.expect fun (a : α) => f a

theorem MeasureTheory.average_nonneg_of_ae {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f : α → E} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] (hf : 0 ≤ᵐ[μ] f) : 0 ≤ ⨍ (a : α), f a ∂μ

The average of a function which is nonnegative almost everywhere is nonnegative.

theorem MeasureTheory.average_nonneg {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : Measure α} {f : α → E} [PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] [ClosedIciTopology E] (hf : 0 ≤ f) : 0 ≤ ⨍ (a : α), f a ∂μ