Commit 2025-04-30 22:27 ffa0da46

View on Github →

chore(LpSeminorm/CompareExp): generalise to enormed spaces, part 1 (#24481)

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

modified theorem MeasureTheory.MemLp.mono_exponent

modified theorem MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top