OAI/MeasureTheory/Falconer/Estimates/SixInputsMain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the classical-threshold input by strict dimension descent

The charged affine plane has smaller dimension than the original space. Its distance conclusion therefore follows from the induction hypothesis. The planar base case and the higher-dimensional analytic proof stay separate.

  1. theorem OAI.Falconer.mainTarget_of_six_published_inputs line 16
  2. theorem OAI.Falconer.classical_distance_of_six_published_inputs line 44