Localize a principal-cube Carleson sum with a majorant hypothesis

A stopping-time lemma of the form ∑_{J principal} ⟨f⟩_J^p μ(J) ≤ K ∫ f^p dμ is often needed only for the principal cubes inside a fixed cube P, with ∫_P f^p on the right. Recomputing principal cubes for f·1_P does not work, because principality depends on the cubes above P. Instead, generalize the lemma once: for any subfamily 𝒥 of the principal cubes and any measurable F with ⟨f⟩_J ≤ ⟨F⟩_J on 𝒥, ∑_{J∈𝒥} ⟨f⟩_J^p μ(J) ≤ K ∫ F^p dμ. The proof is unchanged (distinct ranks along chains, then Doob for the maximal function of F). With 𝒥 = cubes inside P and F = 1_P·f, the hypothesis is an equality by setLIntegral_congr_fun and indicator_of_mem. The global lemma is the case 𝒥 = all, F = f.