Theorems · Definition · dynamical systems

SymbolicDynamics.FullShift.Pattern.shift

{A : Type u_1} →
  [inst : Inhabited A] → {G : Type u_2} → [AddMonoid G] → SymbolicDynamics.FullShift.Pattern A G → G → G → A

Translate a finite pattern p so that it occurs at the translate v, before completing into a configuration. On input h : G, we proceed as follows: * if h lies in the left-translate of the support, i.e. h ∈ p.support.image (v + ·), choose (noncomputably) w ∈ p.support with v + w = h and return p.config w; * otherwise return default. This definition does not assume left-cancellation; it only chooses a preimage. Uniqueness (and the usual equations such as Pattern.shift p v (v + w) = p.config w) require a left-cancellation hypothesis and are proved in separate lemmas.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

4 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

InhabitedAddMonoid