OAI/Analysis/RieszRectifiability/Limits/CompactSchwartzApproximation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported approximation in Schwartz space

Expanding smooth cutoffs approximate Schwartz functions in the Schwartz topology. Continuity of directional differentiation preserves this convergence, while compact support ensures the approximating derivatives have zero integral. Consequently, tempered distributions are determined by their compactly supported Schwartz tests.

  1. theorem OAI.RieszRectifiability.exists_compact_schwartz_approximation line 24
  2. theorem OAI.RieszRectifiability.exists_compact_directional_schwartz_approximation line 56
  3. theorem OAI.RieszRectifiability.tempered_distribution_eq_of_compact_tests line 69