OAI/MeasureTheory/Falconer/Geometry/AmbientChartBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Ambient symbol bounds imply the ordinary rotated chart bounds

Only derivatives of the original symbol evaluated at sphere points are used. The one-coordinate curve has a fixed, rotation-independent budget.

  1. theorem OAI.Falconer.rotatedChartCurve_derivative_scale line 16
  2. theorem OAI.Falconer.ambient_symbol_rotated_chart_budget line 33