OAI/Analysis/RieszRectifiability/Kernel/GradientRieszTestIdentity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Gradient identities for scalar Riesz tests

Summing directional Schwartz derivatives over an orthonormal basis recovers the dilated fractional gradient kernel. Integrating this identity and passing to vanishing capped truncations yields the fractional Schwartz integral with its factor of negative one half.

  1. abbrev OAI.RieszRectifiability.scalarSchwartzDerivative line 22
  2. theorem OAI.RieszRectifiability.sum_symmetricScalarRieszTestKernel_gradient line 25
  3. theorem OAI.RieszRectifiability.sum_scalarRieszSchwartzTest_gradient line 40
  4. theorem OAI.RieszRectifiability.sum_scalarCappedTransform_gradient_tendsto line 64