OAI/Analysis/MatrixSigning/Optimization/Coordinates.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.RationalInput.coordinates line 14
  2. def OAI.CurrentKS.RationalInput.trace line 17
  3. def OAI.CurrentKS.RationalInput.orientation line 19
  4. def OAI.CurrentKS.RationalInput.scale line 21
  5. def OAI.CurrentKS.RationalInput.indices line 23
  6. def OAI.CurrentKS.RationalInput.index line 26
  7. def OAI.CurrentKS.RationalInput.normalizedCoordinates line 28
  8. lemma OAI.CurrentKS.RationalInput.index_injective line 31
  9. lemma OAI.CurrentKS.RationalInput.index_range line 34
  10. lemma OAI.CurrentKS.RationalInput.index_trace_ne line 39
  11. lemma OAI.CurrentKS.RationalInput.indices_length_le line 42
  12. lemma OAI.CurrentKS.RationalInput.trace_cast line 49
  13. lemma OAI.CurrentKS.RationalInput.orientation_cast line 52
  14. lemma OAI.CurrentKS.RationalInput.scale_cast line 58
  15. lemma OAI.CurrentKS.RationalInput.coordinates_cast line 61
  16. lemma OAI.CurrentKS.RationalInput.decode_coordinates line 67
  17. lemma OAI.CurrentKS.RationalInput.trace_zero_iff line 72
  18. lemma OAI.CurrentKS.RationalInput.scale_pos line 77
  19. lemma OAI.CurrentKS.RationalInput.dimension_ne line 83
  20. lemma OAI.CurrentKS.RationalInput.decode_normalizedCoordinates line 92
  21. lemma OAI.CurrentKS.RationalInput.normalized_input_properties line 101