Combining Finitely Many A.E. Equalities

This file provides a key technical lemma for combining finitely many a.e.-equalities into an a.e.-equality of the finite sum.

Main results

• finset_sum_ae_eq: If each f i is a.e.-equal to g i on a finite index set s, then the pointwise sums over s are a.e.-equal.

theorem finset_sum_ae_eq {α : Type u_1} {ι : Type u_2} {β : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [AddCommMonoid β] (s : Finset ι) (f g : ι → α → β) (h : ∀ i ∈ s, f i =ᵐ[μ] g i) : (fun (ω : α) => ∑ i ∈ s, f i ω) =ᵐ[μ] fun (ω : α) => ∑ i ∈ s, g i ω

Combine finitely many a.e.-equalities into an a.e.-equality of the finite sum.

If each f i is a.e.-equal to g i on a finite index set s, then the pointwise sums over s are a.e.-equal. Uses EventuallyEq.fun_add to combine equalities.