OAI/Analysis/RieszRectifiability/Kernel/MeanZeroGramDecay.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Mean-zero pairing decay

Cancellation against constants turns Lipschitz control into a radius gain for pairings with mean-zero functions. Support-ball mass and growth bounds further control these pairings in terms of the support radius and the uniform size of the mean-zero function.

  1. theorem OAI.RieszRectifiability.mean_zero_lipschitz_pairing_bound line 22
  2. theorem OAI.RieszRectifiability.integral_abs_le_support_ball_mass line 50
  3. theorem OAI.RieszRectifiability.compact_lipschitz_test_memLp line 70
  4. theorem OAI.RieszRectifiability.mean_zero_gram_bound_of_growth line 79
  5. theorem OAI.RieszRectifiability.integral_pairing_zero_of_disjoint_support line 99