OAI/MeasureTheory/Falconer/Angular/AngularTerminal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Terminal independent angular energies in every dimension

Only the sup norm of the actual endpoint symbols and the two original cell masses enter the stopping estimate. The radial shell measure is normalized, so its total mass has no frequency factor.

  1. theorem OAI.Falconer.independentAngularEnergy_bound line 16
  2. theorem OAI.Falconer.endpoint_angular_terminal line 42