Commit 2023-12-07 08:20 b06c98e6

View on Github →

feat: a function with vanishing integral against smooth functions supported in U is ae zero in U (#8805) A stronger version of #8800, the differences are:

  • assume either IsSigmaCompact U or SigmaCompactSpace M;
  • only need test functions satisfying tsupport g ⊆ U rather than support g ⊆ U;
  • requires LocallyIntegrableOn U rather than LocallyIntegrable on the whole space. Also fills in some missing APIs around the manifold and measure theory libraries.

Estimated changes

added theorem ContMDiff.extend_one
added theorem Smooth.extend_one
added theorem contMDiff_subtype_val
added theorem smooth_subtype_iff
added theorem smooth_subtype_val