Exact principal, first, and high stream orders in the integrated flux.

theorem AVenhance.Infra.Section4.iterate_three_order_list_sum {α : Type u_1} (P : List α) (n : α → ℕ) (f : α → ℝ) : (List.map f P).sum = (List.map f (List.filter (fun (p : α) => n p == 0) P)).sum + (List.map f (List.filter (fun (p : α) => n p == 1) P)).sum + (List.map f (List.filter (fun (p : α) => decide (2 ≤ n p)) P)).sum

Split a finite sum into its zero, first, and high coefficient orders.