Absorbing the outer collapse-shape sum #
The number of admissible block-composition shapes is at most 2^n. In the
final scalar ledger that same factor has already been placed on the left of
each fixed-shape estimate. The lemma below cancels these two occurrences
without introducing division.
theorem
Anderson4D.sum_le_of_card_le_two_pow_of_two_pow_mul_le
{ι : Type u_1}
[DecidableEq ι]
(S : Finset ι)
(F : ι → ℝ)
(B : ℝ)
(n : ℕ)
(hcard : S.card ≤ 2 ^ n)
(hB : 0 ≤ B)
(hscaled : ∀ x ∈ S, 2 ^ n * F x ≤ B)
:
If there are at most 2^n terms and every term multiplied by 2^n is
bounded by the same nonnegative target, then their sum is bounded by that
target.