Drop global L¹ hypotheses in weighted dyadic theorems: ask only IntegrableOn on cubes

Stopping-time/sparse constructions on dyadic cubes usually use f only through f·1_Q (weak type applied to the localized function) and finiteness of averages over Q. Replace hf : Integrable f by hf : ∀ k m, IntegrableOn f (cube k m); the localized function is integrable by (integrable_indicator_iff (measurableSet_cube _ _)).2 (hf _ _), and finiteness of ⨍⁻ ‖f‖ₑ over Q is just (hf _ _).2.ne (HasFiniteIntegral on the restricted measure). Keep the old Integrable statement as a wrapper via fun k m ↦ hf.integrableOn. For an A_p weight, ∫|f|ᵖw < ∞ gives cube integrability by Hölder against σ = w^{-1/(p-1)}, so a weighted Lᵖ inequality can be stated for every measurable f: split on whether ∫|f|ᵖw = ∞ (then the right side is C·∞ = ∞ once C ≠ 0).