Actual ordered derivatives of finite correction sums.

theorem AVenhance.Infra.Section4.amnr_list_sum_contDiff (T : List (AmnrSpace → ℝ)) (hT : ∀ f ∈ T, ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) T.sum

theorem AVenhance.Infra.Section4.amnrWord_list_sum_global {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) (T : List (AmnrSpace → ℝ)) (hT : ∀ f ∈ T, ContDiff ℝ (↑⊤) f) (w : List (Option (Fin 2))) : amnrWord b w T.sum = (List.map (amnrWord b w) T).sum

Ordered differentiation commutes with a finite sum of actual smooth fields.

theorem AVenhance.Infra.Section4.amnr_list_sum_apply (T : List (AmnrSpace → ℝ)) (z : AmnrSpace) : T.sum z = (List.map (fun (f : AmnrSpace → ℝ) => f z) T).sum

Evaluation of a finite function sum is the sum of its actual values.