OAI/MeasureTheory/Falconer/Geometry/EuclideanRieszEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite Riesz energies from the original all-dimensional Frostman bounds

The dyadic potential argument and its scalar scale identity are dimension independent.

  1. def OAI.Falconer.euclideanRieszPotential line 17
  2. def OAI.Falconer.euclideanEnergyMajorant line 20
  3. theorem OAI.Falconer.euclidean_riesz_kernel_majorant line 24
  4. theorem OAI.Falconer.euclidean_energy_term_integral_le line 53
  5. theorem OAI.Falconer.euclidean_riesz_potential_uniform_bound line 69
  6. theorem OAI.Falconer.rieszEnergyOn_lt_top_of_frostman line 99