Theorems · Definition · dynamical systems

Dynamics.coverEntropyInfEntourage

{X : Type u_1} → (X → X) → Set X → SetRel X X → EReal

The entropy of an entourage U, defined as the exponential rate of growth of the size of the smallest (U, n)-refined cover of F. Takes values in the space of extended real numbers [-∞, +∞]. This second version uses a liminf, and is chosen as an alternative definition.

Defined in

Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Cited by

15 results in Mathlib

Foundations

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