Commit 2026-05-12 08:52 424dce2f

View on Github →

feat(SymbolicDynamics): basic setup of Zd, full shift, cylinders, pat… (#28546) This PR adds a group-generic foundation for symbolic dynamics over an arbitrary group G, together with convenient specializations for ℤ and ℤ^d. Summary of additions:

  • Full shift and shift action
    • abbrev FullShift (A G) := G → A (inherits product topology from the Π-type).
    • Right shift shift g x with convention (shift g x) h = x (h * g).
  • Cylinders and topology
    • cylinder U x : Set (G → A) for finite U : Finset G.
    • Cylinders are open under [DiscreteTopology A]; with a finite alphabet they are also closed.
    • Equality with dependent products:
      cylinder U x = Set.pi (↑U) (fun i => ({x i} : Set A)), enabling use of the Set.pi API.
  • Patterns, occurrences, and subshifts
    • Pattern A G with finite support : Finset G and data : support → A.
    • Pattern.occursIn p x g (occurrence at translate g) and the expected shift law.
    • forbids F and Subshift A G (closed, shift-invariant subsets).
    • FixedSupport A G U with an equivalence to (U → A) to obtain finiteness.
  • Language on finite shapes and counting
    • languageOn X U, languageCardOn X U, and patternCountOn Y U.
  • Entropy along a shape sequence
    • limsupAtTop (as an sInf of eventual upper bounds).
    • entropyAlong X F hF := limsup (log (patternCountOn X (F n) + 1) / |F n|)
      for any nonempty finite shapes F : ℕ → Finset G (the + 1 avoids log 0).
  • Specializations
    • IntShapes: segments [-n,n] on Multiplicative ℤ, with entropy_Z.
    • ZdShapes: boxes [-n,n]^d on ℤ^d (as functions Fin d → ℤ), with entropy_Zd. Mathematical remarks:
  • The API is shape-parametric: entropy is defined along user-provided finite shapes.
  • On amenable groups, using a Følner sequence yields a canonical value (Ornstein–Weiss).
    This PR does not assume amenability; the family of shapes is an explicit input. Motivation: Provide a clean, reusable base for symbolic dynamics on groups in mathlib. Future work:
  • Add a Følner predicate and prove shape-independence / limit existence on amenable groups.
  • Expand the ℤ/ℤ^d toolkit (alternative shapes, mixing, factors).
  • Develop 1D theory and, longer-term, multidimensional SFT results (e.g. along the lines of Hochman–Meyerovitch).

Estimated changes