coverEntropyInfEntourage_le_netEntropyInfEntourage

English

For a symmetric U, coverEntropyInfEntourage T F U ≤ netEntropyInfEntourage T F U.

Русский

Для симметричной U: coverEntropyInfEntourage T F U ≤ netEntropyInfEntourage T F U.

LaTeX

$$$\text{coverEntropyInfEntourage}(T,F,U)\le \text{netEntropyInfEntourage}(T,F,U)$$$

Lean4

theorem coverEntropyInfEntourage_le_netEntropyInfEntourage (T : X → X) (F : Set X) {U : Set (X × X)} (U_rfl : idRel ⊆ U)
    (U_symm : IsSymmetricRel U) : coverEntropyInfEntourage T F (U ○ U) ≤ netEntropyInfEntourage T F U :=
  expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_le_netMaxcard T F U_rfl U_symm n)

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