OAI/Geometry/Perimeter/Regularity/FiberCrossing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPISingularHarnack.fiberPrimitive line 10
  2. theorem OAI.RPISingularHarnack.fiberPrimitive_hasDerivAt line 12
  3. theorem OAI.RPISingularHarnack.fiberPrimitive_continuous line 17
  4. theorem OAI.RPISingularHarnack.fiber_crossing_identity line 21
  5. theorem OAI.RPISingularHarnack.fiber_crossing_bound_of_order_defect line 47
  6. theorem OAI.RPISingularHarnack.fiber_order_defect_of_positive_derivative line 108
  7. theorem OAI.RPISingularHarnack.fiber_crossing_bound line 122
  8. theorem OAI.RPISingularHarnack.fiber_flux_height_identity line 132
  9. theorem OAI.RPISingularHarnack.fiber_flux_height_defect line 166