Monotone.iterate_le_of_le
theorem Monotone.iterate_le_of_le :
∀ {α : Type u_1} [inst : Preorder α] {f g : α → α}, Monotone f → f ≤ g → ∀ (n : ℕ), f^[n] ≤ g^[n]
The theorem `Monotone.iterate_le_of_le` states that for any type `α` with a preorder, if we have two functions `f` and `g` from `α` to `α` such that `f` is monotone and `f` is less than or equal to `g`, then for any natural number `n`, the `n`-th iterate of `f` is less than or equal to the `n`-th iterate of `g`. In mathematical notation, if `f ≤ g` and `f` is monotone, then `f^[n] ≤ g^[n]` for all natural numbers `n`.
More concisely: If `f` is a monotone function less than or equal to `g` between preordered type `α`, then for all natural numbers `n`, `f^(n) ≤ g^(n)`.
|
Monotone.monotone_iterate_of_le_map
theorem Monotone.monotone_iterate_of_le_map :
∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x : α}, Monotone f → x ≤ f x → Monotone fun n => f^[n] x := by
sorry
This theorem states that if `f` is a monotone function over a set with a pre-order structure and there exists a point `x` such that `x ≤ f x`, then the sequence formed by repeatedly applying `f` to `x` (`f^[n] x`) is also monotone. In other words, for a monotone function, whenever `x` is less than or equal to its image under `f`, the sequence obtained by iterating `f` on `x` preserves the order.
More concisely: If `f` is a monotone function on a pre-ordered set and `x` is an element such that `x ≤ f x`, then the sequence `(f^[n] x)` is monotone.
|
Function.Commute.iterate_pos_lt_iff_map_lt
theorem Function.Commute.iterate_pos_lt_iff_map_lt :
∀ {α : Type u_1} [inst : LinearOrder α] {f g : α → α},
Function.Commute f g → Monotone f → StrictMono g → ∀ {x : α} {n : ℕ}, 0 < n → (f^[n] x < g^[n] x ↔ f x < g x)
The theorem `Function.Commute.iterate_pos_lt_iff_map_lt` states that for any type `α` with a linear order, and any two functions `f` and `g` from `α` to `α` that commute, if `f` is monotone and `g` is strictly monotone, then for any element `x` in `α` and any positive natural number `n`, the `n`th iteration of `f` on `x` is less than the `n`th iteration of `g` on `x` if and only if `f(x)` is less than `g(x)`.
More concisely: For any type `α` with a linear order, and functions `f` and `g` from `α` to `α` that commute, if `f` is monotone and `g` is strictly monotone, then `x < y` implies `(iterate f x n) < (iterate g x n)` if and only if `f x < g x`, where `n` is a positive natural number.
|
Monotone.le_iterate_of_le
theorem Monotone.le_iterate_of_le :
∀ {α : Type u_1} [inst : Preorder α] {f g : α → α}, Monotone g → f ≤ g → ∀ (n : ℕ), f^[n] ≤ g^[n]
This theorem states that given a type `α` with a preorder structure, and two functions `f` and `g` from `α` to `α`, if the function `g` is monotone and `f` is less than or equal to `g`, then for any natural number `n`, the `n`-th iterate of `f` (applying `f` `n` times) is less than or equal to the `n`-th iterate of `g`. In other words, the inequality between `f` and `g` persists through any number of iterations.
More concisely: Given a preorder `α` and monotone functions `f` and `g` with `f ≤ g`, the `n`-th iteration of `f` is less than or equal to the `n`-th iteration of `g` for all natural numbers `n`.
|
Monotone.antitone_iterate_of_map_le
theorem Monotone.antitone_iterate_of_map_le :
∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x : α}, Monotone f → f x ≤ x → Antitone fun n => f^[n] x := by
sorry
The theorem `Monotone.antitone_iterate_of_map_le` states that if we have a function `f` which is increasing (or monotone), and at some point `x` the value of `f` is less than or equal to `x`, then the sequence obtained by repeatedly applying `f` to `x` (denoted `f^[n] x`) will be a decreasing (or antitone) sequence. Here, `f^[n] x` represents the `n`-th iterate of `f` at `x`, i.e., applying `f` to `x` `n` times.
More concisely: If `f` is a monotone function such that `f(x) <= x`, then `f^[n] (x)` is an antitone sequence for all `n >= 0`.
|
Monotone.seq_pos_lt_seq_of_lt_of_le
theorem Monotone.seq_pos_lt_seq_of_lt_of_le :
∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
Monotone f →
∀ {n : ℕ}, 0 < n → x 0 ≤ y 0 → (∀ k < n, x (k + 1) < f (x k)) → (∀ k < n, f (y k) ≤ y (k + 1)) → x n < y n
The theorem `Monotone.seq_pos_lt_seq_of_lt_of_le` states that, for any type `α` which has a preorder, a function `f` from `α` to `α`, and two sequences `x` and `y` of elements of `α` indexed by natural numbers, if `f` is monotone, then under certain conditions, `x n` is less than `y n` for any given natural number `n` greater than `0`. The conditions are: `x 0` is less than or equal to `y 0`; for each `k` less than `n`, `x` at `k+1` is less than `f` applied to `x` at `k`; and for each `k` less than `n`, `f` applied to `y` at `k` is less than or equal to `y` at `k+1`.
More concisely: If `α` is a type with a preorder, `f` is a monotone function from `α` to `α`, and `x` and `y` are sequences in `α` such that `x 0 ≤ y 0` and for all `k < n`, `x k < f(x k)` and `f(y k) ≤ y k+1`, then `x n < y n` for any `n > 0`.
|
Monotone.seq_le_seq
theorem Monotone.seq_le_seq :
∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
Monotone f → ∀ (n : ℕ), x 0 ≤ y 0 → (∀ k < n, x (k + 1) ≤ f (x k)) → (∀ k < n, f (y k) ≤ y (k + 1)) → x n ≤ y n
The theorem `Monotone.seq_le_seq` states that for all types `α` equipped with a preorder, for any function `f` from `α` to `α`, and for any sequences `x` and `y` of elements in `α` indexed by natural numbers, if `f` is monotone, the first element of `x` is less than or equal to the first element of `y`, for all indices `k` less than any given natural number `n` the `(k+1)`-th element of `x` is less than or equal to `f` applied to the `k`-th element of `x`, and for all indices `k` less than `n`, `f` applied to the `k`-th element of `y` is less than or equal to the `(k+1)`-th element of `y`, then the `n`-th element of `x` is less than or equal to the `n`-th element of `y`.
In simpler terms, this theorem says that if `f` is a monotone function and sequences `x` and `y` are such that each element of `x` is stretched by `f` in a way that's not more than the corresponding stretching of `y` by `f` (starting from the same or lower initial value), then every element of `x` is less than or equal to the corresponding element of `y`.
More concisely: If `f` is a monotone function and `x` and `y` are sequences such that `x[0] <= y[0]` and `f(x[i-1]) <= y[i]` for all `i < n`, then `x[n] <= y[n]`.
|
Function.id_le_iterate_of_id_le
theorem Function.id_le_iterate_of_id_le :
∀ {α : Type u_1} [inst : Preorder α] {f : α → α}, id ≤ f → ∀ (n : ℕ), id ≤ f^[n]
This theorem states that if a function `f` applied to any `x` is always greater than or equal to `x` itself (expressed as `id ≤ f`), then this property holds true for any number of iterations of `f` on `x`. In other words, if `f(x) ≥ x` for all `x`, then `f(f(f ...(n times)... f(x))) ≥ x` for any natural number `n`. Here, `α` is a type with a preorder, meaning that it has a binary relation that is reflexive and transitive.
More concisely: If `f : α -> α` satisfies `id ≤ f` (where `id` is the identity function on type `α`), then for any natural number `n`, `f^n(x) geq x` holds for all `x` in `α`. (Here, `f^n` denotes the `n`-th composition of `f` with itself.)
|
StrictMono.strictMono_iterate_of_lt_map
theorem StrictMono.strictMono_iterate_of_lt_map :
∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x : α}, StrictMono f → x < f x → StrictMono fun n => f^[n] x := by
sorry
This theorem states that if `f` is a strictly monotone function and `x` is some point such that `x < f(x)`, then the iterates `f^[n] x`, which represent the sequence obtained by applying the function `f` `n` times to `x`, form a strictly monotone sequence. In other words, for any two integers `i` and `j` with `i < j`, it holds that `f^[i] x < f^[j] x`.
More concisely: If `f` is a strictly monotone function and `x` is such that `x < f(x)`, then the sequence `{f^[n] x}` is strictly increasing.
|
StrictMono.strictAnti_iterate_of_map_lt
theorem StrictMono.strictAnti_iterate_of_map_lt :
∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x : α}, StrictMono f → f x < x → StrictAnti fun n => f^[n] x := by
sorry
The theorem `StrictMono.strictAnti_iterate_of_map_lt` states that if `f` is a strictly monotone function and `f(x) < x` for some point `x`, then applying the function `f` repeatedly (`f^[n] x`) produces a strictly antitone sequence. In other words, for any natural numbers `n` and `m` such that `n < m`, `f` applied `m` times to `x` is less than `f` applied `n` times to `x`. Here, strictly monotone means that, for any `a` and `b`, if `a < b`, then `f(a) < f(b)`, and strictly antitone means that, for any `a` and `b`, if `a < b`, then `f` applied `b` times to `x` is less than `f` applied `a` times to `x`.
More concisely: If `f` is a strictly monotone function with `f(x) < x` for some `x`, then for all natural numbers `n` and `m` with `n < m`, `f^[m] x < f^[n] x`.
|