The upper bound via compression

Compress S to a closed set T (exists_closed, Lemma 2), then bound the runs of T by the radicals of its elements (sum_L_le_of_closed, Lemma 3 and equation (7)).

theorem RunsOfMultiples.sum_L_eq_sum_card_A (S : Finset ℕ) (hS : ∀ a ∈ S, 0 < a) : ∑ a ∈ S, L S a = ∑ t ∈ Finset.Icc 1 S.card, (A S t).card

∑_{a ∈ S} L S a = ∑_{t = 1}^{|S|} |A S t|.

theorem RunsOfMultiples.upper_bound_alt : ∃ (C : ℝ) (N : ℕ), ∀ (S : Finset ℕ), (∀ a ∈ S, 0 < a) → N ≤ S.card → ↑(∑ a ∈ S, kVal S a) ≤ C * ↑S.card * Real.log ↑S.card * Real.log (Real.log ↑S.card)

Upper bound, second proof.