coverEntropyEntourage_le_log_card_div

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

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