English
Under standard hypotheses, coverEntropyEntourage T F (U○U) ≤ log(coverMincard T F U n) / n for nonzero n.
Русский
При обычных предположениях выполняется: coverEntropyEntourage T F (U○U) ≤ log(coverMincard T F U n) / n для ненулевого n.
LaTeX
$$$coverEntropyEntourage(T,F,(U\circ U)) ≤ \dfrac{\log(coverMincard(T,F,U,n))}{n}$$$
Lean4
theorem coverEntropyEntourage_le_log_coverMincard_div {T : X → X} {F : Set X} (F_inv : MapsTo T F F) {U : Set (X × X)}
(U_symm : IsSymmetricRel U) {n : ℕ} (n_pos : n ≠ 0) :
coverEntropyEntourage T F (U ○ U) ≤ log (coverMincard T F U n) / n :=
by
have cv_mono : Monotone fun m ↦ (coverMincard T F (U ○ U) m).toENNReal := fun _ _ k_m ↦
ENat.toENNReal_mono (coverMincard_monotone_time T F (U ○ U) k_m)
have h := cv_mono.expGrowthSup_comp_mul n_pos
rw [mul_comm, ← div_eq_iff (natCast_ne_bot n) (natCast_ne_top n) (Nat.cast_ne_zero.2 n_pos)] at h
rw [coverEntropyEntourage, ← h]
apply monotone_div_right_of_nonneg n.cast_nonneg'
rw [← expGrowthSup_pow]
refine expGrowthSup_monotone fun m ↦ ?_
rw [← ENat.toENNReal_pow]
exact ENat.toENNReal_mono (coverMincard_mul_le_pow F_inv U_symm n m)
