OAI/InformationTheory/SecretKey/MatrixBasics.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ZeroKey.exists_unitary_polar line 19
  2. lemma OAI.ZeroKey.re_trace_nonneg line 35
  3. lemma OAI.ZeroKey.re_trace_mul_nonneg line 38
  4. lemma OAI.ZeroKey.re_trace_star_mul line 47
  5. lemma OAI.ZeroKey.re_trace_unitary_mul_le line 53
  6. lemma OAI.ZeroKey.traceNorm_nonneg line 67
  7. lemma OAI.ZeroKey.re_trace_unitary_mul_le_traceNorm line 70
  8. lemma OAI.ZeroKey.exists_unitary_traceNorm line 79
  9. lemma OAI.ZeroKey.traceNorm_add_le line 88
  10. lemma OAI.ZeroKey.trace_re_unitary_conjugate line 95
  11. lemma OAI.ZeroKey.trace_mul_conjTranspose_eq_inner line 108
  12. lemma OAI.ZeroKey.norm_matrixVector line 113
  13. lemma OAI.ZeroKey.re_trace_mul_conjTranspose_le line 118
  14. lemma OAI.ZeroKey.traceNorm_mul_conjTranspose_le line 127
  15. lemma OAI.ZeroKey.sqrtRows_gram line 147
  16. lemma OAI.ZeroKey.traceNorm_submatrix_le line 153
  17. theorem OAI.ZeroKey.positive_block_estimate line 160
  18. def OAI.ZeroKey.InClass line 169
  19. def OAI.ZeroKey.weight line 173
  20. lemma OAI.ZeroKey.cp_positive line 176
  21. def OAI.ZeroKey.amplifyTensor line 185
  22. lemma OAI.ZeroKey.tensorMap_amplify_positive line 192
  23. lemma OAI.ZeroKey.tensorMap_global_transpose line 206
  24. lemma OAI.ZeroKey.outer_transpose_conj line 220
  25. lemma OAI.ZeroKey.tensorMap_outer_block line 225
  26. lemma OAI.ZeroKey.filtered_block_estimate line 243
  27. lemma OAI.ZeroKey.trace_sqrt_filter line 254
  28. lemma OAI.ZeroKey.sqrt_filtered_block_estimate line 258
  29. lemma OAI.ZeroKey.tensorMap_outer_block_adjoint line 271
  30. lemma OAI.ZeroKey.direct_block_bound line 280
  31. lemma OAI.ZeroKey.reversed_block_bound line 290
  32. lemma OAI.ZeroKey.trace_mul_nonneg line 304
  33. lemma OAI.ZeroKey.psd_of_quadratic_nonneg line 312
  34. lemma OAI.ZeroKey.trace_mul_outer line 326
  35. def OAI.ZeroKey.effectDual line 336
  36. lemma OAI.ZeroKey.effectDual_pairing line 339
  37. lemma OAI.ZeroKey.effectDual_positive line 354
  38. lemma OAI.ZeroKey.tensorMap_add line 364
  39. lemma OAI.ZeroKey.tensorMap_smul line 370
  40. lemma OAI.ZeroKey.tensorMap_expansion line 376
  41. lemma OAI.ZeroKey.tensorMap_effect_pairing line 394
  42. lemma OAI.ZeroKey.tensor_weight_nonneg line 409
  43. lemma OAI.ZeroKey.matrix_cfc_continuous line 422
  44. lemma OAI.ZeroKey.matrix_cfc_mul line 427
  45. lemma OAI.ZeroKey.matrix_cfc_nonneg line 431
  46. def OAI.ZeroKey.whiteningFunction line 435
  47. def OAI.ZeroKey.unwhiteningFunction line 437
  48. def OAI.ZeroKey.supportFunction line 439
  49. lemma OAI.ZeroKey.whitening_mul_unwhitening line 441
  50. lemma OAI.ZeroKey.whitening_square line 447
  51. lemma OAI.ZeroKey.whitening_of_psd line 457
  52. def OAI.ZeroKey.cutFunction line 499
  53. lemma OAI.ZeroKey.spectral_cut line 501
  54. lemma OAI.ZeroKey.commute_of_sum_projection line 543
  55. lemma OAI.ZeroKey.whitened_effects_commute line 552
  56. lemma OAI.ZeroKey.projection_cross_zero line 579
  57. lemma OAI.ZeroKey.commuting_spectral_cut line 583
  58. lemma OAI.ZeroKey.congruence_cross line 594
  59. lemma OAI.ZeroKey.congruence_diagonal line 601
  60. lemma OAI.ZeroKey.generalized_effect_split line 607
  61. def OAI.ZeroKey.qform line 645
  62. lemma OAI.ZeroKey.qform_nonneg line 648
  63. lemma OAI.ZeroKey.qform_congruence line 653
  64. lemma OAI.ZeroKey.qform_add line 659
  65. lemma OAI.ZeroKey.qform_sub line 664
  66. lemma OAI.ZeroKey.tensor_qform_eq_weight line 668
  67. lemma OAI.ZeroKey.tensor_filter_congruence line 674
  68. lemma OAI.ZeroKey.filter_qform_split line 680
  69. lemma OAI.ZeroKey.input_split_weights line 695
  70. lemma OAI.ZeroKey.outer_add_four line 752
  71. lemma OAI.ZeroKey.sqrt_mul_mono line 758
  72. theorem OAI.ZeroKey.four_effect_inequality line 762
  73. lemma OAI.ZeroKey.cp_sum line 848
  74. lemma OAI.ZeroKey.cp_comp line 860
  75. def OAI.ZeroKey.tensorLinear line 865
  76. lemma OAI.ZeroKey.cp_tensorLinear line 874
  77. lemma OAI.ZeroKey.tensorLinear_transpose line 882
  78. lemma OAI.ZeroKey.ppt_tensorLinear line 890