Weight conventions at a single point break pointwise sup bounds; state lemmas via subcube integrals

I modelled a one-sided power weight t^a as if 0 < t then t^a else 1. Then the pointwise claim 'v ≤ L^a on [0,L)' is false at t = 0, although the claim is true almost everywhere. For maximal-function estimates (∫_R M_R v ≤ B|R|), the clean hypothesis is ∀ dyadic Q ⊆ R, ∫_Q v ≤ B·|Q|, because averages ignore null sets. Prove a pointwise corollary (v ≤ B on R) for the easy cases. In the boundary case, transfer the cube integral to ℝ (for example with a funUnique measure-preserving map), then switch Ico to Ioo with setLIntegral_congr Ioo_ae_eq_Ico, so that t > 0 inside the integral.