iterate — Mathlib

English

Iterates of a Lipschitz function are Lipschitz: if f is Lipschitz with constant K, then f^[n] is Lipschitz with constant K^n.

Русский

Итерации липшицева отображения сохраняют липшицевость: если f имеет константу K, то f^n имеет константу K^n.

LaTeX

$$$\\text{LipschitzWith } K f \\Rightarrow \\forall n, \\text{ LipschitzWith } (K^n) (f^{[n]})$$$

Lean4

/-- Iterates of a Lipschitz function are Lipschitz. -/
protected theorem iterate {f : α → α} (hf : LipschitzWith K f) : ∀ n, LipschitzWith (K ^ n) f^[n]
  | 0 => by simpa only [pow_zero] using LipschitzWith.id
  | n + 1 => by rw [pow_succ]; exact (LipschitzWith.iterate hf n).comp hf

Похожие утверждения