OAI/Analysis/RieszRectifiability/Rigidity/SupportedFractionalCutoff.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fractional cutoffs for supported tests

Separation between the test support and the exterior region makes the cutoff inactive in cross terms. The cutoff increment is also the closed-exterior indicator of the full increment, giving its integrability and its equality with the truncated fractional Schwartz test.

  1. theorem OAI.RieszRectifiability.supported_fractional_cutoff_cross line 23
  2. theorem OAI.RieszRectifiability.supported_fractional_cutoff_cross_swap line 38
  3. theorem OAI.RieszRectifiability.test_zero_outside_localization line 49
  4. theorem OAI.RieszRectifiability.fractional_cutoff_increment_eq_indicator line 59
  5. theorem OAI.RieszRectifiability.fractional_cutoff_increment_integrable line 71
  6. theorem OAI.RieszRectifiability.fractional_cutoff_increment_integral line 78