OAI/Analysis/LipschitzHilbert/Geometry/UnitDirectionCharts.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

A finite collection of orthogonal charts for a unit direction field. The clipped slope is defined on the whole plane. On its orientation patch it agrees exactly with the ratio of the two coordinates.

  1. def OAI.LipschitzHilbert.horizontalUnit line 16
  2. theorem OAI.LipschitzHilbert.horizontalUnit_norm line 18
  3. def OAI.LipschitzHilbert.directionChart line 21
  4. theorem OAI.LipschitzHilbert.directionChart_center line 24
  5. def OAI.LipschitzHilbert.chartField line 28
  6. theorem OAI.LipschitzHilbert.chartField_lipschitz line 31
  7. theorem OAI.LipschitzHilbert.chartField_unit line 38
  8. theorem OAI.LipschitzHilbert.coordinate_lipschitz line 43
  9. def OAI.LipschitzHilbert.chartDenominator line 49
  10. def OAI.LipschitzHilbert.rawChartSlope line 51
  11. def OAI.LipschitzHilbert.clippedChartSlope line 54
  12. theorem OAI.LipschitzHilbert.ratio_dist_bound line 57
  13. theorem OAI.LipschitzHilbert.rawChartSlope_lipschitz line 78
  14. theorem OAI.LipschitzHilbert.clippedChartSlope_lipschitz line 98
  15. theorem OAI.LipschitzHilbert.clippedChartSlope_abs line 103
  16. theorem OAI.LipschitzHilbert.chart_coordinates line 108
  17. theorem OAI.LipschitzHilbert.clippedChartSlope_eq_ratio line 120
  18. theorem OAI.LipschitzHilbert.exists_finite_direction_charts line 131