OAI/Geometry/IsometricImmersion/Caps/EllipticCutoffEdge.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.Weighted.coordLinear_norm_le line 12
  2. def OAI.SmoothLocal.Weighted.ellipticEdgeRaw line 33
  3. def OAI.SmoothLocal.Weighted.ellipticEdgeKernel line 36
  4. def OAI.SmoothLocal.Weighted.ellipticEdgeDerivative line 39
  5. def OAI.SmoothLocal.Weighted.ellipticEdgeDerivativeConstant line 42
  6. theorem OAI.SmoothLocal.Weighted.ellipticEdgeRaw_contDiffOn line 45
  7. theorem OAI.SmoothLocal.Weighted.ellipticEdgeHalfPlane_isOpen line 50
  8. theorem OAI.SmoothLocal.Weighted.ellipticEdgeKernel_norm_le line 53
  9. theorem OAI.SmoothLocal.Weighted.ellipticEdgeRaw_partial_bound line 64
  10. theorem OAI.SmoothLocal.Weighted.ellipticEdgeDerivative_norm_le line 99
  11. theorem OAI.SmoothLocal.Weighted.ellipticEdgeKernel_hasFDerivAt_boundary line 118
  12. theorem OAI.SmoothLocal.Weighted.ellipticEdgeKernel_hasFDerivAt line 140
  13. theorem OAI.SmoothLocal.Weighted.ellipticEdgeDerivative_continuous line 158
  14. theorem OAI.SmoothLocal.Weighted.ellipticEdgeKernel_contDiff_one line 182
  15. def OAI.SmoothLocal.Weighted.ellipticWeightC1 line 188
  16. theorem OAI.SmoothLocal.Weighted.ellipticWeightC1_eq line 191
  17. theorem OAI.SmoothLocal.Weighted.ellipticWeightC1_zero line 203
  18. theorem OAI.SmoothLocal.Weighted.ellipticWeightC1_nonneg line 207
  19. theorem OAI.SmoothLocal.Weighted.ellipticWeightC1_le_distance_six line 214
  20. theorem OAI.SmoothLocal.Weighted.ellipticWeightC1_partial_eq line 223
  21. theorem OAI.SmoothLocal.Weighted.ellipticWeightC1_contDiffOn line 233