Smooth finite folds #
The traversal order is fixed, while the initial accumulator and each visited value may depend on the parameters. The update rule can operate on different normed spaces for its accumulator and entries. No associativity, commutativity, or permutation argument is needed.
theorem
List.contDiffAt_foldl
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{ι : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
(indices : List ι)
{step : F → G → F}
(hstep : ContDiff 𝕜 n fun (p : F × G) => step p.1 p.2)
{initial : E → F}
{term : ι → E → G}
{x : E}
(hinit : ContDiffAt 𝕜 n initial x)
(hterm : ∀ i ∈ indices, ContDiffAt 𝕜 n (term i) x)
:
ContDiffAt 𝕜 n (fun (y : E) => foldl (fun (acc : F) (i : ι) => step acc (term i y)) (initial y) indices) x
A smooth update rule preserves local smoothness along a fixed traversal. Only the visited entries and initial accumulator need to be smooth near the input.
theorem
List.contDiff_foldl
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{ι : Type u_5}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedAddCommGroup G]
[NormedSpace 𝕜 G]
{n : WithTop ℕ∞}
(indices : List ι)
{step : F → G → F}
(hstep : ContDiff 𝕜 n fun (p : F × G) => step p.1 p.2)
{initial : E → F}
{term : ι → E → G}
(hinit : ContDiff 𝕜 n initial)
(hterm : ∀ i ∈ indices, ContDiff 𝕜 n (term i))
:
A fixed traversal of a smooth update rule preserves smoothness of the accumulator. Only entries visited by the list need to be smooth; repetition and empty traversals are allowed.