OAI/MeasureTheory/Falconer/Recursion/FiniteProjectionPotential.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite projected-energy average used for the good projections in Orponen--Shmerkin, Appendix A.4. The critical directional loss is linear in the dyadic depth; the planar point potential is strictly subcritical.

  1. theorem OAI.Falconer.finite_projection_potential line 15
  2. def OAI.Falconer.planarProjectionEnergy line 54
  3. theorem OAI.Falconer.finite_projection_energy_average line 58