Integrated all-order drift errors with linear lower-energy dependence.

theorem AVenhance.Infra.Section4.IteratesVelocityEnergy.velocity_list_integrable {α : Type u_1} (P : List α) (f : α → AmnrSpace → ℝ) (hf : ∀ p ∈ P, MeasureTheory.IntegrableOn (f p) timeCube MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (z : AmnrSpace) => (List.map (fun (p : α) => f p z) P).sum) timeCube MeasureTheory.volume

theorem AVenhance.Infra.Section4.IteratesVelocityEnergy.velocity_list_integral {α : Type u_1} (P : List α) (f : α → AmnrSpace → ℝ) (hf : ∀ p ∈ P, MeasureTheory.IntegrableOn (f p) timeCube MeasureTheory.volume) : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, (List.map (fun (p : α) => f p z) P).sum = (List.map (fun (p : α) => ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, f p z) P).sum

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