OAI/MeasureTheory/Falconer/Estimates/ConeSections.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Fiber volumes of the Euclidean cone over a gnomonic chart

  1. def OAI.Falconer.euclideanCons line 11
  2. theorem OAI.Falconer.euclideanCons_zero line 14
  3. theorem OAI.Falconer.euclideanCons_succ line 15
  4. theorem OAI.Falconer.euclideanCons_self line 18
  5. theorem OAI.Falconer.euclideanCons_continuous line 24
  6. theorem OAI.Falconer.euclideanCons_smul line 31
  7. theorem OAI.Falconer.gnomonicCone_section_positive line 39
  8. theorem OAI.Falconer.gnomonicCone_section_volume line 54
  9. theorem OAI.Falconer.gnomonicCone_section_nonpositive line 60
  10. theorem OAI.Falconer.gnomonicCone_volume_slices line 67