The full first-coefficient-order stream contribution.

theorem AVenhance.Infra.Section4.IteratesFirstStreamSum.first_stream_abs_sum {α : Type u_1} (P : List α) (f : α → ℝ) : |(List.map f P).sum| ≤ (List.map (fun (p : α) => |f p|) P).sum