Theorem MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux

Modification history

2024-08-08 10:31
Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
chore: backports for leanprover/lean4#4814 (part 36) (#15612)
Modified MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_auxView on Github →
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_fderiv_auxView on Github →