OAI/MeasureTheory/Falconer/Geometry/PlanarChartRepair.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Choosing bounded representatives of almost-everywhere planar chart maps

  1. def OAI.Falconer.boundedPlanarPoint line 10
  2. def OAI.Falconer.chartedPlanarDirection line 13
  3. theorem OAI.Falconer.boundedPlanarPoint_measurable line 17
  4. theorem OAI.Falconer.chartedPlanarDirection_measurable line 20
  5. theorem OAI.Falconer.boundedPlanarPoint_norm line 30
  6. theorem OAI.Falconer.chartedPlanarDirection_unit line 36
  7. theorem OAI.Falconer.chartedPlanarDirection_chart line 42
  8. theorem OAI.Falconer.boundedPlanarPoint_eq line 49
  9. theorem OAI.Falconer.chartedPlanarDirection_eq line 52