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