Commit 2024-06-28 22:16 6c7310ca

View on Github →

feat: prove the Gagliardo-Nirenberg-Sobolev inequality (#14165)

From the Sobolev inequality project

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem MeasureTheory.snorm_restrict_eq

Created Mathlib/MeasureTheory/Integral/SobolevInequality.lean

added def MeasureTheory.GridLines.T

added theorem MeasureTheory.GridLines.T_empty

added theorem MeasureTheory.GridLines.T_insert_le_T_lmarginal_singleton

added theorem MeasureTheory.GridLines.T_lmarginal_antitone

added theorem MeasureTheory.GridLines.T_univ

added theorem MeasureTheory.lintegral_mul_prod_lintegral_pow_le

added theorem MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv

added theorem MeasureTheory.lintegral_pow_le_pow_lintegral_fderiv_aux

added theorem MeasureTheory.lintegral_prod_lintegral_pow_le

added def MeasureTheory.snormLESNormFDerivOfEqInnerConst

added theorem MeasureTheory.snorm_le_snorm_fderiv

added theorem MeasureTheory.snorm_le_snorm_fderiv_of_eq

added theorem MeasureTheory.snorm_le_snorm_fderiv_of_eq_inner

added theorem MeasureTheory.snorm_le_snorm_fderiv_of_le

added theorem MeasureTheory.snorm_le_snorm_fderiv_one