Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-29 17:35
03cf1129
View on Github →
feat: remove completeness assumption in Sobolev inequality (
#14262
)
Estimated changes
Modified
Mathlib/Analysis/Normed/Group/Completion.lean
added
theorem
UniformSpace.Completion.nnnorm_coe
Modified
Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
added
theorem
HasCompactSupport.ennnorm_le_lintegral_Ici_deriv
Modified
Mathlib/MeasureTheory/Integral/SobolevInequality.lean
modified
theorem
MeasureTheory.lintegral_prod_lintegral_pow_le