OAI/Analysis/TracialSplitting/MatrixNormalization.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentMain.matrix_norm_le_sum line 22
  2. lemma OAI.CurrentMain.matrix_norm_le_card_mul line 36
  3. lemma OAI.CurrentMain.positiveFunctional_matrix_nonneg line 59
  4. def OAI.CurrentMain.positiveFunctional_matrix line 81
  5. lemma OAI.CurrentMain.positiveFunctional_matrix_one line 97
  6. lemma OAI.CurrentMain.positiveFunctional_matrix_pos_contraction line 103
  7. def OAI.Pureness.selfAdjointFunctionalComplex line 119
  8. lemma OAI.Pureness.selfAdjointFunctionalComplex_apply line 128
  9. lemma OAI.Pureness.selfAdjointFunctional_nonneg line 133
  10. theorem OAI.Pureness.exists_normalizedPositiveState line 160
  11. def OAI.CurrentMain.rowGram line 192
  12. def OAI.CurrentMain.rowMul line 195
  13. lemma OAI.CurrentMain.rowGram_mul line 199
  14. lemma OAI.CurrentMain.rowMul_one line 212
  15. lemma OAI.CurrentMain.selfAdjoint_near_one_strictlyPositive line 222
  16. lemma OAI.CurrentMain.rowGram_isSelfAdjoint line 230
  17. lemma OAI.CurrentMain.rowMul_norm_sub_le line 237
  18. theorem OAI.CurrentMain.normalize_almost_row line 248
  19. lemma OAI.CurrentMain.state_norm_le line 326
  20. def OAI.CurrentMain.ProjectionCorner.compressPositive line 348
  21. lemma OAI.CurrentMain.ProjectionCorner.compressPositive_one line 357
  22. lemma OAI.CurrentMain.ProjectionCorner.compressPositive_self line 362
  23. lemma OAI.CurrentMain.exists_state_at_projection line 369
  24. lemma OAI.CurrentMain.state_scalar_error line 382
  25. def OAI.CurrentMain.rotateRow line 406
  26. def OAI.CurrentMain.rowPair line 408
  27. lemma OAI.CurrentMain.rowPair_rotate line 411
  28. lemma OAI.CurrentMain.rotateRow_right_support line 422
  29. lemma OAI.CurrentMain.rotateRow_norm_le line 426
  30. lemma OAI.CurrentMain.rotateRow_covariance line 435
  31. lemma OAI.CurrentMain.rowPair_rotate_error line 457
  32. def OAI.CurrentMain.scalarRowGram line 489
  33. lemma OAI.CurrentMain.scalarRowGram_posSemidef line 493
  34. lemma OAI.CurrentMain.scalarRowGram_trace_le line 503
  35. lemma OAI.CurrentMain.scalarRowGram_eigenvalue_le_one line 513