OAI/Analysis/RieszRectifiability/Limits/CompactDerivativeTests.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported directional derivative tests

Directional derivatives of smooth compactly supported functions remain continuous and compactly supported, with support inside that of the original function. Integration by parts against the constant function shows that their volume integral vanishes, making them mean-zero test functions.

  1. theorem OAI.RieszRectifiability.compact_smooth_directional_derivative_test line 22