coverEntropyInfEntourage_nonneg — Mathlib

English

Under assumptions with F invariant under T and U symmetric, for nonzero n we have: coverEntropyEntourage T F (U○U) ≤ log (coverMincard T F U n) / n.

Русский

При условии инвариантности F относительно T и симметричности U выполняется: coverEntropyEntourage T F (U○U) ≤ log(coverMincard T F U n) / n для ненулевого n.

LaTeX

$$$coverEntropyEntourage(T,F,(U\circ U)) \leq \dfrac{\log(coverMincard(T,F,U,n))}{n}$$$

Lean4

theorem coverEntropyInfEntourage_nonneg (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) :
    0 ≤ coverEntropyInfEntourage T F U := by
  apply Monotone.expGrowthInf_nonneg
  · exact fun _ _ m_n ↦ ENat.toENNReal_mono (coverMincard_monotone_time T F U m_n)
  · rw [ne_eq, funext_iff.not, not_forall]
    use 0
    rw [coverMincard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]
    exact one_ne_zero

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