Mathlib.Order.Iterate

Module docstring

{"# Inequalities on iterates

In this file we prove some inequalities comparing f^[n] x and g^[n] x where f and g are two self-maps that commute with each other.

Current selection of inequalities is motivated by formalization of the rotation number of a circle homeomorphism. ","### Comparison of two sequences

If $f$ is a monotone function, then $∀ k, x{k+1} ≤ f(xk)$ implies that $xk$ grows slower than $f^k(x0)$, and similarly for the reversed inequalities. If $xk$ and $yk$ are two sequences such that $x{k+1} ≤ f(xk)$ and $y{k+1} ≥ f(yk)$ for all $k < n$, then $x0 ≤ y0$ implies $xn ≤ yn$, see Monotone.seq_le_seq.

If some of the inequalities in this lemma are strict, then we have $xn < yn$. The rest of the lemmas in this section formalize this fact for different inequalities made strict. ","### Iterates of two functions

In this section we compare the iterates of a monotone function f : α → α to iterates of any function g : β → β. If h : β → α satisfies h ∘ g ≤ f ∘ h, then h (g^[n] x) grows slower than f^[n] (h x), and similarly for the reversed inequality.

Then we specialize these two lemmas to the case β = α, h = id. ","### Comparison of iterations and the identity function

If $f(x) ≤ x$ for all $x$ (we express this as f ≤ id in the code), then the same is true for any iterate of $f$, and similarly for the reversed inequality. ","### Iterates of commuting functions

If f and g are monotone and commute, then f x ≤ g x implies f^[n] x ≤ g^[n] x, see Function.Commute.iterate_le_of_map_le. We also prove two strict inequality versions of this lemma, as well as iff versions. "}

Monotone.seq_le_seq theorem

 (hf : Monotone f) (n : ℕ) (h₀ : x 0 ≤ y 0) (hx : ∀ k < n, x (k + 1) ≤ f (x k)) (hy : ∀ k < n, f (y k) ≤ y (k + 1)) :
  x n ≤ y n

Full source

theorem seq_le_seq (hf : Monotone f) (n : ℕ) (h₀ : x 0 ≤ y 0) (hx : ∀ k < n, x (k + 1) ≤ f (x k))
    (hy : ∀ k < n, f (y k) ≤ y (k + 1)) : x n ≤ y n := by
  induction n with
  | zero => exact h₀
  | succ n ihn =>
    refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
    · exact fun k hk => hx _ (hk.trans n.lt_succ_self)
    · exact fun k hk => hy _ (hk.trans n.lt_succ_self)

Monotone Iteration Comparison Theorem

Informal description

Let $f$ be a monotone function and $n$ be a natural number. Given two sequences $(x_k)$ and $(y_k)$ such that: 1. $x_0 \leq y_0$, 2. For all $k < n$, $x_{k+1} \leq f(x_k)$, 3. For all $k < n$, $f(y_k) \leq y_{k+1}$, then $x_n \leq y_n$.

Monotone.seq_pos_lt_seq_of_lt_of_le theorem

 (hf : Monotone f) {n : ℕ} (hn : 0 < n) (h₀ : x 0 ≤ y 0) (hx : ∀ k < n, x (k + 1) < f (x k))
  (hy : ∀ k < n, f (y k) ≤ y (k + 1)) : x n < y n

Full source

theorem seq_pos_lt_seq_of_lt_of_le (hf : Monotone f) {n : ℕ} (hn : 0 < n) (h₀ : x 0 ≤ y 0)
    (hx : ∀ k < n, x (k + 1) < f (x k)) (hy : ∀ k < n, f (y k) ≤ y (k + 1)) : x n < y n := by
  induction n with
  | zero => exact hn.false.elim
  | succ n ihn =>
  suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)
  cases n with
  | zero => exact h₀
  | succ n =>
    refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le <;>
    exact hk.trans n.succ.lt_succ_self

Strict inequality for monotone function iterates with mixed conditions

Informal description

Let $f$ be a monotone function and $n$ be a positive natural number. Suppose two sequences $(x_k)$ and $(y_k)$ satisfy: 1. $x_0 \leq y_0$, 2. For all $k < n$, $x_{k+1} < f(x_k)$, 3. For all $k < n$, $f(y_k) \leq y_{k+1}$. Then $x_n < y_n$.

Monotone.seq_pos_lt_seq_of_le_of_lt theorem

 (hf : Monotone f) {n : ℕ} (hn : 0 < n) (h₀ : x 0 ≤ y 0) (hx : ∀ k < n, x (k + 1) ≤ f (x k))
  (hy : ∀ k < n, f (y k) < y (k + 1)) : x n < y n

Full source

theorem seq_pos_lt_seq_of_le_of_lt (hf : Monotone f) {n : ℕ} (hn : 0 < n) (h₀ : x 0 ≤ y 0)
    (hx : ∀ k < n, x (k + 1) ≤ f (x k)) (hy : ∀ k < n, f (y k) < y (k + 1)) : x n < y n :=
  hf.dual.seq_pos_lt_seq_of_lt_of_le hn h₀ hy hx

Strict inequality for monotone iterates with mixed conditions ($\leq$ and $<$)

Informal description

Let $f$ be a monotone function and $n$ be a positive natural number. Given two sequences $(x_k)$ and $(y_k)$ such that: 1. $x_0 \leq y_0$, 2. For all $k < n$, $x_{k+1} \leq f(x_k)$, 3. For all $k < n$, $f(y_k) < y_{k+1}$, then $x_n < y_n$.

Monotone.seq_lt_seq_of_lt_of_le theorem

 (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0) (hx : ∀ k < n, x (k + 1) < f (x k)) (hy : ∀ k < n, f (y k) ≤ y (k + 1)) :
  x n < y n

Full source

theorem seq_lt_seq_of_lt_of_le (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0)
    (hx : ∀ k < n, x (k + 1) < f (x k)) (hy : ∀ k < n, f (y k) ≤ y (k + 1)) : x n < y n := by
  cases n
  exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy]

Strict inequality for monotone iterates with initial strict condition

Informal description

Let $f$ be a monotone function and $n$ be a natural number. Given two sequences $(x_k)$ and $(y_k)$ such that: 1. $x_0 < y_0$, 2. For all $k < n$, $x_{k+1} < f(x_k)$, 3. For all $k < n$, $f(y_k) \leq y_{k+1}$, then $x_n < y_n$.

Monotone.seq_lt_seq_of_le_of_lt theorem

 (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0) (hx : ∀ k < n, x (k + 1) ≤ f (x k)) (hy : ∀ k < n, f (y k) < y (k + 1)) :
  x n < y n

Full source

theorem seq_lt_seq_of_le_of_lt (hf : Monotone f) (n : ℕ) (h₀ : x 0 < y 0)
    (hx : ∀ k < n, x (k + 1) ≤ f (x k)) (hy : ∀ k < n, f (y k) < y (k + 1)) : x n < y n :=
  hf.dual.seq_lt_seq_of_lt_of_le n h₀ hy hx

Strict inequality for monotone iterates with mixed conditions ($\leq$ and $<$) and strict initial condition

Informal description

Let $f$ be a monotone function and $n$ be a natural number. Given two sequences $(x_k)_{k=0}^n$ and $(y_k)_{k=0}^n$ such that: 1. $x_0 < y_0$, 2. For all $k < n$, $x_{k+1} \leq f(x_k)$, 3. For all $k < n$, $f(y_k) < y_{k+1}$, then $x_n < y_n$.

Monotone.le_iterate_comp_of_le theorem

(hf : Monotone f) (H : h ∘ g ≤ f ∘ h) (n : ℕ) : h ∘ g^[n] ≤ f^[n] ∘ h

Full source

theorem le_iterate_comp_of_le (hf : Monotone f) (H : h ∘ g ≤ f ∘ h) (n : ℕ) :
    h ∘ g^[n] ≤ f^[n]f^[n] ∘ h := fun x => by
  apply hf.seq_le_seq n <;> intros <;>
    simp [iterate_succ', -iterate_succ, comp_apply, id_eq, le_refl]
  case hx => exact H _

Monotone Iteration Comparison: $h \circ g^{[n]} \leq f^{[n]} \circ h$ under $h \circ g \leq f \circ h$

Informal description

Let $f : \alpha \to \alpha$ be a monotone function and $g : \beta \to \beta$ be any function. If $h : \beta \to \alpha$ satisfies $h \circ g \leq f \circ h$, then for any natural number $n$, the composition $h \circ g^{[n]}$ is pointwise less than or equal to $f^{[n]} \circ h$, i.e., for all $x \in \beta$, we have $h(g^{[n]}(x)) \leq f^{[n]}(h(x))$.

Monotone.iterate_comp_le_of_le theorem

(hf : Monotone f) (H : f ∘ h ≤ h ∘ g) (n : ℕ) : f^[n] ∘ h ≤ h ∘ g^[n]

Full source

theorem iterate_comp_le_of_le (hf : Monotone f) (H : f ∘ h ≤ h ∘ g) (n : ℕ) :
    f^[n]f^[n] ∘ h ≤ h ∘ g^[n] :=
  hf.dual.le_iterate_comp_of_le H n

Monotone Iteration Comparison: $f^{[n]} \circ h \leq h \circ g^{[n]}$ under $f \circ h \leq h \circ g$

Informal description

Let $f : \alpha \to \alpha$ be a monotone function and $g : \beta \to \beta$ be any function. If $h : \beta \to \alpha$ satisfies $f \circ h \leq h \circ g$, then for any natural number $n$, the composition $f^{[n]} \circ h$ is pointwise less than or equal to $h \circ g^{[n]}$, i.e., for all $x \in \beta$, we have $f^{[n]}(h(x)) \leq h(g^{[n]}(x))$.

Monotone.iterate_le_of_le theorem

{g : α → α} (hf : Monotone f) (h : f ≤ g) (n : ℕ) : f^[n] ≤ g^[n]

Full source

/-- If `f ≤ g` and `f` is monotone, then `f^[n] ≤ g^[n]`. -/
theorem iterate_le_of_le {g : α → α} (hf : Monotone f) (h : f ≤ g) (n : ℕ) : f^[n] ≤ g^[n] :=
  hf.iterate_comp_le_of_le h n

Monotone Iteration Preserves Inequality: $f^{[n]} \leq g^{[n]}$ under $f \leq g$

Informal description

Let $f, g : \alpha \to \alpha$ be functions such that $f$ is monotone and $f \leq g$ pointwise (i.e., $f(x) \leq g(x)$ for all $x \in \alpha$). Then for any natural number $n$, the $n$-th iterate of $f$ is pointwise less than or equal to the $n$-th iterate of $g$, i.e., $f^{[n]}(x) \leq g^{[n]}(x)$ for all $x \in \alpha$.

Monotone.le_iterate_of_le theorem

{g : α → α} (hg : Monotone g) (h : f ≤ g) (n : ℕ) : f^[n] ≤ g^[n]

Full source

/-- If `f ≤ g` and `g` is monotone, then `f^[n] ≤ g^[n]`. -/
theorem le_iterate_of_le {g : α → α} (hg : Monotone g) (h : f ≤ g) (n : ℕ) : f^[n] ≤ g^[n] :=
  hg.dual.iterate_le_of_le h n

Monotonicity Preserves Iterated Inequality: $f^{[n]} \leq g^{[n]}$ under $f \leq g$ and $g$ monotone

Informal description

Let $f, g : \alpha \to \alpha$ be functions such that $g$ is monotone and $f(x) \leq g(x)$ for all $x \in \alpha$. Then for any natural number $n$, the $n$-th iterate of $f$ satisfies $f^{[n]}(x) \leq g^{[n]}(x)$ for all $x \in \alpha$.

Function.id_le_iterate_of_id_le theorem

(h : id ≤ f) (n : ℕ) : id ≤ f^[n]

Full source

/-- If $x ≤ f x$ for all $x$ (we write this as `id ≤ f`), then the same is true for any iterate
`f^[n]` of `f`. -/
theorem id_le_iterate_of_id_le (h : id ≤ f) (n : ℕ) : id ≤ f^[n] := by
  simpa only [iterate_id] using monotone_id.iterate_le_of_le h n

Iterates Preserve Pointwise Inequality with Identity: $\mathrm{id} \leq f^{[n]}$ under $\mathrm{id} \leq f$

Informal description

If a function $f \colon \alpha \to \alpha$ satisfies $x \leq f(x)$ for all $x \in \alpha$ (i.e., $\mathrm{id} \leq f$), then for any natural number $n$, the $n$-th iterate $f^{[n]}$ of $f$ also satisfies $x \leq f^{[n]}(x)$ for all $x \in \alpha$.

Function.iterate_le_id_of_le_id theorem

(h : f ≤ id) (n : ℕ) : f^[n] ≤ id

Full source

theorem iterate_le_id_of_le_id (h : f ≤ id) (n : ℕ) : f^[n] ≤ id :=
  @id_le_iterate_of_id_le αᵒᵈ _ f h n

Iterates Remain Below Identity under $f \leq \mathrm{id}$

Informal description

For any function $f \colon \alpha \to \alpha$ satisfying $f(x) \leq x$ for all $x \in \alpha$ (i.e., $f \leq \mathrm{id}$), the $n$-th iterate $f^{[n]}$ of $f$ satisfies $f^{[n]}(x) \leq x$ for all $x \in \alpha$ and any natural number $n$.

Function.monotone_iterate_of_id_le theorem

(h : id ≤ f) : Monotone fun m => f^[m]

Full source

theorem monotone_iterate_of_id_le (h : id ≤ f) : Monotone fun m => f^[m] :=
  monotone_nat_of_le_succ fun n x => by
    rw [iterate_succ_apply']
    exact h _

Monotonicity of Iterates for Functions Dominating the Identity

Informal description

If a function $f : \alpha \to \alpha$ satisfies $f(x) \geq x$ for all $x \in \alpha$ (i.e., $\text{id} \leq f$), then the sequence of iterates $f^{[n]}$ is monotone with respect to $n \in \mathbb{N}$. In other words, for any natural numbers $m \leq n$, we have $f^{[m]}(x) \leq f^{[n]}(x)$ for all $x \in \alpha$.

Function.antitone_iterate_of_le_id theorem

(h : f ≤ id) : Antitone fun m => f^[m]

Full source

theorem antitone_iterate_of_le_id (h : f ≤ id) : Antitone fun m => f^[m] := fun m n hmn =>
  @monotone_iterate_of_id_le αᵒᵈ _ f h m n hmn

Antitonicity of Iterates for Functions Bounded by Identity

Informal description

If a function $f : \alpha \to \alpha$ satisfies $f(x) \leq x$ for all $x \in \alpha$ (i.e., $f \leq \text{id}$), then the sequence of iterates $f^{[n]}$ is antitone with respect to $n \in \mathbb{N}$. In other words, for any natural numbers $m \leq n$, we have $f^{[n]}(x) \leq f^{[m]}(x)$ for all $x \in \alpha$.

Function.Commute.iterate_le_of_map_le theorem

(h : Commute f g) (hf : Monotone f) (hg : Monotone g) {x} (hx : f x ≤ g x) (n : ℕ) : f^[n] x ≤ g^[n] x

Full source

theorem iterate_le_of_map_le (h : Commute f g) (hf : Monotone f) (hg : Monotone g) {x}
    (hx : f x ≤ g x) (n : ℕ) : f^[n] x ≤ g^[n] x := by
  apply hf.seq_le_seq n
  · rfl
  · intros; rw [iterate_succ_apply']
  · intros; simp [h.iterate_right _ _, hg.iterate _ hx]

Monotone Commuting Functions Preserve Inequality Under Iteration

Informal description

Let $f, g : \alpha \to \alpha$ be monotone functions that commute (i.e., $f \circ g = g \circ f$). For any $x \in \alpha$ and natural number $n$, if $f(x) \leq g(x)$, then the $n$-th iterate of $f$ at $x$ is less than or equal to the $n$-th iterate of $g$ at $x$, i.e., $f^{[n]}(x) \leq g^{[n]}(x)$.

Function.Commute.iterate_pos_lt_of_map_lt theorem

(h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x} (hx : f x < g x) {n} (hn : 0 < n) : f^[n] x < g^[n] x

Full source

theorem iterate_pos_lt_of_map_lt (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x}
    (hx : f x < g x) {n} (hn : 0 < n) : f^[n] x < g^[n] x := by
  apply hf.seq_pos_lt_seq_of_le_of_lt hn
  · rfl
  · intros; rw [iterate_succ_apply']
  · intros; simp [h.iterate_right _ _, hg.iterate _ hx]

Strict inequality for iterates of commuting monotone functions: $f^{[n]}(x) < g^{[n]}(x)$ when $f(x) < g(x)$

Informal description

Let $f, g : \alpha \to \alpha$ be two commuting functions, where $f$ is monotone and $g$ is strictly monotone. If $f(x) < g(x)$ for some $x \in \alpha$, then for any positive integer $n$, the $n$-th iterate of $f$ at $x$ is strictly less than the $n$-th iterate of $g$ at $x$, i.e., $f^{[n]}(x) < g^{[n]}(x)$.

Function.Commute.iterate_pos_lt_of_map_lt' theorem

(h : Commute f g) (hf : StrictMono f) (hg : Monotone g) {x} (hx : f x < g x) {n} (hn : 0 < n) : f^[n] x < g^[n] x

Full source

theorem iterate_pos_lt_of_map_lt' (h : Commute f g) (hf : StrictMono f) (hg : Monotone g) {x}
    (hx : f x < g x) {n} (hn : 0 < n) : f^[n] x < g^[n] x :=
  @iterate_pos_lt_of_map_lt αᵒᵈ _ g f h.symm hg.dual hf.dual x hx n hn

Strict inequality for iterates of commuting functions: $f^{[n]}(x) < g^{[n]}(x)$ when $f$ is strictly monotone and $f(x) < g(x)$

Informal description

Let $f, g : \alpha \to \alpha$ be two commuting functions, where $f$ is strictly monotone and $g$ is monotone. If $f(x) < g(x)$ for some $x \in \alpha$, then for any positive integer $n$, the $n$-th iterate of $f$ at $x$ is strictly less than the $n$-th iterate of $g$ at $x$, i.e., $f^{[n]}(x) < g^{[n]}(x)$.

Function.Commute.iterate_pos_lt_iff_map_lt theorem

(h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n} (hn : 0 < n) : f^[n] x < g^[n] x ↔ f x < g x

Full source

theorem iterate_pos_lt_iff_map_lt (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n}
    (hn : 0 < n) : f^[n]f^[n] x < g^[n] x ↔ f x < g x := by
  rcases lt_trichotomy (f x) (g x) with (H | H | H)
  · simp only [*, iterate_pos_lt_of_map_lt]
  · simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]
  · simp only [lt_asymm H, lt_asymm (h.symm.iterate_pos_lt_of_map_lt' hg hf H hn)]

Strict inequality equivalence for iterates of commuting monotone functions: $f^{[n]}(x) < g^{[n]}(x) \leftrightarrow f(x) < g(x)$

Informal description

Let $f, g : \alpha \to \alpha$ be two commuting functions, where $f$ is monotone and $g$ is strictly monotone. For any $x \in \alpha$ and any positive integer $n$, the following equivalence holds: $$ f^{[n]}(x) < g^{[n]}(x) \quad \text{if and only if} \quad f(x) < g(x). $$

Function.Commute.iterate_pos_lt_iff_map_lt' theorem

(h : Commute f g) (hf : StrictMono f) (hg : Monotone g) {x n} (hn : 0 < n) : f^[n] x < g^[n] x ↔ f x < g x

Full source

theorem iterate_pos_lt_iff_map_lt' (h : Commute f g) (hf : StrictMono f) (hg : Monotone g) {x n}
    (hn : 0 < n) : f^[n]f^[n] x < g^[n] x ↔ f x < g x :=
  @iterate_pos_lt_iff_map_lt αᵒᵈ _ _ _ h.symm hg.dual hf.dual x n hn

Strict inequality equivalence for iterates of commuting functions: $f^n(x) < g^n(x) \leftrightarrow f(x) < g(x)$ when $f$ is strictly monotone

Informal description

Let $f, g : \alpha \to \alpha$ be two commuting functions, where $f$ is strictly monotone and $g$ is monotone. For any $x \in \alpha$ and any positive integer $n$, the following equivalence holds: $$ f^n(x) < g^n(x) \quad \text{if and only if} \quad f(x) < g(x). $$

Function.Commute.iterate_pos_le_iff_map_le theorem

(h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n} (hn : 0 < n) : f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Full source

theorem iterate_pos_le_iff_map_le (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n}
    (hn : 0 < n) : f^[n]f^[n] x ≤ g^[n] x ↔ f x ≤ g x := by
  simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt' hg hf hn)

Inequality equivalence for iterates of commuting functions: $f^n(x) \leq g^n(x) \leftrightarrow f(x) \leq g(x)$ with $f$ monotone and $g$ strictly monotone

Informal description

Let $f, g : \alpha \to \alpha$ be two commuting functions, where $f$ is monotone and $g$ is strictly monotone. For any $x \in \alpha$ and any positive integer $n$, the following equivalence holds: $$ f^n(x) \leq g^n(x) \quad \text{if and only if} \quad f(x) \leq g(x). $$

Function.Commute.iterate_pos_le_iff_map_le' theorem

(h : Commute f g) (hf : StrictMono f) (hg : Monotone g) {x n} (hn : 0 < n) : f^[n] x ≤ g^[n] x ↔ f x ≤ g x

Full source

theorem iterate_pos_le_iff_map_le' (h : Commute f g) (hf : StrictMono f) (hg : Monotone g) {x n}
    (hn : 0 < n) : f^[n]f^[n] x ≤ g^[n] x ↔ f x ≤ g x := by
  simpa only [not_lt] using not_congr (h.symm.iterate_pos_lt_iff_map_lt hg hf hn)

Inequality equivalence for iterates of commuting functions: $f^{[n]}(x) \leq g^{[n]}(x) \leftrightarrow f(x) \leq g(x)$ with $f$ strictly monotone and $g$ monotone

Informal description

Let $f, g : \alpha \to \alpha$ be two commuting functions, where $f$ is strictly monotone and $g$ is monotone. For any $x \in \alpha$ and any positive integer $n$, the following equivalence holds: $$ f^{[n]}(x) \leq g^{[n]}(x) \quad \text{if and only if} \quad f(x) \leq g(x). $$

Function.Commute.iterate_pos_eq_iff_map_eq theorem

(h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n} (hn : 0 < n) : f^[n] x = g^[n] x ↔ f x = g x

Full source

theorem iterate_pos_eq_iff_map_eq (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n}
    (hn : 0 < n) : f^[n]f^[n] x = g^[n] x ↔ f x = g x := by
  simp only [le_antisymm_iff, h.iterate_pos_le_iff_map_le hf hg hn,
    h.symm.iterate_pos_le_iff_map_le' hg hf hn]

Equality equivalence for iterates of commuting functions: $f^{[n]}(x) = g^{[n]}(x) \leftrightarrow f(x) = g(x)$ with $f$ monotone and $g$ strictly monotone

Informal description

Let $f, g : \alpha \to \alpha$ be two commuting functions, where $f$ is monotone and $g$ is strictly monotone. For any $x \in \alpha$ and any positive integer $n$, the following equivalence holds: $$ f^{[n]}(x) = g^{[n]}(x) \quad \text{if and only if} \quad f(x) = g(x). $$

Monotone.monotone_iterate_of_le_map theorem

(hf : Monotone f) (hx : x ≤ f x) : Monotone fun n => f^[n] x

Full source

/-- If `f` is a monotone map and `x ≤ f x` at some point `x`, then the iterates `f^[n] x` form
a monotone sequence. -/
theorem monotone_iterate_of_le_map (hf : Monotone f) (hx : x ≤ f x) : Monotone fun n => f^[n] x :=
  monotone_nat_of_le_succ fun n => by
    rw [iterate_succ_apply]
    exact hf.iterate n hx

Monotonicity of Iterates for Monotone Functions with $x \leq f(x)$

Informal description

Let $f : \alpha \to \alpha$ be a monotone function and let $x \in \alpha$ satisfy $x \leq f(x)$. Then the sequence of iterates $(f^{[n]}(x))_{n \in \mathbb{N}}$ is monotone increasing, i.e., for any natural numbers $n \leq m$, we have $f^{[n]}(x) \leq f^{[m]}(x)$.

Monotone.antitone_iterate_of_map_le theorem

(hf : Monotone f) (hx : f x ≤ x) : Antitone fun n => f^[n] x

Full source

/-- If `f` is a monotone map and `f x ≤ x` at some point `x`, then the iterates `f^[n] x` form
an antitone sequence. -/
theorem antitone_iterate_of_map_le (hf : Monotone f) (hx : f x ≤ x) : Antitone fun n => f^[n] x :=
  hf.dual.monotone_iterate_of_le_map hx

Decreasing Iterates for Monotone Functions with $f(x) \leq x$

Informal description

Let $f : \alpha \to \alpha$ be a monotone function and let $x \in \alpha$ satisfy $f(x) \leq x$. Then the sequence of iterates $(f^{[n]}(x))_{n \in \mathbb{N}}$ is antitone (i.e., decreasing), meaning that for any natural numbers $n \leq m$, we have $f^{[n]}(x) \geq f^{[m]}(x)$.

StrictMono.strictMono_iterate_of_lt_map theorem

(hf : StrictMono f) (hx : x < f x) : StrictMono fun n => f^[n] x

Full source

/-- If `f` is a strictly monotone map and `x < f x` at some point `x`, then the iterates `f^[n] x`
form a strictly monotone sequence. -/
theorem strictMono_iterate_of_lt_map (hf : StrictMono f) (hx : x < f x) :
    StrictMono fun n => f^[n] x :=
  strictMono_nat_of_lt_succ fun n => by
    rw [iterate_succ_apply]
    exact hf.iterate n hx

Strictly Increasing Iterates for Strictly Monotone Functions with $x < f(x)$

Informal description

Let $f : \alpha \to \alpha$ be a strictly monotone function and let $x \in \alpha$ satisfy $x < f(x)$. Then the sequence of iterates $(f^{[n]}(x))_{n \in \mathbb{N}}$ is strictly increasing, i.e., for any natural numbers $n < m$, we have $f^{[n]}(x) < f^{[m]}(x)$.

StrictMono.strictAnti_iterate_of_map_lt theorem

(hf : StrictMono f) (hx : f x < x) : StrictAnti fun n => f^[n] x

Full source

/-- If `f` is a strictly antitone map and `f x < x` at some point `x`, then the iterates `f^[n] x`
form a strictly antitone sequence. -/
theorem strictAnti_iterate_of_map_lt (hf : StrictMono f) (hx : f x < x) :
    StrictAnti fun n => f^[n] x :=
  hf.dual.strictMono_iterate_of_lt_map hx

Strictly Decreasing Iterates for Strictly Increasing Functions with $f(x) < x$

Informal description

Let $f : \alpha \to \alpha$ be a strictly increasing function and let $x \in \alpha$ satisfy $f(x) < x$. Then the sequence of iterates $(f^{[n]}(x))_{n \in \mathbb{N}}$ is strictly decreasing, i.e., for any natural numbers $n < m$, we have $f^{[n]}(x) > f^{[m]}(x)$.