OAI/Analysis/RieszRectifiability/Kernel/UncenteredEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Subtracting the cutoff mean reduces an uncentered height test to the normalized energy estimate. Centered moment and tail bounds determine the resulting quantitative coefficient.

  1. def OAI.RieszRectifiability.uncenteredEnergyCoefficient line 18
  2. theorem OAI.RieszRectifiability.uncentered_inner_energy_bound line 23