Marcinkiewicz in Lean: parametrize over a truncation-closed class P

A Marcinkiewicz interpolation theorem whose weak-type hypotheses quantify over all AEStronglyMeasurable f cannot be applied to operators bounded only on L¹ ∩ L², such as a Calderón–Zygmund operator defined on L². The proof uses the hypotheses only on f·1_S and f·1_Sᶜ for S = {2‖f‖ > s}, and on their sum. So add a predicate P : (α → E) → Prop with hP : ∀ f, P f → ∀ S, NullMeasurableSet S μ → P (S.indicator f), and replace the measurability hypotheses with P f. The old theorem is then the one-liner with P := AEStronglyMeasurable · μ and hP from AEStronglyMeasurable.indicator₀. For P = L¹ ∩ L², use Integrable.indicator₀ and MemLp.indicator; note that MemLp.indicator takes the set hypothesis first. The layer cake still needs Measurable (T f). Use T' h := if hh : MemLp h 2 then (hT_meas h hh).enorm.mk _ else 0, transfer weak-type bounds with measure_congr, and move ∫⁻ T' f ^ p back with lintegral_congr_ae.