Lean4
/-- From a dynamical cover `s` with entourage `U` and time `m`, we construct covers with entourage
`U ○ U` and any multiple `m * n` of `m` with controlled cardinality. This lemma is the first step
in a submultiplicative-like property of `coverMincard`, with consequences such as explicit bounds
for the topological entropy (`coverEntropyInfEntourage_le_card_div`) and an equality between
two notions of topological entropy (`coverEntropyInf_eq_coverEntropySup_of_inv`). -/
theorem iterate_le_pow {T : X → X} {F : Set X} (F_inv : MapsTo T F F) {U : Set (X × X)} (U_symm : IsSymmetricRel U)
{m : ℕ} (n : ℕ) {s : Finset X} (h : IsDynCoverOf T F U m s) :
∃ t : Finset X, IsDynCoverOf T F (U ○ U) (m * n) t ∧ t.card ≤ s.card ^ n := by
classical
-- Deal with the edge cases: `F = ∅` or `m = 0`.
rcases F.eq_empty_or_nonempty with rfl | F_nemp
· exact ⟨∅, by simp⟩
have _ : Nonempty X := F_nemp.nonempty
have s_nemp := h.nonempty F_nemp
obtain ⟨x, x_F⟩ := F_nemp
rcases m.eq_zero_or_pos with rfl | m_pos
· use { x }
simp only [zero_mul, Finset.coe_singleton, Finset.card_singleton]
exact
⟨isDynCoverOf_zero T F (U ○ U) (singleton_nonempty x),
one_le_pow_of_one_le' (Nat.one_le_of_lt (Finset.Nonempty.card_pos s_nemp)) n⟩
-- The proof goes as follows. Given an orbit of length `(m * n)` starting from `y`, each of its
-- iterates `y`, `T^[m] y`, `T^[m]^[2] y` ... is `(dynEntourage T U m)`-close to a point of `s`.
-- Conversely, given a sequence `t 0`, `t 1`, `t 2` of points in `s`, we choose a point
-- `z = dyncover t` such that `z`, `T^[m] z`, `T^[m]^[2] z` ... are `(dynEntourage T U m)`-close
-- to `t 0`, `t 1`, `t 2`... Then `y`, `T^[m] y`, `T^[m]^[2] y` ... are
-- `(dynEntourage T (U ○ U) m)`-close to `z`, `T^[m] z`, `T^[m]^[2] z`, so that the union of such
-- `z` provides the desired cover. Since there are at most `s.card ^ n` sequences of
-- length `n` with values in `s`, we get the upper bound we want on the cardinality.
-- First step: construct `dyncover`. Given `t 0`, `t 1`, `t 2`, if we cannot find such a point
-- `dyncover t`, we use the dummy `x`.
have (t : Fin n → s) :
∃ y : X, (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)) ⊆ ball y (dynEntourage T (U ○ U) (m * n)) :=
by
rcases (⋂ k : Fin n, T^[m * k] ⁻¹' ball (t k) (dynEntourage T U m)).eq_empty_or_nonempty with inter_empt |
inter_nemp
· exact inter_empt ▸ ⟨x, empty_subset _⟩
· obtain ⟨y, y_int⟩ := inter_nemp
refine ⟨y, fun z z_int ↦ ?_⟩
simp only [ball, dynEntourage, Prod.map_iterate, mem_preimage, mem_iInter, Prod.map_apply] at y_int z_int ⊢
intro k k_mn
replace k_mn := Nat.div_lt_of_lt_mul k_mn
specialize z_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
specialize y_int ⟨(k / m), k_mn⟩ (k % m) (Nat.mod_lt k m_pos)
rw [← Function.iterate_add_apply T (k % m) (m * (k / m)), Nat.mod_add_div k m] at y_int z_int
exact mem_comp_of_mem_ball U_symm y_int z_int
choose! dyncover h_dyncover using this
let sn := range dyncover
refine ⟨sn.toFinset, ?_, ?_⟩
· -- We implement the argument at the beginning: given `y ∈ F`, we extract `t 0`, `t 1`, `t 2`
-- such that `y`, `T^[m] y`, `T^[m]^[2] y` ... is `(dynEntourage T U m)`-close to `t 0`, `t 1`,
-- `t 2`... Then `dyncover t` is a point of `range dyncover` which satisfies the conclusion
-- of the lemma.
rw [Finset.coe_nonempty] at s_nemp
have _ : Nonempty s := Finset.Nonempty.coe_sort s_nemp
intro y y_F
have key : ∀ k : Fin n, ∃ z : s, y ∈ T^[m * k] ⁻¹' ball z (dynEntourage T U m) :=
by
intro k
have := h (MapsTo.iterate F_inv (m * k) y_F)
simp only [mem_iUnion, exists_prop] at this
obtain ⟨z, z_s, hz⟩ := this
exact ⟨⟨z, z_s⟩, hz⟩
choose! t ht using key
simp only [toFinset_range, Finset.coe_image, Finset.coe_univ, image_univ, mem_range, iUnion_exists,
iUnion_iUnion_eq', mem_iUnion, sn]
use t
apply h_dyncover t
simp only [mem_iInter, mem_preimage] at ht ⊢
exact ht
· rw [toFinset_card]
apply (Fintype.card_range_le dyncover).trans
simp only [Fintype.card_fun, Fintype.card_coe, Fintype.card_fin, le_refl]
