coverEntropyEntourage_le_coverEntropyInfEntourage

English

The entropy defined via sup is bounded above by the entropy defined via inf: coverEntropyEntourage ≤ coverEntropyInfEntourage.

Русский

Энтропия через sup не превосходит энтропию через inf: coverEntropyEntourage ≤ coverEntropyInfEntourage.

LaTeX

$$$\mathrm{coverEntropyEntourage}(T,F,U) \leq \mathrm{coverEntropyInfEntourage}(T,F,U)$$$

Lean4

theorem coverEntropyEntourage_le_coverEntropyInfEntourage {T : X → X} {F : Set X} (F_inv : MapsTo T F F)
    {U : Set (X × X)} (U_symm : IsSymmetricRel U) :
    coverEntropyEntourage T F (U ○ U) ≤ coverEntropyInfEntourage T F U :=
  by
  refine (le_liminf_of_le) (eventually_atTop.2 ⟨1, fun m m_pos ↦ ?_⟩)
  exact coverEntropyEntourage_le_log_coverMincard_div F_inv U_symm (Nat.one_le_iff_ne_zero.1 m_pos)

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