OAI/Geometry/PrescribedPotential/MatrixHilbertCoordinates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Matrix Hilbert Coordinates.

  1. abbrev OAI.MetricSystem.Mat line 19
  2. abbrev OAI.MetricSystem.HM line 20
  3. def OAI.MetricSystem.encodeLinear line 25
  4. def OAI.MetricSystem.encode line 33
  5. lemma OAI.MetricSystem.encode_apply line 34
  6. lemma OAI.MetricSystem.decode_apply line 35
  7. def OAI.MetricSystem.rawTrace line 38
  8. lemma OAI.MetricSystem.rawTrace_add line 40
  9. lemma OAI.MetricSystem.rawTrace_smul line 42
  10. lemma OAI.MetricSystem.rawTrace_inv line 44
  11. def OAI.MetricSystem.principalLinear line 47
  12. lemma OAI.MetricSystem.principalLinear_add line 55
  13. lemma OAI.MetricSystem.principalLinear_smul line 62
  14. def OAI.MetricSystem.principalBilinear line 73
  15. lemma OAI.MetricSystem.principalBilinear_inv line 86
  16. def OAI.MetricSystem.inverseCoefficient line 90
  17. lemma OAI.MetricSystem.inverseCoefficient_smooth line 92
  18. def OAI.MetricSystem.W line 99
  19. def OAI.MetricSystem.quadraticCoefficient line 103