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

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

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

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

theorem AVenhance.Infra.Section4.iterate_truncated_velocity_split_linear_energy_bound {s : ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {v : ℝ → Homogenization.Vec 2 → ℝ} {a : AmnrSpace → ℝ} (hs1 : s ≤ 1) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (ha : ContinuousOn a (Set.Ici 0 ×ˢ Set.univ)) (P : List (List (Fin 2) × List (Fin 2))) (D G : ℕ → ℝ) {H : ℝ} (hD : ∀ (j : ℕ), 0 ≤ D j) (hG : ∀ (j : ℕ), 0 ≤ G j) (hH : 0 ≤ H) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ P, ∀ (j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ D p.1.length) (hEa : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, a z ^ 2 ≤ H ^ 2) (hEv : ∀ p ∈ P, (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ G p.2.length ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, a z * iterateVelocitySplit P (b z.1) (v z.1) z.2| ≤ 2 * H * (List.map (fun (p : List (Fin 2) × List (Fin 2)) => D p.1.length * G p.2.length) P).sum

The actual split sum is bounded linearly by the lower scalar energy bounds. This is the form used in the norm recurrence, before induction.

theorem AVenhance.Infra.Section4.iterate_truncated_material_error_linear_energy_bound {s : ℝ} {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {v : ℝ → Homogenization.Vec 2 → ℝ} {a : AmnrSpace → ℝ} (hs1 : s ≤ 1) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (ha : ContinuousOn a (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (D G : ℕ → ℝ) {H : ℝ} (hD : ∀ (j : ℕ), 0 ≤ D j) (hG : ∀ (j : ℕ), 0 ≤ G j) (hH : 0 ≤ H) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w), ∀ (j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ D p.1.length) (hEa : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, a z ^ 2 ≤ H ^ 2) (hEv : ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p.2 (v t))) ≤ G p.2.length ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, a z * iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) z| ≤ 2 * H * ∑ j ∈ Finset.range w.length, ↑(w.length.choose (j + 1)) * D (j + 1) * G (w.length - (j + 1))

The actual drift error has an explicit binomially grouped linear energy bound. Every scalar gradient premise is at a strictly lower word length.