Theorems · Definition · dynamical systems

SymbolicDynamics.FullShift.shift

{A : Type u_1} → {G : Type u_2} → [AddMonoid G] → G → (G → A) → G → A

The left-translation shift on configurations, in additive notation. We call configuration an element of G → A. Given a configuration x : G → A and an element g : G of the additive monoid, the shifted configuration shift g x is defined by (shift g x) h = x (g + h). Intuitively, this moves the whole configuration "in the direction of g": the value at position h in the shifted configuration is the value that was at position g + h in the original one. For example, if G = ℤ and A = {0, 1}, then shift 1 x is the sequence obtained from x by shifting every symbol one step to the left.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

10 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

AddMonoid