OAI/MeasureTheory/Falconer/Radial/HyperplaneFiber.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Smooth compactly supported fibers in the actual hyperplane coordinates.

  1. def OAI.Falconer.hyperplaneFiberDensity line 13
  2. theorem OAI.Falconer.hyperplaneFiberDensity_measurable line 17
  3. theorem OAI.Falconer.hyperplaneCoordinateMeasure_withDensity line 21
  4. theorem OAI.Falconer.hyperplaneFrame_line line 39
  5. theorem OAI.Falconer.hyperplaneFiberDensity_line line 50
  6. def OAI.Falconer.hyperplaneRealFiber line 60
  7. theorem OAI.Falconer.hyperplaneFiber_line_compact line 63
  8. theorem OAI.Falconer.hyperplaneRealFiber_compact line 73
  9. theorem OAI.Falconer.hyperplaneRealFiber_smooth line 83
  10. def OAI.Falconer.hyperplaneSchwartzFiber line 104
  11. theorem OAI.Falconer.hyperplaneSchwartzFiber_nonneg line 109
  12. theorem OAI.Falconer.hyperplaneSchwartzFiber_density line 114