The actual first stream coefficient sum over the time cell.

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