Commit 2025-01-13 10:56 ce6118d7

chore(LpSpace): move results about the L^p norm earlier (#20541) MeasureTheory.Function.LpSpace is supposed to be about the L^p space itself, but contains a bunch of results about the L^p norm as well. Move those results to MeasureTheory.Function.LpSeminorm.Basic and MeasureTheory.Function.LpSeminorm.CompareExp. Also rename lemmas about nesting of L^p norms. From LeanAPAP Moves:

• Memℒp.memℒp_of_exponent_le_of_measure_support_ne_top -> Memℒp.mono_exponent_of_measure_support_ne_top
• Memℒp.memℒp_of_exponent_le -> Memℒp.mono_exponent