OAI/Geometry/CylinderCovering/Nilpotent/ShearC1.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RuledApproximation.NilpotentShear.field_contDiff line 11
  2. lemma OAI.RuledApproximation.NilpotentShear.field_hasFDerivAt line 16
  3. lemma OAI.RuledApproximation.NilpotentShear.field_fderiv line 22
  4. lemma OAI.RuledApproximation.NilpotentShear.field_squareZero line 28
  5. lemma OAI.RuledApproximation.NilpotentShear.field_smoothNear line 35
  6. lemma OAI.RuledApproximation.NilpotentShear.signedSquare_hasDerivAt line 40
  7. lemma OAI.RuledApproximation.NilpotentShear.signedSquare_deriv line 56
  8. lemma OAI.RuledApproximation.NilpotentShear.signedSquare_contDiff line 59
  9. lemma OAI.RuledApproximation.NilpotentShear.signedSquare_not_contDiff_two line 65
  10. lemma OAI.RuledApproximation.NilpotentShear.signedSquare_not_contDiffAt_two_zero line 76
  11. lemma OAI.RuledApproximation.NilpotentShear.signedSquareField_contDiff line 87
  12. lemma OAI.RuledApproximation.NilpotentShear.signedSquareField_squareZero line 90
  13. lemma OAI.RuledApproximation.NilpotentShear.signedSquareField_apply line 94
  14. lemma OAI.RuledApproximation.NilpotentShear.signedSquareField_not_contDiff_two line 99
  15. lemma OAI.RuledApproximation.NilpotentShear.signedSquareField_not_contDiffAt_two_zero line 109
  16. lemma OAI.RuledApproximation.NilpotentShear.signedSquareField_not_smoothNear_two line 121
  17. lemma OAI.RuledApproximation.NilpotentShear.signedSquareField_fderiv_zero line 127
  18. lemma OAI.RuledApproximation.NilpotentShear.signedSquareField_large_derivative line 131
  19. theorem OAI.RuledApproximation.NilpotentShear.field_physical_cover line 151
  20. theorem OAI.RuledApproximation.NilpotentShear.signedSquareField_physical_cover line 159
  21. theorem OAI.RuledApproximation.NilpotentShear.field_weighted_cover line 165
  22. theorem OAI.RuledApproximation.NilpotentShear.field_null_domain_cover line 182