English
Similarly, expGrowthSup(u+v) ≤ expGrowthSup u ⊔ expGrowthSup v.
Русский
Аналогично, expGrowthSup(u+v) ≤ expGrowthSup(u) ⊔ expGrowthSup(v).
LaTeX
$$$\expGrowthSup(u+v) = \expGrowthSup(u) \sqcup \expGrowthSup(v)$$$
Lean4
theorem expGrowthSup_add : expGrowthSup (u + v) = expGrowthSup u ⊔ expGrowthSup v :=
by
rw [← expGrowthSup_sup]
apply le_antisymm
· refine expGrowthSup_le_of_eventually_le (b := 2) ofNat_ne_top (Eventually.of_forall fun n ↦ ?_)
rw [Pi.sup_apply u v n, Pi.add_apply u v n, two_mul]
exact add_le_add (le_max_left (u n) (v n)) (le_max_right (u n) (v n))
· refine expGrowthSup_monotone fun n ↦ ?_
exact
sup_le (self_le_add_right (u n) (v n))
(self_le_add_left (v n) (u n))
-- By lemma `expGrowthSup_add`, `expGrowthSup` is an `AddMonoidHom` from `ℕ → ℝ≥0∞` to
-- `Tropical ERealᵒᵈ`. Lemma `expGrowthSup_sum` is exactly `Finset.trop_inf`. We prove it from
-- scratch to reduce imports.
