OAI/Analysis/RieszRectifiability/Rigidity/FractionalDilationDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Differentiating dilated fractional kernels

Measurability and the gradient dominator justify differentiation under the integral near dilation one. Comparing with the dilation scaling identity identifies the integrated gradient kernel with the fractional Schwartz kernel, and hence gives the gradient representation of the fractional test.

  1. theorem OAI.RieszRectifiability.dilatedFractionalKernel_aestronglyMeasurable line 23
  2. theorem OAI.RieszRectifiability.dilatedFractionalGradientKernel_aestronglyMeasurable line 32
  3. theorem OAI.RieszRectifiability.fractional_gradient_integral_identity line 45
  4. theorem OAI.RieszRectifiability.fractionalSchwartzTest_eq_gradient_integral line 78