coverEntropyInf_image_le_of_uniformContinuous

English

If φ is uniformly continuous on an invariant set G and F ⊆ G, then the same entropy comparison holds for F in G.

Русский

Если φ равномерно непрерывна на инвариантном множестве G и F ⊆ G, то для F в G выполняется та же оценка энтропии.

LaTeX

$$$\\operatorname{coverEntropy}(T, \\phi(F)) \\le \\operatorname{coverEntropy}(S, F)$$$

Lean4

/-- The entropy of `φ '' F` is lower than entropy of `F` if  `φ` is uniformly continuous. This
  version uses a `liminf`. -/
theorem coverEntropyInf_image_le_of_uniformContinuous [UniformSpace X] [UniformSpace Y] {S : X → X} {T : Y → Y}
    {φ : X → Y} (h : Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) :
    coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F :=
  by
  rw [coverEntropyInf_image_of_comap _ h F]
  exact coverEntropyInf_antitone S F (uniformContinuous_iff.1 h')

Похожие утверждения