OAI/Analysis/RieszRectifiability/Kernel/MeanZeroSchwartzApproximation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RieszRectifiability.unitSmoothCutoff_integral_pos line 14
2. theorem OAI.RieszRectifiability.exists_compact_complex_schwartz_unit_integral line 25
3. theorem OAI.RieszRectifiability.exists_compact_mean_zero_schwartz_approximation line 43
4. theorem OAI.RieszRectifiability.inverse_fourier_has_compact_mean_zero_approximants line 63
5. theorem OAI.RieszRectifiability.tempered_distribution_zero_on_mean_zero_tests line 70