coverEntropyEntourage_le_netEntropyEntourage

English

For symmetric U, netEntropyInfEntourage T F U ≤ netEntropyEntourage T F U.

Русский

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

LaTeX

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

Lean4

theorem coverEntropyEntourage_le_netEntropyEntourage (T : X → X) (F : Set X) {U : Set (X × X)} (U_rfl : idRel ⊆ U)
    (U_symm : IsSymmetricRel U) : coverEntropyEntourage T F (U ○ U) ≤ netEntropyEntourage T F U :=
  expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_le_netMaxcard T F U_rfl U_symm n)

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