coverEntropyInfEntourage_monotone

English

The entropy-entourage functional is monotone with respect to the set in its argument.

Русский

Функционал энтропии-окружения монотонен по аргументу множества.

LaTeX

$$$\\text{Monotone}(F \\mapsto \\mathrm{coverEntropyEntourage}(T, F, U))$$$

Lean4

theorem coverEntropyInfEntourage_monotone (T : X → X) (U : Set (X × X)) :
    Monotone fun F : Set X ↦ coverEntropyInfEntourage T F U :=
  by
  refine fun F G F_G ↦ ExpGrowth.expGrowthInf_monotone fun n ↦ ?_
  exact ENat.toENNReal_mono (coverMincard_monotone_subset T U n F_G)

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