OAI/Analysis/RieszRectifiability/Foundations/NormalizedLocalEnergyBasic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local integrability of normalized Lipschitz energies

Growth bounds make normalized Lipschitz functions square-integrable on balls and their fractional pair energies integrable on the corresponding product measure. An auxiliary sequence bound absorbs finitely many exceptional scales into one nonnegative bound.

  1. theorem OAI.RieszRectifiability.normalized_lipschitz_memLp_on_ball line 21
  2. theorem OAI.RieszRectifiability.normalized_lipschitz_energy_integrable_on_ball line 30
  3. theorem OAI.RieszRectifiability.nonnegative_uniform_bound_of_eventually_le line 46