OAI/Analysis/RieszRectifiability/Rigidity/FractionalGradientBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounds for dilated fractional gradients

Lipschitz control of the derivative bounds symmetric dilated differences near the origin. Radial Schwartz decay controls the far region, providing the two estimates needed for fractional-gradient integrability and dilation arguments.

  1. theorem OAI.RieszRectifiability.lipschitz_fderiv_dilated_difference_bound line 23
  2. theorem OAI.RieszRectifiability.schwartz_dilated_fractional_gradient_near_bound line 44
  3. theorem OAI.RieszRectifiability.norm_le_twice_affine_shift line 76
  4. theorem OAI.RieszRectifiability.schwartz_operator_apply_radial_bound line 84
  5. theorem OAI.RieszRectifiability.schwartz_dilated_fractional_gradient_far_bound line 98