OAI/Geometry/Perimeter/Regularity/FiberCompactness.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.integral_phase_error_mul line 13
  2. theorem OAI.RPISingularHarnack.integrable_phase_error_mul line 27
  3. theorem OAI.RPISingularHarnack.cutoffPhaseError_distribution line 36
  4. theorem OAI.RPISingularHarnack.cutoffPhaseError_convolution_fderiv line 87
  5. theorem OAI.RPISingularHarnack.integral_abs_convolution_le line 130
  6. theorem OAI.RPISingularHarnack.smooth_directional_translation_lintegral_le line 144
  7. theorem OAI.RPISingularHarnack.minimizing_normal_scalar_integrable line 175
  8. theorem OAI.RPISingularHarnack.cutoffPhaseError_convolution_variation_le line 201
  9. theorem OAI.RPISingularHarnack.localizedPhaseError_integrable line 241
  10. theorem OAI.RPISingularHarnack.phase_error_cutoff_derivative_le line 252
  11. theorem OAI.RPISingularHarnack.cutoffPhaseError_convolution_height_variation line 284
  12. theorem OAI.RPISingularHarnack.translation_lintegral_le_of_mollifier_direction_bound line 323
  13. theorem OAI.RPISingularHarnack.cutoffPhaseError_horizontal_translation_le line 365