OAI/Analysis/RieszRectifiability/Nets/CellOscillationTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Transferring cell oscillation bounds

Localization independence transfers scalar Riesz oscillation bounds to a contained ball. Comparing the centers and scales then turns a cell-centered bound into the corresponding normalized bound on a nearby ball.

  1. theorem OAI.RieszRectifiability.ScalarOscillationBound.of_ball_subset line 21
  2. theorem OAI.RieszRectifiability.cell_oscillation_controls_nearby_ball line 39