English
For any T, F, G and U, the entropyEntourage of the union equals the maximum of the entropies of the parts.
Русский
Энтропия по энтourage при объединении множеств равна максимуму энтропий по компонентам.
LaTeX
$$$\operatorname{coverEntropyEntourage}(T, F \cup G, U) = \max\big( \operatorname{coverEntropyEntourage}(T, F, U), \operatorname{coverEntropyEntourage}(T, G, U) \big)$$$
Lean4
theorem coverEntropyEntourage_union {T : X → X} {F G : Set X} {U : Set (X × X)} :
coverEntropyEntourage T (F ∪ G) U = max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) :=
by
refine le_antisymm ?_ ?_
· apply le_of_le_of_eq (expGrowthSup_monotone fun n ↦ ?_) expGrowthSup_add
rw [Pi.add_apply, ← ENat.toENNReal_add]
exact ENat.toENNReal_mono (coverMincard_union_le T F G U n)
·
exact
max_le (coverEntropyEntourage_monotone T U subset_union_left)
(coverEntropyEntourage_monotone T U subset_union_right)
