English
Let T be a transformation on X, F a subset of X, and U an entourage with idRel ⊆ U and symmetry. For any natural number n, the size of a minimal dynamical cover of F by (U ○ U) is at most the size of a maximal dynamical net of F by U; i.e., coverMincard T F (U ○ U) n ≤ netMaxcard T F U n.
Русский
Пусть T — преобразование на X, F — подмножество X, и U — окрестность с условием idRel ⊆ U и симметричностью. Для любого n минимальная величина покрытия динамически образованного F с помощью (U ○ U) не превосходит максимальную величину динамической сети F с помощью U; то есть coverMincard T F (U ○ U) n ≤ netMaxcard T F U n.
LaTeX
$$$\forall X\;\forall T:X\to X\;\forall F\subseteq X\;\forall U\subseteq X\times X\;\forall n:\mathbb{N},\ (idRel\subseteq U)\land IsSymmetricRel U\Rightarrow\ coverMincard\ T\ F\ (U\circ U)\ n\le\ netMaxcard\ T\ F\ U\ n$$$
Lean4
/-- Given an entourage `U` and a time `n`, a minimal dynamical cover by `U ○ U` has a smaller
cardinality than a maximal dynamical net by `U`. This lemma is the second of two key results to
compare two versions topological entropy: with cover and with nets. -/
theorem coverMincard_le_netMaxcard (T : X → X) (F : Set X) {U : Set (X × X)} (U_rfl : idRel ⊆ U)
(U_symm : IsSymmetricRel U) (n : ℕ) : coverMincard T F (U ○ U) n ≤ netMaxcard T F U n := by
classical
-- WLOG, there exists a maximal dynamical net `s`.
rcases eq_top_or_lt_top (netMaxcard T F U n) with h | h
· exact h ▸ le_top
obtain ⟨s, s_net, s_card⟩ := (netMaxcard_finite_iff T F U n).1 h
rw [← s_card]
apply IsDynCoverOf.coverMincard_le_card
by_contra h
obtain ⟨x, x_F, x_uncov⟩ := not_subset.1 h
simp only [Finset.mem_coe, mem_iUnion, exists_prop, not_exists, not_and] at x_uncov
have larger_net : IsDynNetIn T F U n (insert x s) :=
by
refine ⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩
refine fun y y_s _ ↦ disjoint_left.2 fun z z_x z_y ↦ x_uncov y y_s ?_
exact mem_ball_dynEntourage_comp T n U_symm x y (nonempty_of_mem ⟨z_x, z_y⟩)
rw [← s.coe_insert x] at larger_net
apply larger_net.card_le_netMaxcard.not_gt
rw [← s_card, Nat.cast_lt]
refine (lt_add_one s.card).trans_eq (s.card_insert_of_notMem fun x_s ↦ ?_).symm
apply
x_uncov x x_s
(ball_mono (dynEntourage_monotone T n (subset_comp_self U_rfl)) x
(ball_mono (idRel_subset_dynEntourage T U_rfl n) x _))
simp only [ball, mem_preimage, mem_idRel]
