OAI/MeasureTheory/Falconer/Radial/SingleStationaryRadial.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One stationary sphere against an unexpanded small displacement

Only the large sphere is expanded. The second displacement remains an arbitrary scalar projection, bounded by the smaller displacement length.

  1. def OAI.Falconer.singleSignedRadialCoefficient line 15
  2. theorem OAI.Falconer.singleSignedRadial_derivatives line 20
  3. theorem OAI.Falconer.singleSignedRadial_noncomparable line 50