coverEntropyInf_eq_coverEntropy — Mathlib

English

If F is T-invariant (MapsTo T F F), then the inf-entropy equals the entropy: coverEntropyInf(T,F) = coverEntropy(T,F).

Русский

Если F инвариантно относительно T (MapsTo T F F), то инфентропия равна энтропии: coverEntropyInf(T,F) = coverEntropy(T,F).

LaTeX

$$$\text{MapsTo } T F F \Rightarrow \operatorname{coverEntropyInf}(T,F) = \operatorname{coverEntropy}(T,F)$$$

Lean4

theorem coverEntropyInf_eq_coverEntropy (T : X → X) {F : Set X} (h : MapsTo T F F) :
    coverEntropyInf T F = coverEntropy T F :=
  by
  refine le_antisymm (coverEntropyInf_le_coverEntropy T F) (iSup₂_le fun U U_uni ↦ ?_)
  obtain ⟨V, V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni
  exact
    (coverEntropyEntourage_antitone T F V_U).trans
      (le_iSup₂_of_le V V_uni (coverEntropyEntourage_le_coverEntropyInfEntourage h V_symm))

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