OAI/Probability/BinarySweep/MatrixBounds/TraceInterpolation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryCoordinateSweeps.TraceHolder.M line 15
  2. lemma OAI.BinaryCoordinateSweeps.TraceHolder.entry_norm_le line 17
  3. lemma OAI.BinaryCoordinateSweeps.TraceHolder.trace_norm_le line 26
  4. lemma OAI.BinaryCoordinateSweeps.TraceHolder.prod_norm_le_one line 33
  5. def OAI.BinaryCoordinateSweeps.TraceHolder.diagPower line 46
  6. lemma OAI.BinaryCoordinateSweeps.TraceHolder.diagPower_add line 49
  7. lemma OAI.BinaryCoordinateSweeps.TraceHolder.diagPower_norm_le_one line 58
  8. lemma OAI.BinaryCoordinateSweeps.TraceHolder.diagPower_imag_norm_le_one line 70
  9. lemma OAI.BinaryCoordinateSweeps.TraceHolder.diagPower_one line 78
  10. lemma OAI.BinaryCoordinateSweeps.TraceHolder.differentiable_diagPower line 89
  11. def OAI.BinaryCoordinateSweeps.TraceHolder.word line 101
  12. def OAI.BinaryCoordinateSweeps.TraceHolder.traceWord line 104
  13. lemma OAI.BinaryCoordinateSweeps.TraceHolder.word_norm_le_one line 107
  14. lemma OAI.BinaryCoordinateSweeps.TraceHolder.differentiable_word line 117
  15. lemma OAI.BinaryCoordinateSweeps.TraceHolder.differentiable_traceWord line 131
  16. def OAI.BinaryCoordinateSweeps.TraceHolder.diagReal line 146
  17. lemma OAI.BinaryCoordinateSweeps.TraceHolder.star_diagReal line 149
  18. lemma OAI.BinaryCoordinateSweeps.TraceHolder.diagReal_mul line 152
  19. lemma OAI.BinaryCoordinateSweeps.TraceHolder.gram_product line 156
  20. lemma OAI.BinaryCoordinateSweeps.TraceHolder.gram_diagonal_factor line 160
  21. theorem OAI.BinaryCoordinateSweeps.TraceHolder.exists_partial_svd line 202