OAI/MeasureTheory/Falconer/Estimates/SliceAverage.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFalconer.periodic_lintegral_interval line 10
  2. theorem OAI.PlanarFalconer.periodic_lintegral_shift line 18
  3. def OAI.PlanarFalconer.sourceDirection line 28
  4. theorem OAI.PlanarFalconer.normal_eq_direction line 31
  5. theorem OAI.PlanarFalconer.continuous_sourceDirection line 37
  6. theorem OAI.PlanarFalconer.sourceDirection_periodic line 41
  7. theorem OAI.PlanarFalconer.plane_polar_lintegral line 45
  8. theorem OAI.PlanarFalconer.norm_sourceDirection line 80
  9. theorem OAI.PlanarFalconer.plane_polar_weighted_lintegral line 85
  10. theorem OAI.PlanarFalconer.normal_polar_weighted_lintegral line 102
  11. theorem OAI.PlanarFalconer.even_lintegral_real line 115
  12. theorem OAI.PlanarFalconer.even_polar_slice_average line 125
  13. def OAI.PlanarFalconer.sourceSliceEnergy line 141
  14. theorem OAI.PlanarFalconer.source_slice_average line 145
  15. theorem OAI.PlanarFalconer.source_slice_average_energy line 155
  16. theorem OAI.PlanarFalconer.measurable_sourceSliceEnergy line 161
  17. theorem OAI.PlanarFalconer.finite_slice_average_of_ball_bound line 171