OAI/MeasureTheory/Falconer/Estimates/PlanarQuarter.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A fixed contraction puts the actual two projection coordinates inside one bounded square without changing their finite combinatorics.

  1. def OAI.Falconer.planarQuarter line 10
  2. theorem OAI.Falconer.planarQuarter_apply line 12
  3. theorem OAI.Falconer.planarQuarter_dist line 16
  4. theorem OAI.Falconer.planarQuarter_injective line 22
  5. theorem OAI.Falconer.planarQuarter_right_inverse line 27
  6. theorem OAI.Falconer.planarQuarter_separated line 33
  7. theorem OAI.Falconer.planarQuarter_regular line 42