OAI/MeasureTheory/Falconer/Radial/GnomonicAffinePlate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Affine hyperplanes in chart coordinates come from linear spherical slabs

  1. theorem OAI.Falconer.coordinateJoin_one_eq_northLift line 13
  2. theorem OAI.Falconer.normalized_affine_chart_inner_le line 17
  3. theorem OAI.Falconer.gnomonic_affine_plate_transport line 48
  4. theorem OAI.Falconer.gnomonicCoordinates_map_affine_plate line 67