coverEntropyEntourage_image_le — Mathlib

English

In the same setting, the entropy-entourage of T on φ(F) with V is bounded above by the entropy-entourage of S on F with the preimage of V under φ × φ.

Русский

В той же конфигурации энтропийное окружение T на φ(F) по V не превосходит энтропийное окружение S на F по предобразу V через φ × φ.

LaTeX

$$$\\operatorname{coverEntropyEntourage}(T, \\phi(F), V) \\le \\operatorname{coverEntropyEntourage}(S, F, (\\phi \\times \\phi)^{-1}(V))$$$

Lean4

theorem coverEntropyEntourage_image_le (h : Semiconj φ S T) (F : Set X) (V : Set (Y × Y)) :
    coverEntropyEntourage T (φ '' F) V ≤ coverEntropyEntourage S F ((map φ φ) ⁻¹' V) :=
  expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_image_le h F V n)

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