Function.IsPeriodicPt.isFixedPt
theorem Function.IsPeriodicPt.isFixedPt :
∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x → Function.IsFixedPt f^[n] x
The theorem `Function.IsPeriodicPt.isFixedPt` states that for any type `α`, function `f` from `α` to `α`, element `x` of type `α`, and natural number `n`, if `x` is a periodic point of `f` with period `n` (i.e., `f` applied `n` times to `x` returns `x`), then `x` is also a fixed point of `f` applied `n` times (i.e., `f` applied `n` times to `x` still gives `x`). Thus, the periodicity of a point for a function implies its fixed point property when the function is iterated the same number of times as the period.
More concisely: If `x` is a periodic point of period `n` for function `f`: i.e., `f^n(x) = x`, then `x` is a fixed point of `f` raised to the power `n`: i.e., `f^n(x) = x`.
|
AddAction.zsmul_mod_period_vadd
theorem AddAction.zsmul_mod_period_vadd :
∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] (j : ℤ) {g : G} {a : α},
(j % ↑(AddAction.period g a)) • g +ᵥ a = j • g +ᵥ a
This theorem states that for any integer `j`, group `G`, element `g` from `G`, and element `a` from a set `α` acted upon by `G`, if `g` acts on `a` in an additive manner, then adding `g`, scaled by `j` modulo the period of the action of `g` on `a`, to `a` is the same as adding `g`, scaled by `j`, to `a`. In other words, the period of the action of `g` on `a` serves as a modulus for scaling `g` before it is added to `a`.
More concisely: For any integer `j`, group `G` action on a set `α` with element `g` and `a ∈ α`, if `g` acts additively on `a`, then `a + (j * g) % (period g) = a + j * g`, where `%` denotes modulo the period of `g`'s action on `a`.
|
MulAction.pow_smul_eq_iff_period_dvd
theorem MulAction.pow_smul_eq_iff_period_dvd :
∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {n : ℕ} {m : M} {a : α},
m ^ n • a = a ↔ MulAction.period m a ∣ n
The theorem `MulAction.pow_smul_eq_iff_period_dvd` states that for any monoid `M`, any `M`-set `α`, any natural number `n`, any element `m` of `M`, and any element `a` of `α`, the condition that `m` to the power `n` acting on `a` equals `a` is equivalent to the statement that the period of the multiplicative action of `m` on `a` divides `n`. This period is defined as the smallest positive `n` such that `m` to the power `n` acting on `a` equals `a` or `0` if no such `n` exists.
More concisely: For any monoid action on an set, the power of an element acting on another equals the identity if and only if the period of the action of that element on the other element divides the power.
|
Function.isPeriodicPt_iff_minimalPeriod_dvd
theorem Function.isPeriodicPt_iff_minimalPeriod_dvd :
∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x ↔ Function.minimalPeriod f x ∣ n := by
sorry
The theorem `Function.isPeriodicPt_iff_minimalPeriod_dvd` states that for any given point `x` and function `f` of type `α → α`, `x` is a periodic point of `f` with period `n` if and only if the minimal period of `x` under `f` divides `n`. In other words, a point `x` repeats its position every `n` steps in the function `f` exactly when `n` is a multiple of the smallest number of steps that brings `x` back to its initial position.
More concisely: A point x is a periodic point of a function f with period n if and only if the minimal period of x under f divides n.
|
Function.IsPeriodicPt.apply_iterate
theorem Function.IsPeriodicPt.apply_iterate :
∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ},
Function.IsPeriodicPt f n x → ∀ (m : ℕ), Function.IsPeriodicPt f n (f^[m] x)
The theorem `Function.IsPeriodicPt.apply_iterate` states that for any type `α`, function `f` from `α` to `α`, element `x` of `α`, and natural number `n`, if `x` is a periodic point of `f` with period `n`, then for any natural number `m`, the `m`-th iteration of `f` on `x` is also a periodic point of `f` with period `n`. In other words, if applying `f` `n` times to `x` gives back `x`, then applying `f` `n` times to the result of applying `f` `m` times to `x` also gives back the result of applying `f` `m` times to `x`.
More concisely: If `x` is a periodic point of degree `n` for the function `f` in `α`, then for any natural number `m`, `f^(m+n)` applied to `x` equals `f^m` applied to `x`.
|
MulAction.zpow_mod_period_smul
theorem MulAction.zpow_mod_period_smul :
∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] (j : ℤ) {g : G} {a : α},
g ^ (j % ↑(MulAction.period g a)) • a = g ^ j • a
This theorem states that for any integer `j`, any group element `g` and any element `a` upon which `g` acts, the action of `g` raised to the power `j` modulo the period of the action of `g` on `a` on `a` is the same as the action of `g` raised to the power `j` on `a`. In mathematical terms, this can be expressed as `g ^ (j mod period(g, a)) * a = g ^ j * a`, where `^` denotes exponentiation, `mod` denotes the modulus operation, and `*` denotes the action of `g` on `a`. The period of an action is the smallest positive integer `n` such that raising `g` to the power `n` and acting on `a` yields `a` again.
More concisely: For any group element `g`, integer `j`, and group element `a` upon which `g` acts, the power `g^(j mod period(g, a))` of `g` acting on `a` is equivalent to the power `g^j` of `g` multiplied by `a`.
|
Function.is_periodic_id
theorem Function.is_periodic_id : ∀ {α : Type u_1} (n : ℕ) (x : α), Function.IsPeriodicPt id n x
The theorem `Function.is_periodic_id` states that for any given type `α`, any natural number `n`, and any element `x` of type `α`, `x` is a periodic point of the identity function with period `n`. In other words, applying the identity function `n` times to `x` will always return `x` itself, which is in essence, the definition of a periodic point.
More concisely: For any type `α` and natural number `n`, the identity function `id` is periodic with period `n` on any element `x` of type `α`, i.e., `id^n(x) = x`.
|
Function.IsPeriodicPt.minimalPeriod_pos
theorem Function.IsPeriodicPt.minimalPeriod_pos :
∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ},
0 < n → Function.IsPeriodicPt f n x → 0 < Function.minimalPeriod f x
This theorem states that for any type `α`, a function `f` from `α` to `α`, any element `x` of type `α`, and any natural number `n`, if `n` is greater than 0 and `x` is a periodic point of `f` with a period of `n` (i.e., applying function `f` `n` times to `x` gives us `x` again), then the minimal period of `x` under the function `f` is also greater than 0. The minimal period is the smallest positive integer `n` such that `f` applied `n` times to `x` returns `x`, or 0 if no such integer exists.
More concisely: If `x` is a periodic point of period `n` (`n` > 0) for function `f` from type `α` to `α`, then the minimal period of `x` under `f` is also a positive integer.
|
Function.IsPeriodicPt.const_mul
theorem Function.IsPeriodicPt.const_mul :
∀ {α : Type u_1} {f : α → α} {x : α} {m : ℕ},
Function.IsPeriodicPt f m x → ∀ (n : ℕ), Function.IsPeriodicPt f (n * m) x
This theorem states that for any type `α`, any function `f` from `α` to `α`, any point `x` of type `α`, and any natural number `m`, if `x` is a periodic point of `f` with period `m`, then for any natural number `n`, `x` is also a periodic point of `f` with period `n * m`. In mathematical terms, if `f^[m](x) = x`, then `f^[n*m](x) = x` for all natural numbers `n`.
More concisely: If `x` is a periodic point of function `f` with period `m` in type `α`, then `x` is also a periodic point of `f` with period `n * m` for any natural number `n`.
|
Function.IsPeriodicPt.eq_of_apply_eq
theorem Function.IsPeriodicPt.eq_of_apply_eq :
∀ {α : Type u_1} {f : α → α} {x y : α} {m n : ℕ},
Function.IsPeriodicPt f m x → Function.IsPeriodicPt f n y → 0 < m → 0 < n → f x = f y → x = y
The theorem `Function.IsPeriodicPt.eq_of_apply_eq` states that for any type `α`, any function `f : α → α`, any two points `x` and `y` of type `α`, and any two positive integers `m` and `n`, if `x` is a periodic point of `f` with period `m`, and `y` is a periodic point of `f` with period `n`, and `f` maps both `x` and `y` to the same point, then `x` must be equal to `y`. In other words, if two points are periodic under a function and are mapped to the same point by the function, then they must be the same point, given that their periodicity is non-zero.
More concisely: If two points have the same periodicity and are mapped to the same image under a function, then they are equal.
|
Function.isPeriodicPt_minimalPeriod
theorem Function.isPeriodicPt_minimalPeriod :
∀ {α : Type u_1} (f : α → α) (x : α), Function.IsPeriodicPt f (Function.minimalPeriod f x) x
This theorem states that for any function `f` mapping a type `α` to `α` and any element `x` of type `α`, `x` is a periodic point of `f` with a period equal to its minimal period. A periodic point of a function is a point `x` such that applying the function a certain number of times (the period) returns `x`. The minimal period of `x` under `f` is the smallest positive number of applications of `f` needed to return to `x`, or zero if `x` is not a periodic point.
More concisely: For any function `f: α -> α` and element `x: α`, if `x` is a periodic point of `f` with minimal period `n`, then applying `f` exactly `n` times to `x` returns `x`.
|
Function.IsPeriodicPt.minimalPeriod_dvd
theorem Function.IsPeriodicPt.minimalPeriod_dvd :
∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, Function.IsPeriodicPt f n x → Function.minimalPeriod f x ∣ n := by
sorry
The theorem `Function.IsPeriodicPt.minimalPeriod_dvd` states that for any type `α`, function `f` of type `α → α`, point `x` of type `α`, and natural number `n`, if `x` is a periodic point of `f` with period `n`, then the minimal period of `x` under `f` divides `n`. In other words, if the function `f`, when applied `n` times to `x`, brings us back to `x`, then `n` is a multiple of the smallest such number of applications of `f` to `x` that bring us back to `x`.
More concisely: If `x` is a periodic point of period `n` for function `f: α → α`, then the minimal period of `x` under `f` divides `n`.
|
Function.isPeriodicPt_zero
theorem Function.isPeriodicPt_zero : ∀ {α : Type u_1} (f : α → α) (x : α), Function.IsPeriodicPt f 0 x
The theorem `Function.isPeriodicPt_zero` states that for any function `f` mapping a type `α` to itself and for any point `x` of type `α`, `x` is a periodic point of `f` with period `0`. In other words, applying the function `f` zero times to `x` results in `x` itself. This is a fundamental property derived from the definition of function iteration and periodicity.
More concisely: For any function from a type to itself, the identity element is a periodic point with period 0.
|
AddAction.isPeriodicPt_vadd_iff
theorem AddAction.isPeriodicPt_vadd_iff :
∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α} {n : ℕ},
Function.IsPeriodicPt (fun x => m +ᵥ x) n a ↔ n • m +ᵥ a = a
This theorem states that for any type `α`, any add monoid `M`, any additive action of `M` on `α`, any element `m` of `M`, any element `a` of `α`, and any natural number `n`, a point `a` is a periodic point of the function `x => m +ᵥ x` with period `n` if and only if the scalar multiplication `n • m +ᵥ a` equals `a`. In other words, the point `a` returns to its original position after `n` applications of the function `x => m +ᵥ x` exactly when adding `m` scaled by `n` to `a` gives `a` back.
More concisely: For any add monoid `M`, additive action on type `α`, element `m` in `M`, element `a` in `α`, and natural number `n`, the element `a` is a periodic point of the function `x => m + α x` with period `n` if and only if `n * m + α a = a`.
|
Function.iterate_injOn_Iio_minimalPeriod
theorem Function.iterate_injOn_Iio_minimalPeriod :
∀ {α : Type u_1} {f : α → α} {x : α}, Set.InjOn (fun x_1 => f^[x_1] x) (Set.Iio (Function.minimalPeriod f x)) := by
sorry
This theorem states that for any type 'α', a function 'f' from 'α' to 'α', and an element 'x' of type 'α', the function defined by the nth iteration of 'f' applied to 'x' is injective on the left-infinite right-open interval up to the minimal period of 'x' under the endomorphism 'f'. In other words, for each pair of natural numbers less than the minimal period of 'x', if the nth iteration of 'f' applied to 'x' equals the mth iteration of 'f' applied to 'x', then n must equal m.
More concisely: For any endomorphism (function) 'f' on type 'α' and element 'x' of type 'α' with minimal period 'p', if the nth and mth applications of 'f' to 'x' are equal for some natural numbers 'n' and 'm' less than 'p', then 'n' equals 'm'.
|
Function.iterate_minimalPeriod
theorem Function.iterate_minimalPeriod : ∀ {α : Type u_1} {f : α → α} {x : α}, f^[Function.minimalPeriod f x] x = x
This theorem states that for any given type `α`, a function `f` from `α` to `α`, and an element `x` of `α`, by iteratively applying the function `f` to `x` for a number of times equal to the minimal period of `x` under `f`, we reach `x` again. That is, `x` is a periodic point under `f` with period equal to its minimal period.
More concisely: For any function `f` and element `x` in a type `α`, if `x` has minimal period `n` under `f`, then applying `f` to `x` `n` times returns `x`.
|
AddAction.nsmul_vadd_eq_iff_period_dvd
theorem AddAction.nsmul_vadd_eq_iff_period_dvd :
∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {n : ℕ} {m : M} {a : α},
n • m +ᵥ a = a ↔ AddAction.period m a ∣ n
This theorem states that for any additive action of an element `m` (from an additive monoid `M`) on an element `a` (from a type `α`), the additive action repeated `n` times brings `a` back to itself if and only if the period of the additive action (i.e., the smallest positive number of times the action needs to be repeated to bring `a` back to itself) divides `n`. In the context of this theorem, `n • m +ᵥ a = a` denotes the additive action of `m` on `a` repeated `n` times, and `AddAction.period m a ∣ n` denotes that the period of the action divides `n`.
More concisely: For any additive action of an element `m` on `α`, the repeated action `n • m +ᵥ a = a` holds if and only if the period of the action `AddAction.period m a` divides `n`.
|
Function.minimalPeriod_pos_of_mem_periodicPts
theorem Function.minimalPeriod_pos_of_mem_periodicPts :
∀ {α : Type u_1} {f : α → α} {x : α}, x ∈ Function.periodicPts f → 0 < Function.minimalPeriod f x
This theorem states that for any type `α`, given a function `f` mapping from `α` to `α` and an element `x` of `α`, if `x` is a periodic point of the function `f` (i.e., `x` is in the set of periodic points of `f`), then the minimal period of `x` under the function `f` is a positive integer. In other words, if `x` repeats its position after certain iterations under `f`, the number of steps it takes for the first such repetition is a positive number.
More concisely: For any function `f` from type `α` to itself and any periodic point `x` of `f`, the minimal period of `x` is a positive integer.
|
Function.periodicOrbit_def
theorem Function.periodicOrbit_def :
∀ {α : Type u_1} (f : α → α) (x : α),
Function.periodicOrbit f x = ↑(List.map (fun n => f^[n] x) (List.range (Function.minimalPeriod f x)))
The theorem `Function.periodicOrbit_def` states that for any type `α` and function `f` mapping `α` to `α`, and for any element `x` of type `α`, the periodic orbit of `x` under `f` is defined as the sequence obtained by applying the function `f` to `x` a number of times corresponding to the values in the range from `0` to the minimal period of `x` under `f` (exclusive). This sequence is then converted to a cycle. This encapsulates the idea of a periodic orbit as a cycle of repeated function applications starting from `x`, with the length of the cycle determined by the minimal period of `x` under `f`. If `x` is not a periodic point, the minimal period would be `0` and hence the cycle would be empty.
More concisely: The theorem `Function.periodicOrbit_def` defines the periodic orbit of an element `x` under a function `f` as the cycle obtained by applying `f` to `x` for up to the minimal period of `x` under `f`. If `x` is not periodic, the orbit is empty.
|
Function.Commute.minimalPeriod_of_comp_dvd_lcm
theorem Function.Commute.minimalPeriod_of_comp_dvd_lcm :
∀ {α : Type u_1} {f : α → α} {x : α} {g : α → α},
Function.Commute f g →
Function.minimalPeriod (f ∘ g) x ∣ (Function.minimalPeriod f x).lcm (Function.minimalPeriod g x)
The theorem `Function.Commute.minimalPeriod_of_comp_dvd_lcm` states that for any two functions `f` and `g` that commute and a point `x`, the minimal period of the composition of `f` and `g` at `x` divides the least common multiple of the minimal periods of `f` and `g` at `x`. In other words, if `f` and `g` are two endomorphisms on a set `α` that commute (meaning that their composition is the same regardless of the order in which they are applied), and `x` is a point in `α`, then the smallest number of times the composition `f ∘ g` needs to be applied on `x` to return to `x` is a divisor of the least common multiple of the smallest number of times `f` and `g` need to be applied on `x` to return to `x`.
More concisely: For commuting endomorphisms f and g on a set α, and any point x in α, the minimal period of their composition at x divides their least common multiple at x.
|
Function.periodicOrbit_eq_cycle_map
theorem Function.periodicOrbit_eq_cycle_map :
∀ {α : Type u_1} (f : α → α) (x : α),
Function.periodicOrbit f x = Cycle.map (fun n => f^[n] x) ↑(List.range (Function.minimalPeriod f x))
This theorem states that for any function `f` of type `α → α` and any element `x` of type `α`, the periodic orbit of `x` under the function `f` is equivalent to the result of mapping the function `(fun n => f^[n] x)` over the list of numbers from `0` to the minimal period of `x` under `f`, and then lifting this list to a cycle. In other words, the periodic orbit of `x` under `f` is the cycle formed by taking the list of natural numbers up to the minimal period of `x`, applying `f` to `x` that many times for each number, and then considering this list as a cycle.
More concisely: The periodic orbit of an element `x` under a function `f` is equivalent to the cycle obtained by applying `f` to `x` repeatedly up to the minimal period of `x`, and then viewing the resulting sequence as a cycle.
|
MulAction.period_eq_minimalPeriod
theorem MulAction.period_eq_minimalPeriod :
∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α},
MulAction.period m a = Function.minimalPeriod (fun x => m • x) a
The theorem `MulAction.period_eq_minimalPeriod` states that for any type `α`, any type `M` with a monoid structure, any action of `M` on `α`, and any elements `m` of type `M` and `a` of type `α`, the period of the multiplicative action of `m` on `a` is exactly the same as the minimal period of `a` under the endomorphism defined by the action of `m`. In other words, the period of the action of `m` on `a` is the smallest number of times you need to apply the action of `m` to `a` to get back to `a` itself, and this number is the same as the minimal period of `a` under the action of `m`.
More concisely: For any monoid action on type `α`, the period of an element `a` under the multiplicative action of an element `m` equals the minimal period of `a` under the endomorphism defined by `m`.
|
Function.IsFixedPt.isPeriodicPt
theorem Function.IsFixedPt.isPeriodicPt :
∀ {α : Type u_1} {f : α → α} {x : α}, Function.IsFixedPt f x → ∀ (n : ℕ), Function.IsPeriodicPt f n x
This theorem states that if a point `x` is a fixed point of a function `f` (meaning `f(x) = x`), then `x` is also a periodic point of `f` for any given natural number `n`. Here, a periodic point refers to a point such that, when the function is applied `n` times iteratively, it returns to its original value. In other words, if `x` is a fixed point of `f`, then `f` applied `n` times to `x` (`f^[n] x`) will always equal `x`, for any `n`.
More concisely: If `x` is a fixed point of the function `f`, then `x` is also a periodic point of `f` for any natural number `n` (i.e., `f^[n] x = x`).
|
AddAction.nsmul_mod_period_vadd
theorem AddAction.nsmul_mod_period_vadd :
∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] (n : ℕ) {m : M} {a : α},
(n % AddAction.period m a) • m +ᵥ a = n • m +ᵥ a
The theorem `AddAction.nsmul_mod_period_vadd` states that for any natural number `n`, and for any elements `m` of type `M` and `a` of type `α` where `M` is an additive monoid and `α` is acted upon by `M`, the result of adding `m` to `a` scaled by `(n modulo the period of the action of m on a)` will be the same as the result of adding `m` to `a` scaled by `n`. In other words, in the context of an additive action, n times the action of an element follows a periodic pattern with its period defined by the `AddAction.period`.
More concisely: For any natural number `n` and elements `m` of an additive monoid `M` acting on type `α`, the scaled action `m * n` is equivalent to `m * (n modulo the period of the action of m)` in `α`.
|
MulAction.pow_mod_period_smul
theorem MulAction.pow_mod_period_smul :
∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] (n : ℕ) {m : M} {a : α},
m ^ (n % MulAction.period m a) • a = m ^ n • a
This theorem, `MulAction.pow_mod_period_smul`, states that for any natural number `n`, any element `m` of a monoid `M`, and any element `a` of a type `α` where `M` acts on `α` multiplicatively, the action of `m` raised to the power of (`n` modulo the period of the action of `m` on `a`) on `a` is the same as the action of `m` raised to the power of `n` on `a`. In other words, the multiplicative action of `m` on `a` repeats every `MulAction.period m a` steps.
More concisely: For any monoid action `m` on type `α`, and any element `a` and natural number `n`, the multiplicative action `m^n` on `a` equals `m^(n mod (period m a))` if `n` is a multiple of the period of the action.
|
Function.minimalPeriod_prod_map
theorem Function.minimalPeriod_prod_map :
∀ {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (x : α × β),
Function.minimalPeriod (Prod.map f g) x = (Function.minimalPeriod f x.1).lcm (Function.minimalPeriod g x.2)
The theorem `Function.minimalPeriod_prod_map` states that for any two types `α` and `β`, an endomorphism `f` on `α`, an endomorphism `g` on `β`, and a point `x` which is a pair from `α` and `β`, the minimal period of the point `x` under the combined map `Prod.map f g` (which applies `f` to the first component of `x` and `g` to the second component) equals the least common multiple of the minimal period of the first component of `x` under `f` and the minimal period of the second component of `x` under `g`. In other words, the recurrence period of `x` under the composite action is the least common multiple of the individual recurrence periods under the actions of `f` and `g`.
More concisely: The minimal period of a point under the product map of two endomorphisms is the least common multiple of their minimal periods applied to the respective components.
|
AddAction.period_eq_minimalPeriod
theorem AddAction.period_eq_minimalPeriod :
∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α},
AddAction.period m a = Function.minimalPeriod (fun x => m +ᵥ x) a
The theorem `AddAction.period_eq_minimalPeriod` states that for any type `α`, any type `M` that forms an additive monoid, any additive action of `M` on `α`, and any elements `m` of type `M` and `a` of type `α`, the period of the additive action of `m` on `a` is exactly the same as the minimal period of `a` under the endomorphism defined by adding `m` to every element of `α`. The period of an additive action of `m` on `a` is the smallest positive natural number `n` for which `n*m + a = a`, or `0` if no such `n` exists, while the minimal period of `a` under an endomorphism is the smallest number of applications of the endomorphism required to return `a` to its original value, or `0` if `a` is not a periodic point of the endomorphism.
More concisely: The period of an additive action of an element on a type equals the minimal period of the type under the corresponding endomorphism.
|
Function.minimalPeriod_eq_one_iff_isFixedPt
theorem Function.minimalPeriod_eq_one_iff_isFixedPt :
∀ {α : Type u_1} {f : α → α} {x : α}, Function.minimalPeriod f x = 1 ↔ Function.IsFixedPt f x
This theorem states that for any function `f` mapping a type `α` to itself and any element `x` of type `α`, the minimal period of `x` under `f` is 1 if and only if `x` is a fixed point of `f`. In other words, `x` repeats its value every single step under the function `f` if and only if applying `f` to `x` results in `x` itself.
More concisely: The element `x` of type `α` has minimal period 1 under the function `f:` `α -> α` if and only if `f(x) = x`.
|
Function.IsPeriodicPt.eq_of_apply_eq_same
theorem Function.IsPeriodicPt.eq_of_apply_eq_same :
∀ {α : Type u_1} {f : α → α} {x y : α} {n : ℕ},
Function.IsPeriodicPt f n x → Function.IsPeriodicPt f n y → 0 < n → f x = f y → x = y
The theorem, `Function.IsPeriodicPt.eq_of_apply_eq_same`, states that for any function `f` mapping from a type `α` to `α`, two periodic points `x` and `y` of the same positive period `n`, if `f` sends both `x` and `y` to the same point, then `x` and `y` must be equal. Note that a periodic point `x` of period `n` for the function `f` is defined as a point such that applying `f` `n` times to `x` results again in `x`. A similar theorem exists for the case of points with different periods.
More concisely: If functions `f:` α -> α maps two periodic points `x` and `y` of the same positive period `n` to the same image, then `x` and `y` are equal.
|
Function.IsPeriodicPt.mul_const
theorem Function.IsPeriodicPt.mul_const :
∀ {α : Type u_1} {f : α → α} {x : α} {m : ℕ},
Function.IsPeriodicPt f m x → ∀ (n : ℕ), Function.IsPeriodicPt f (m * n) x
The theorem `Function.IsPeriodicPt.mul_const` states that if a point `x` in the domain of a function `f` is a periodic point of `f` with period `m`, then `x` is also a periodic point of `f` with any period that is a multiple of `m`. In mathematical terms, if the `n`-th iterate of a function `f` satisfies `f^[m](x) = x`, then for any natural number `n`, `f^[m*n](x) = x`.
More concisely: If a function `f` has a periodic point `x` with period `m`, then `x` is also a periodic point of `f` with any period that is a multiple of `m`. In other words, if `f^[m](x) = x`, then `f^[n](x) = x` for all natural numbers `n` such that `m` divides `n`.
|
MulAction.isPeriodicPt_smul_iff
theorem MulAction.isPeriodicPt_smul_iff :
∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α} {n : ℕ},
Function.IsPeriodicPt (fun x => m • x) n a ↔ m ^ n • a = a
This theorem states that for any types `α` and `M`, where `M` has a monoid structure and `α` has an action of `M`, for any element `m` of `M`, an element `a` of `α`, and a natural number `n`, a point `a` is a periodic point of the function `(λx, m • x)` with period `n` if and only if the `n`-th power of `m` acting on `a` results in `a`. In other words, if the `n`-th iteration of the action of `m` on `a` gives `a` back, then `a` is a periodic point of the action of `m` with period `n`, and vice versa.
More concisely: For any monoid `M` and type `α` with an `M`-action, an element `a` of `α` is periodic under the action of `m` with period `n` if and only if `(m ^ n) . a = a`.
|
Function.IsPeriodicPt.minimalPeriod_le
theorem Function.IsPeriodicPt.minimalPeriod_le :
∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ},
0 < n → Function.IsPeriodicPt f n x → Function.minimalPeriod f x ≤ n
The theorem `Function.IsPeriodicPt.minimalPeriod_le` states that for any type `α`, function `f` from `α` to `α`, point `x` of type `α`, and natural number `n`, if `n` is greater than 0 and `x` is a periodic point of `f` with period `n`, then the minimal period of `x` under `f` is less than or equal to `n`. This essentially means that the smallest number of iterations of `f` needed to return to `x` can't be more than the defined period `n` of `x` under `f`, assuming `n` is not zero.
More concisely: For any function f from type α to α, point x of type α, and natural number n greater than 0, if x is a periodic point of f with period n, then the minimal period of x under f is less than or equal to n.
|
Function.minimalPeriod_pos_iff_mem_periodicPts
theorem Function.minimalPeriod_pos_iff_mem_periodicPts :
∀ {α : Type u_1} {f : α → α} {x : α}, 0 < Function.minimalPeriod f x ↔ x ∈ Function.periodicPts f
This theorem states that for any domain type `α`, endomorphism `f` and point `x`, the minimal period of `x` under `f` is positive if and only if `x` is a periodic point of `f`. In other words, a point `x` in the domain of a function `f` has a nonzero minimal period under `f` if and only if there exists some positive natural number `n` such that `f` applied `n` times to `x` returns `x` (i.e., `x` is in the set of periodic points of `f`).
More concisely: For any endomorphism `f` over a domain `α` and point `x`, the minimal period of `x` under `f` is positive if and only if `x` is a periodic point of `f` with some positive period.
|