English
Under a semiconjugacy h between S and T, the cover entropy of T over φ(F) is bounded by that of S over F, provided φ is uniformly continuous on the relevant set.
Русский
При наличии полу-сообщения h между S и T справедливо, что энтропия покрытия топологического типа для T над φ(F) не превышает энтропию покрытия для S над F, при условии равномерной непрерывности φ на соответствующем множестве.
LaTeX
$$$\\text{Semiconj } φ S T \\Rightarrow \\text{UniformContinuousOn } φ G \\land F \\subseteq G \\land \\text{MapsTo } S G G \\Rightarrow \\text{coverEntropyInf } T (φ''F) \\le \\text{coverEntropyInf } S F$$$
Lean4
theorem coverEntropyInf_image_le_of_uniformContinuousOn_invariant [UniformSpace X] [UniformSpace Y] {S : X → X}
{T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) {F G : Set X} (h' : UniformContinuousOn φ G) (hF : F ⊆ G)
(hG : MapsTo S G G) : coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F :=
by
rw [← coverEntropyInf_restrict_subset hF hG]
have hφ : Semiconj (G.restrict φ) (hG.restrict S G G) T :=
by
intro a
rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq a]
apply (coverEntropyInf_image_le_of_uniformContinuous hφ (uniformContinuousOn_iff_restrict.1 h') (val ⁻¹' F)).trans_eq'
rw [← image_image_val_eq_restrict_image, image_preimage_coe G F, inter_eq_right.2 hF]
