Commit 2024-08-25 14:14 9b07fb6d

View on Github →

feat(Dynamics.TopologicalEntropy): add CoverEntropy (#15753) Second PR in a sequence to implement the notion of topological entropy for maps using Bowen-Dinaburg's formalism. This file defines a notion of topological entropy for transformations of a uniform space, using covers.

Dynamical uniformities
Topological entropy via covers
Topological entropy via nets
Behaviour under morphisms
Behaviour for subsets and unions
Behaviour under products
Full shift Things get more serious. The first file was pretty short; this one is the longest. Paging @pitmonticone @sgouezel

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

added theorem Dynamics.IsDynCoverOf.coverEntropyEnt_le_log_card_div

added theorem Dynamics.IsDynCoverOf.iterate_le_pow

added theorem Dynamics.IsDynCoverOf.nonempty

added theorem Dynamics.IsDynCoverOf.nonempty_inter

added theorem Dynamics.IsDynCoverOf.of_entourage_subset

added theorem Dynamics.IsDynCoverOf.of_le

added def Dynamics.IsDynCoverOf

added theorem Dynamics.coverEntropyEnt_antitone

added theorem Dynamics.coverEntropyEnt_empty

added theorem Dynamics.coverEntropyEnt_finite_of_isCompact_invariant

added theorem Dynamics.coverEntropyEnt_le_coverEntropy

added theorem Dynamics.coverEntropyEnt_le_coverEntropyInfEnt

added theorem Dynamics.coverEntropyEnt_le_log_coverMincard_div

added theorem Dynamics.coverEntropyEnt_nonneg

added theorem Dynamics.coverEntropyEnt_univ

added theorem Dynamics.coverEntropyInfEnt_antitone

added theorem Dynamics.coverEntropyInfEnt_empty

added theorem Dynamics.coverEntropyInfEnt_le_coverEntropyEnt

added theorem Dynamics.coverEntropyInfEnt_le_coverEntropyInf

added theorem Dynamics.coverEntropyInfEnt_nonneg

added theorem Dynamics.coverEntropyInfEnt_univ

added theorem Dynamics.coverEntropyInf_antitone

added theorem Dynamics.coverEntropyInf_empty

added theorem Dynamics.coverEntropyInf_eq_coverEntropy

added theorem Dynamics.coverEntropyInf_eq_iSup_basis

added theorem Dynamics.coverEntropyInf_le_coverEntropy

added theorem Dynamics.coverEntropyInf_nonneg

added theorem Dynamics.coverEntropy_antitone

added theorem Dynamics.coverEntropy_empty

added theorem Dynamics.coverEntropy_eq_iSup_basis

added theorem Dynamics.coverEntropy_nonneg

added theorem Dynamics.coverMincard_antitone

added theorem Dynamics.coverMincard_empty

added theorem Dynamics.coverMincard_eq_zero_iff

added theorem Dynamics.coverMincard_finite_iff

added theorem Dynamics.coverMincard_finite_of_isCompact_invariant

added theorem Dynamics.coverMincard_finite_of_isCompact_uniformContinuous

added theorem Dynamics.coverMincard_le_card

added theorem Dynamics.coverMincard_le_pow

added theorem Dynamics.coverMincard_monotone_time

added theorem Dynamics.coverMincard_mul_le_pow

added theorem Dynamics.coverMincard_univ

added theorem Dynamics.coverMincard_zero

added theorem Dynamics.exists_isDynCoverOf_of_isCompact_invariant

added theorem Dynamics.exists_isDynCoverOf_of_isCompact_uniformContinuous

added theorem Dynamics.isDynCoverOf_empty

added theorem Dynamics.isDynCoverOf_univ

added theorem Dynamics.isDynCoverOf_zero

added theorem Dynamics.log_coverMincard_iterate_le

added theorem Dynamics.log_coverMincard_le_add

added theorem Dynamics.log_coverMincard_nonneg

added theorem Dynamics.nonempty_inter_of_coverMincard

added theorem Dynamics.one_le_coverMincard_iff