List Utils

Small list-fold lemmas used throughout TorchLean proof files.

These are intentionally generic (not NN-specific) and live in a single place so large proofs do not accumulate many near-duplicate "foldl max" / "foldl add" helper lemmas.

theorem List.foldl_max_le_of_le {ι β : Type} [LinearOrder β] (l : List ι) (f : ι → β) {acc eps : β} (hacc : acc ≤ eps) (hf : ∀ (i : ι), i ∈ l → f i ≤ eps) : foldl (fun (a : β) (i : ι) => max a (f i)) acc l ≤ eps

foldl max upper bound helper.

If the initial accumulator and every f i are ≤ eps, then the folded maximum is also ≤ eps.

theorem List.le_foldl_max_init {ι β : Type} [LinearOrder β] (l : List ι) (f : ι → β) (acc : β) : acc ≤ foldl (fun (a : β) (i : ι) => max a (f i)) acc l

Lower bound helper for foldl max.

The folded maximum is always at least as large as the initial accumulator.

theorem List.le_foldl_max_of_mem {ι β : Type} [LinearOrder β] (l : List ι) (f : ι → β) {acc : β} {i : ι} (hi : i ∈ l) : f i ≤ foldl (fun (a : β) (j : ι) => max a (f j)) acc l

Membership helper for foldl max.

If i ∈ l, then f i is ≤ the folded maximum.

theorem List.foldl_add_init {α β : Type} [AddMonoid β] (l : List α) (f : α → β) (acc : β) : foldl (fun (a : β) (x : α) => a + f x) acc l = acc + foldl (fun (a : β) (x : α) => a + f x) 0 l

Turn foldl (fun a x => a + f x) acc into acc + foldl (fun a x => a + f x) 0.

This is the standard "peel off the initial accumulator" lemma for left folds over +.

theorem List.add_foldl_add0 {α β : Type} [AddMonoid β] (l : List α) (f : α → β) (acc : β) : acc + foldl (fun (a : β) (x : α) => a + f x) 0 l = foldl (fun (a : β) (x : α) => a + f x) acc l