OAI/MeasureTheory/Falconer/Angular/CapSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate support inherited from a geometric sphere cap

The two coordinate bounds are consequences of the actual cap support. They do not impose additional localization assumptions on the amplitude.

  1. theorem OAI.Falconer.chartPole_inner line 16
  2. theorem OAI.Falconer.transverse_coordinate_bounds line 21
  3. theorem OAI.Falconer.rotated_cap_coordinate_bounds line 33
  4. theorem OAI.Falconer.cap_mem_rotated_north line 52
  5. theorem OAI.Falconer.cap_amplitude_chart_support line 68
  6. theorem OAI.Falconer.cap_amplitude_chart_radius line 92