OAI/MeasureTheory/Falconer/Slicing/HyperplaneSlice.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual hyperplane slices are bounded by the measurable thin-slab majorant.

  1. theorem OAI.Falconer.lintegral_interval_rescale line 13
  2. theorem OAI.Falconer.coordinate_slab_average line 33
  3. theorem OAI.Falconer.coordinate_slice_le_slab_liminf line 82
  4. def OAI.Falconer.hyperplaneSliceEmbedding line 136
  5. theorem OAI.Falconer.hyperplane_slice_le_majorant line 140