OAI/MeasureTheory/Falconer/Angular/GnomonicCap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A small spherical cap has bounded original affine coordinates

  1. theorem OAI.Falconer.northLift_zero_vector line 11
  2. theorem OAI.Falconer.northLift_zero_norm line 14
  3. theorem OAI.Falconer.gnomonicChart_zero_coe line 19
  4. theorem OAI.Falconer.inner_northLift_zero line 24
  5. theorem OAI.Falconer.gnomonic_cap_first_coordinate line 29
  6. theorem OAI.Falconer.gnomonic_cap_coordinates_norm line 38
  7. theorem OAI.Falconer.gnomonic_cap_law_bounded line 54