pow_end — Mathlib

English

Iterates of an endomorphism maintain Lipschitz property with exponentiated constants: f^n is Lipschitz with (K^n).

Русский

Итерация липшицева эндоморфизма сохраняет липшицевость: f^n липшицево с константой K^n.

LaTeX

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

Lean4

protected theorem pow_end {f : Function.End α} {K} (h : LipschitzWith K f) :
    ∀ n : ℕ, LipschitzWith (K ^ n) (f ^ n : Function.End α)
  | 0 => by simpa only [pow_zero] using LipschitzWith.id
  | n + 1 => by
    rw [pow_succ, pow_succ]
    exact (LipschitzWith.pow_end h n).mul_end h

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