OAI/MeasureTheory/Falconer/Recursion/ProfileNear.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The normalized near reduction for the actual regularized profile

The child energies retain the original endpoint symbols. No separation of the parent cells is imposed; the near relation is on their two internal center displacements, as in the manuscript.

  1. def OAI.Falconer.profileModelMass line 20
  2. theorem OAI.Falconer.profile_near_prefactor line 23
  3. def OAI.Falconer.profileNearEnergy line 42
  4. theorem OAI.Falconer.profile_near_reduction line 56
  5. theorem OAI.Falconer.profile_angular_terminal line 129