OAI/Analysis/RieszRectifiability/Kernel/BallLocalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Localization to balls

Restricting a measure preserves its global upper growth bound and gives finite mass on positive-radius balls. The diameter estimate controls pairs of points in a ball, while the Lipschitz height estimate supplies the boundedness needed for local MemLp control.

  1. theorem OAI.RieszRectifiability.globalGrowth_restrict line 22
  2. theorem OAI.RieszRectifiability.finiteMeasure_restrict_ball_of_globalGrowth line 28
  3. theorem OAI.RieszRectifiability.ball_restriction_mass_bound line 34
  4. theorem OAI.RieszRectifiability.ball_restriction_pair_diameter line 41
  5. theorem OAI.RieszRectifiability.lipschitz_height_bound_on_ball line 54
  6. theorem OAI.RieszRectifiability.lipschitz_height_memLp_on_ball line 64