OAI/MeasureTheory/Falconer/Radial/ClassicalAffineDistance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The strict classical threshold on a charged affine plane

Coordinates are used isometrically inside the actual affine plane, so the conclusion concerns original distances.

  1. theorem OAI.Falconer.frostman_exponent_le_dimension line 17
  2. theorem OAI.Falconer.classical_distance_in_affine_plane line 27