OAI/Analysis/RieszRectifiability/Kernel/LocalLipschitzEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Local Lipschitz control of fractional energy

Almost-everywhere Lipschitz difference bounds and bounded pair distances give integrability of fractional pair energies under global upper growth. Their weighted differences lie in L², yielding integrability of the associated bilinear pairing.

  1. theorem OAI.RieszRectifiability.fractionalEnergy_bound_of_difference_bound line 22
  2. theorem OAI.RieszRectifiability.fractionalEnergy_integrable_of_ae_lipschitz line 42
  3. theorem OAI.RieszRectifiability.fractionalBilinear_integrable_of_ae_lipschitz line 62
  4. theorem OAI.RieszRectifiability.ae_difference_bound_of_lipschitzOn line 79
  5. theorem OAI.RieszRectifiability.lipschitzOn_bounded_product_real line 87
  6. theorem OAI.RieszRectifiability.squared_cutoff_height_lipschitzOn line 96
  7. theorem OAI.RieszRectifiability.localized_cutoff_energy_bound line 110