OAI/Geometry/TamingCompatibility/Charts/LocalMatrixOperator.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.LocalMatrixOperator.oneVector line 19
  2. lemma OAI.TamingCompatibility.LocalMatrixOperator.oneVector_apply line 23
  3. def OAI.TamingCompatibility.LocalMatrixOperator.combine line 30
  4. lemma OAI.TamingCompatibility.LocalMatrixOperator.combine_apply line 32
  5. lemma OAI.TamingCompatibility.LocalMatrixOperator.combine_pair line 34
  6. def OAI.TamingCompatibility.LocalMatrixOperator.principal line 37
  7. def OAI.TamingCompatibility.LocalMatrixOperator.lower line 41
  8. def OAI.TamingCompatibility.LocalMatrixOperator.flatPrincipal line 44
  9. lemma OAI.TamingCompatibility.LocalMatrixOperator.flatPrincipal_sum line 48
  10. lemma OAI.TamingCompatibility.LocalMatrixOperator.covector_expansion line 56
  11. lemma OAI.TamingCompatibility.LocalMatrixOperator.operator_expansion line 66
  12. lemma OAI.TamingCompatibility.LocalMatrixOperator.principal_at_unitary_center line 104
  13. lemma OAI.TamingCompatibility.LocalMatrixOperator.principal_smooth line 120
  14. lemma OAI.TamingCompatibility.LocalMatrixOperator.lower_smooth line 134