OAI/Analysis/LipschitzHilbert/Estimates/ChartPullback.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The orthogonal chart and product coordinates preserve the input L2 norm. The slope and endpoint factors satisfy global quantitative bounds.

  1. def OAI.LipschitzHilbert.chartCoordinateMap line 14
  2. def OAI.LipschitzHilbert.chartSchwartz line 17
  3. theorem OAI.LipschitzHilbert.chartSchwartz_apply line 20
  4. theorem OAI.LipschitzHilbert.chartCoordinateMap_measurePreserving line 23
  5. theorem OAI.LipschitzHilbert.chartSchwartz_norm line 27
  6. theorem OAI.LipschitzHilbert.chartInverse_measurePreserving line 34
  7. theorem OAI.LipschitzHilbert.chartDenominator_bounds line 39
  8. theorem OAI.LipschitzHilbert.clippedChartSlope_small_lipschitz line 46
  9. theorem OAI.LipschitzHilbert.chartDenominator_measurable line 52
  10. theorem OAI.LipschitzHilbert.shortTransform_clippedChart line 56