le_coverEntropyInfEntourage_image

English

Under semiconjugacy, the infimum-entourage of S on F, transported along φ, with the relation V, is bounded above by the infimum-entourage of T on φ(F) with V, for any V.

Русский

При семиконъюгатности инфимум-entourage S на F, перенесённой через φ, по отношению V, не превосходит инфимум-entourage T на φ(F) с V.

LaTeX

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

Lean4

theorem le_coverEntropyInfEntourage_image (h : Semiconj φ S T) (F : Set X) {V : Set (Y × Y)}
    (V_symm : IsSymmetricRel V) :
    coverEntropyInfEntourage S F ((map φ φ) ⁻¹' (V ○ V)) ≤ coverEntropyInfEntourage T (φ '' F) V :=
  expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (le_coverMincard_image h F V_symm n)

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