OAI/Analysis/RieszRectifiability/Foundations/DyadicLipschitzFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Normalized dyadic Lipschitz test families

The family packages mean-zero compactly supported tests with dyadic radii, separated centers, and weights whose squares are the dimensional powers of the radii. Its support and regularity assumptions give integrability, while global upper growth gives weighted Gram estimates at both finer and coarser scales.

  1. structure OAI.RieszRectifiability.DyadicLipschitzFamily line 22
  2. theorem OAI.RieszRectifiability.DyadicLipschitzFamily.memLp_integrable line 43
  3. theorem OAI.RieszRectifiability.DyadicLipschitzFamily.support_ball line 49
  4. theorem OAI.RieszRectifiability.DyadicLipschitzFamily.radius_antitone line 55
  5. theorem OAI.RieszRectifiability.DyadicLipschitzFamily.radius_eq_of_level_eq line 63
  6. theorem OAI.RieszRectifiability.DyadicLipschitzFamily.fine_gram line 69
  7. theorem OAI.RieszRectifiability.DyadicLipschitzFamily.coarse_gram line 81