OAI/Geometry/CylinderCovering/Singular/EdgeOneDifferential.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingularEdgeOne.labelContinuous_apply line 12
  2. lemma OAI.SingularEdgeOne.labelContinuous_symm_apply line 13
  3. lemma OAI.SingularEdgeOne.edgeField_labelMap line 16
  4. lemma OAI.SingularEdgeOne.edgeField_conjugacy line 29
  5. lemma OAI.SingularEdgeOne.edgeField_hasFDerivAt line 35
  6. lemma OAI.SingularEdgeOne.edgeField_fderiv line 50
  7. lemma OAI.SingularEdgeOne.scaled_derivative_conjugacy line 57
  8. lemma OAI.SingularEdgeOne.edgeHamiltonian_deriv_w line 69
  9. lemma OAI.SingularEdgeOne.edgeHamiltonian_deriv_l line 83
  10. lemma OAI.SingularEdgeOne.hasEigenvalue_conjugacy line 105
  11. lemma OAI.SingularEdgeOne.scaled_eigenvalue_iff line 138
  12. lemma OAI.SingularEdgeOne.edgeField_Hamiltonian line 152
  13. lemma OAI.SingularEdgeOne.labelContinuous_matrix line 159
  14. lemma OAI.SingularEdgeOne.labelContinuous_det line 165
  15. lemma OAI.SingularEdgeOne.labelMap_integral_image line 171
  16. lemma OAI.SingularEdgeOne.physicalWeight_dictionary line 181
  17. lemma OAI.SingularEdgeOne.physical_cost_dictionary line 191