theorem averagedWith_weightedSum {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] {D : Set H} {I : Type v} [Fintype I] (ω α : I → ℝ) (T : I → ↑D → H) (hω : ∀ (i : I), ω i ∈ Set.Icc 0 1) (hω_sum : ∑ i : I, ω i = 1) (hT : ∀ (i : I), AveragedWith (α i) (T i)) : AveragedWith (∑ i : I, ω i * α i) fun (x : ↑D) => ∑ i : I, ω i • T i x

Proposition 4.42: a finite convex combination of α i-averaged operators on a subset of a real Hilbert space is (\sum i, ω i * α i)-averaged.