OAI/Analysis/RieszRectifiability/Rigidity/FractionalSymbolBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the fractional symbol

The cosine difference defining the fractional symbol is nonnegative and has quadratic cancellation near the origin. Combining this local bound with inverse-power decay at infinity gives integrability under upper growth bounds, in particular for volume.

  1. def OAI.RieszRectifiability.fractionalSymbolKernel line 20
  2. def OAI.RieszRectifiability.fractionalSymbol line 23
  3. theorem OAI.RieszRectifiability.fractionalSymbolKernel_nonneg line 26
  4. theorem OAI.RieszRectifiability.fractionalSymbolKernel_measurable line 30
  5. theorem OAI.RieszRectifiability.one_sub_cos_inner_quadratic line 35
  6. theorem OAI.RieszRectifiability.fractionalSymbolKernel_near_bound line 53
  7. theorem OAI.RieszRectifiability.fractionalSymbolKernel_far_bound line 70
  8. theorem OAI.RieszRectifiability.fractionalSymbolKernel_integrable_of_growth line 77
  9. theorem OAI.RieszRectifiability.fractionalSymbolKernel_integrable line 98
  10. theorem OAI.RieszRectifiability.fractionalSymbol_nonneg line 102
  11. theorem OAI.RieszRectifiability.fractionalSymbol_zero line 105