OAI/MeasureTheory/Falconer/Slicing/GaussianPrunedBalls.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate ball estimates for the actual retained slice laws

  1. theorem OAI.Falconer.gaussian_pruned_point_kernel_ball line 13
  2. theorem OAI.Falconer.gaussian_pruned_direction_kernel_ball line 25
  3. theorem OAI.Falconer.slicePointCoordinates_map_ball line 38
  4. theorem OAI.Falconer.gaussian_pruned_point_coordinate_ball line 53
  5. theorem OAI.Falconer.sliceDirectionCoordinates_map_ball line 66
  6. theorem OAI.Falconer.gaussian_pruned_direction_coordinate_ball line 89