OAI/Analysis/RieszRectifiability/Kernel/DerivativeTests.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Analytic bounds for Schwartz test functions

Integration by parts shows that a Schwartz directional derivative has zero integral. The zeroth Schwartz seminorms of a test function and its Fréchet derivative also give global boundedness and Lipschitz constants.

  1. theorem OAI.RieszRectifiability.schwartz_directional_derivative_integral_zero line 21
  2. theorem OAI.RieszRectifiability.schwartz_real_bounded_lipschitz line 32
  3. theorem OAI.RieszRectifiability.compact_smooth_directional_test_admissible line 45