Passing a weighted bound from truncated to full dyadic square function

To pass a weighted L^p bound from truncated square functions S_{a,n} f = (Σ_{a≤k<a+n} |Δ_k f|²)^{1/2} to the full (Σ_{k∈ℤ} |Δ_k f|²)^{1/2}, define the full one as the ENNReal supremum ⨆ m, ‖S_{-m,2m} f x‖ₑ. Prove S_{a,n} ≤ S_{a-1,n+2} using Finset.sum_range_succ', which peels off the new bottom term; the new top term is dropped as nonnegative. This gives monotonicity in m. Then ENNReal.orderIsoRpow.map_iSup pulls ^p through the supremum, and lintegral_iSup finishes. For the reverse comparison, which sharpness needs, bound S_{a,n} ≤ S_{-m,2m} whenever [a, a+n) ⊆ [-m, m). Rewrite both sums with Finset.sum_image over the images of range under (b + ·) in ℤ, then use sum_le_sum_of_subset_of_nonneg. The subset step is ⟨(a + i + m).toNat, by omega, by omega⟩, and omega handles toNat and natAbs directly.