OAI/Geometry/RuledCovering/SingularField.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RuledApproximation.singular_parameter_bounds line 12
  2. lemma OAI.RuledApproximation.singularField_contDiffAt line 25
  3. lemma OAI.RuledApproximation.singularField_contDiffOn line 41
  4. lemma OAI.RuledApproximation.singularField_smul line 45
  5. lemma OAI.RuledApproximation.singularField_fderiv_smul line 60
  6. lemma OAI.RuledApproximation.singularField_level line 76
  7. lemma OAI.RuledApproximation.singularField_wall line 81
  8. def OAI.RuledApproximation.matrixCLM line 91
  9. lemma OAI.RuledApproximation.matrixCLM_apply line 95
  10. lemma OAI.RuledApproximation.hasFDerivAt_vec2 line 100
  11. lemma OAI.RuledApproximation.singularField_fderiv line 112
  12. lemma OAI.RuledApproximation.matrixCLM_trace line 150
  13. lemma OAI.RuledApproximation.matrixCLM_det line 157
  14. lemma OAI.RuledApproximation.singularField_trace_det line 164
  15. lemma OAI.RuledApproximation.singularField_hyperbolic line 171
  16. lemma OAI.RuledApproximation.singularField_scaled_hyperbolic line 189