English
For a dynamic cover h of T on F with U and a bound s, coverEntropyEntourage is controlled by log-card bounds.
Русский
Для динамического покрытия h и окружения U предел энтропии контролируется логарифмическими ограничениями по карте покрытия.
LaTeX
$$∀ h:IsDynCoverOf(T,F,U,n,s), coverEntropyEntourage(T,F,(U\circ U)) ≤ log s.card / n$$
Lean4
theorem coverEntropyEntourage_le_log_card_div {T : X → X} {F : Set X} (F_inv : MapsTo T F F) {U : Set (X × X)}
(U_symm : IsSymmetricRel U) {n : ℕ} (n_pos : n ≠ 0) {s : Finset X} (h : IsDynCoverOf T F U n s) :
coverEntropyEntourage T F (U ○ U) ≤ log s.card / n :=
by
apply (coverEntropyEntourage_le_log_coverMincard_div F_inv U_symm n_pos).trans
apply monotone_div_right_of_nonneg n.cast_nonneg' (log_monotone _)
exact_mod_cast coverMincard_le_card h