OAI/MeasureTheory/Falconer/Estimates/DimensionDescent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The charged-plane alternative by induction on the ambient dimension

The affine plane has strictly smaller dimension than the original odd ambient space. The lower-dimensional distance theorem therefore applies to the charged-plane alternative in the dimension induction.

  1. theorem OAI.Falconer.distance_in_affine_plane_of_lower_dimensions line 16
  2. theorem OAI.Falconer.charged_plane_distance_of_lower_dimensions line 66