OAI/MeasureTheory/Falconer/Measures/ScalarProductBalls.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fine-scale ball bounds for a Cartesian product of separated scalar sets, with its actual Euclidean embedding.

  1. theorem OAI.Falconer.scalar_interval_card line 9
  2. def OAI.Falconer.scalarProductPoints line 31
  3. theorem OAI.Falconer.rowPoint_pair_injective line 34
  4. theorem OAI.Falconer.scalarProductPoints_card line 40
  5. theorem OAI.Falconer.scalarProductPoints_ball_card line 44
  6. theorem OAI.Falconer.scalarProductPoints_fine_ball line 65