OAI/MeasureTheory/Falconer/Recursion/PointRieszPotential.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A Riesz potential bound from small balls at one fixed center

  1. def OAI.Falconer.rieszSmallBallBound line 11
  2. theorem OAI.Falconer.rieszSmallBallBound_lt_top line 15
  3. theorem OAI.Falconer.singleton_eq_zero_of_point_frostman line 22
  4. theorem OAI.Falconer.point_energy_term_integral_le line 35
  5. theorem OAI.Falconer.point_riesz_potential_bound line 51