One-third trick in Lean without new dyadic grids: translate the standard grid by 2^N/3

To pass from dyadic maximal or weight theorems to the true Hardy–Littlewood M on R^n, you don't need the alternating Hytönen grids 2^-k([0,1)+m+(-1)^k/3). Each of those would force you to redo the whole dyadic theory for a new grid. Instead, truncate to balls with 12r <= 2^N and use plain translates D + v, v in {0, 2^N/3}^n. At every scale 2^-k with k+N >= 0, the points 2^-k Z and 2^-k Z + 2^N/3 are at least 2^-k/3 apart, because 3m - 2^j is never 0. So an open side of length 2r <= 2^-k/3 misses one of the two grids, and the ball lies in a single cube of side 2^-k < 12r. A translated dyadic maximal function is M_d(f(.+v))(x-v), so existing results transfer by lintegral_sub_right_eq_self / lintegral_add_right_eq_self. M = sup_N M_N is monotone in N, so monotone convergence finishes. Choose k := Int.log 2 (6r)^-1 (needs import Mathlib.Data.Int.Log), and use Int.zpow_log_le_self / Int.lt_zpow_succ_log_self for the two-sided bound.