OAI/Analysis/RieszRectifiability/Kernel/OscillationEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fractional height energy from scalar oscillation

A squared cutoff times a centered Lipschitz height is a mean-zero test with an explicit Lipschitz bound. Scalar Riesz oscillation controls its pairing; combined with the ball and shell second-moment estimates, this bounds the fractional pair energy of the rescaled height on the inner ball.

  1. def OAI.RieszRectifiability.centeredHeightTestConstant line 22
  2. theorem OAI.RieszRectifiability.lipschitz_height_bound_on_support line 25
  3. theorem OAI.RieszRectifiability.centered_height_test_oscillation_bound line 41
  4. theorem OAI.RieszRectifiability.inner_energy_bound_from_oscillation line 86