Joint initial-time regularity of the actual explicit lower velocity sum.

theorem AVenhance.Infra.Section4.IteratesVelocitySmooth.velocity_contDiffOn_list {α : Type u_1} (P : List α) (f : α → AmnrSpace → ℝ) (S : Set AmnrSpace) (hf : ∀ p ∈ P, ContDiffOn ℝ (↑⊤) (f p) S) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => (List.map (fun (p : α) => f p z) P).sum) S

theorem AVenhance.Infra.Section4.iterateVelocitySplit_smooth_up_to_initial {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {v : ℝ → Homogenization.Vec 2 → ℝ} (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)) (P : List (List (Fin 2) × List (Fin 2))) : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => iterateVelocitySplit P (b z.1) (v z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)

The explicit velocity sum is smooth jointly up to zero. This supplies a regular representative of the actual material error on the positive cell.