English
The product of a list of Lipschitz endomorphisms is Lipschitz, with constant the product of their constants in the list.
Русский
Произведение списка липшицевых эндоморфизмов является липшицевым, константа равна произведению констант из списка.
LaTeX
$$$\\forall l:\\text{List }\\iota,\\, \\text{LipschitzWith } (l.map K).prod (l.map f).prod$$$
Lean4
/-- The product of a list of Lipschitz continuous endomorphisms is a Lipschitz continuous
endomorphism. -/
protected theorem list_prod (f : ι → Function.End α) (K : ι → ℝ≥0) (h : ∀ i, LipschitzWith (K i) (f i)) :
∀ l : List ι, LipschitzWith (l.map K).prod (l.map f).prod
| [] => by simpa using LipschitzWith.id
| i :: l => by
simp only [List.map_cons, List.prod_cons]
exact (h i).mul_end (LipschitzWith.list_prod f K h l)
