theorem MeasureTheory.Memℒp.mono_exponent {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [NormedAddCommGroup E] {p q : ENNReal} {f : α → E} (hpq : p ≤ q) (hfq : MeasureTheory.Memℒp f q μ) : MeasureTheory.Memℒp f p μ