OAI/MeasureTheory/Falconer/Estimates/QuarterEndpointMap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A fixed quarter chart closes under the actual local cell map. Its contraction does not accumulate with the number of selected intervals.

  1. def OAI.Falconer.quarterEndpointPoint line 13
  2. def OAI.Falconer.quarterEndpointSet line 18
  3. theorem OAI.Falconer.quarterEndpointPoint_eq line 22
  4. theorem OAI.Falconer.quarterEndpointSet_eq line 30
  5. theorem OAI.Falconer.quarterEndpointPoint_dist line 38
  6. theorem OAI.Falconer.quarterEndpointPoint_injOn line 43
  7. theorem OAI.Falconer.quarterEndpointSet_geometry line 51
  8. theorem OAI.Falconer.quarterEndpointPoint_local line 79
  9. theorem OAI.Falconer.quarterEndpointPoint_near line 90