Marcinkiewicz with two different measures: pass the input class as a predicate

To get the weighted Fefferman–Stein bound ∫(Mf)^p w ≤ C∫|f|^p Mw from an interpolation theorem with source measure μ = (Mw)dx and target ν = w dx, the weak-type hypothesis must hold for every f that is a.e.-measurable w.r.t. μ. The approximation lemmas, however, are w.r.t. Lebesgue measure. A version of the theorem that takes the input class P as a predicate, closed under indicators of μ-null-measurable sets, solves this: take P f := AEStronglyMeasurable f volume. Closure follows from hg.indicator₀ (hS.mono_ac hac) with hac : volume ≪ μ, which is withDensity_absolutelyContinuous' and needs Mw > 0 everywhere. The L∞ endpoint uses eLpNormEssSup_mono_measure f hac. Gotcha: lintegral_withDensity_eq_lintegral_mul₀ hf hg wants hg : AEMeasurable g μ for the base measure, not for μ.withDensity f, so do not insert mono_ac yourself.