English
If φ semiconjugates S to T, then the entropy-entourage of S on F, transported via φ, with the symmetric entourage V, is bounded above by the entropy-entourage of T on φ(F) with V, provided V is symmetric.
Русский
Если φ является семиконъюгатом S к T, то энтропийное окружение S на F, перенесённое через φ, с симметричным окружением V, не превышает энтропийное окружение T на φ(F) с V.
LaTeX
$$$\\operatorname{coverEntropyEntourage}(S, F, (\\phi \\times \\phi)^{-1}(V \\circ V)) \\le \\operatorname{coverEntropyEntourage}(T, \\phi(F), V)$$$
Lean4
theorem le_coverEntropyEntourage_image (h : Semiconj φ S T) (F : Set X) {V : Set (Y × Y)} (V_symm : IsSymmetricRel V) :
coverEntropyEntourage S F ((map φ φ) ⁻¹' (V ○ V)) ≤ coverEntropyEntourage T (φ '' F) V :=
expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (le_coverMincard_image h F V_symm n)
