Theorem MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv

Modification history

2024-06-28 22:16
Mathlib/MeasureTheory/Integral/SobolevInequality.lean
feat: prove the Gagliardo-Nirenberg-Sobolev inequality (#14165) …
Added MeasureTheory.lintegral_pow_le_pow_lintegral_fderivView on Github →