isFixedPt_fixedPoint_iterate — Mathlib

English

If f has a contracting iterate f^[n], then the fixed point of that iterate is a fixed point of f.

Русский

Если f имеет сжатый параметр итерации f^[n], то фиксированная точка этой итерации является фиксированной точкой f.

LaTeX

$$$\\text{IsFixedPt}(f, \\mathrm{fixedPoint}(f^{[n]}, hf))$$$

Lean4

/-- If a map `f` has a contracting iterate `f^[n]`, then the fixed point of `f^[n]` is also a fixed
point of `f`. -/
theorem isFixedPt_fixedPoint_iterate {n : ℕ} (hf : ContractingWith K f^[n]) : IsFixedPt f (hf.fixedPoint f^[n]) :=
  by
  set x := hf.fixedPoint f^[n]
  have hx : f^[n] x = x := hf.fixedPoint_isFixedPt
  have := hf.toLipschitzWith.dist_le_mul x (f x)
  rw [← iterate_succ_apply, iterate_succ_apply', hx] at this
  contrapose! this
  simpa using mul_lt_mul_of_pos_right (NNReal.coe_lt_one.2 hf.left) <| dist_pos.2 (Ne.symm this)

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