Theorems · Definition · dynamical systems
Dynamics.coverEntropy
{X : Type u_1} → [UniformSpace X] → (X → X) → Set X → ERealThe entropy of T restricted to F, obtained by taking the supremum
of coverEntropyEntourage over entourages. Note that this supremum is approached by taking small
entourages. This first version uses a limsup, and is chosen as the default definition
for topological entropy.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- iSupproof · cited by 2,415
- UniformSpacestatement and proof · cited by 2,040
- ERealstatement · cited by 793
- uniformityproof · cited by 765
- Dynamics.coverEntropyEntourageproof · cited by 20
Cited by23
Results whose statement or proof uses this declaration.
- Dynamics.coverEntropy_monotonestatement · cited by 3
- Dynamics.coverEntropyInf_le_coverEntropystatement · cited by 2
- Dynamics.coverEntropySupBotHomproof · cited by 2
- Dynamics.coverEntropy_eq_iSup_netEntropyEntouragestatement · cited by 2
- Dynamics.coverEntropy_image_of_comapstatement · cited by 2
- Dynamics.coverEntropy_restrict_subsetstatement and proof · cited by 2
- Dynamics.coverEntropy_antitonestatement · cited by 1
- Dynamics.coverEntropy_emptystatement · cited by 1
- Dynamics.coverEntropy_image_le_of_uniformContinuousstatement and proof · cited by 1
- Dynamics.coverEntropy_unionstatement · cited by 1
- Dynamics.coverEntropyEntourage_le_coverEntropystatement · cited by 1
- Dynamics.coverEntropyInf_eq_coverEntropystatement · cited by 0