OAI/InformationTheory/SecretKey/Gap.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroKey.faithful_input_effects line 20
  2. lemma OAI.ZeroKey.traceNorm_unitary_mul_le line 39
  3. lemma OAI.ZeroKey.traceNorm_unitary_mul line 45
  4. lemma OAI.ZeroKey.traceNorm_mul_unitary_le line 52
  5. lemma OAI.ZeroKey.traceNorm_mul_unitary line 58
  6. lemma OAI.ZeroKey.traceNorm_posSemidef line 65
  7. lemma OAI.ZeroKey.re_trace_le_traceNorm line 69
  8. lemma OAI.ZeroKey.traceNorm_conjTranspose_le line 72
  9. lemma OAI.ZeroKey.traceNorm_conjTranspose line 82
  10. lemma OAI.ZeroKey.traceNorm_transpose_le line 86
  11. lemma OAI.ZeroKey.traceNorm_transpose line 92
  12. def OAI.ZeroKey.rootFidelity line 96
  13. lemma OAI.ZeroKey.polar_fidelity line 98
  14. def OAI.ZeroKey.unitSign line 120
  15. lemma OAI.ZeroKey.unitSign_square line 122
  16. lemma OAI.ZeroKey.signed_absolute line 125
  17. lemma OAI.ZeroKey.powers_stormer line 163
  18. lemma OAI.ZeroKey.fidelity_lower line 186
  19. lemma OAI.ZeroKey.traceNorm_neg line 213
  20. lemma OAI.ZeroKey.traceNorm_sub_comm line 216
  21. lemma OAI.ZeroKey.abs_re_trace_le_traceNorm line 219
  22. lemma OAI.ZeroKey.traceNorm_smul_nonneg line 227
  23. lemma OAI.ZeroKey.sqrt_transpose line 241
  24. lemma OAI.ZeroKey.rootFidelity_symm line 247
  25. lemma OAI.ZeroKey.rootFidelity_transpose line 253
  26. lemma OAI.ZeroKey.eveBlock_positive line 259
  27. lemma OAI.ZeroKey.trace_eveBlock line 265
  28. lemma OAI.ZeroKey.fidelity_eveBlock line 270
  29. lemma OAI.ZeroKey.continuous_traceNorm line 306
  30. lemma OAI.ZeroKey.measurable_traceNorm line 316
  31. lemma OAI.ZeroKey.measurable_sqrt_psd line 320
  32. lemma OAI.ZeroKey.measurable_rootFidelity line 329
  33. lemma OAI.ZeroKey.measurable_re_trace line 339
  34. lemma OAI.ZeroKey.traceNorm_sub_le_trace line 346
  35. lemma OAI.ZeroKey.traceNorm_sub_integrable line 351
  36. lemma OAI.ZeroKey.memLp_sqrt line 372
  37. lemma OAI.ZeroKey.sqrt_product_integrable line 377
  38. lemma OAI.ZeroKey.integral_sqrt_product_le line 386
  39. lemma OAI.ZeroKey.uniform_gap_arithmetic line 403
  40. lemma OAI.ZeroKey.two_term_root_cauchy line 414
  41. lemma OAI.ZeroKey.root_cross_le_sum line 429
  42. lemma OAI.ZeroKey.rootFidelity_le_sqrt_trace line 441
  43. lemma OAI.ZeroKey.rootFidelity_integrable line 450
  44. lemma OAI.ZeroKey.traceNorm_sub_triangle line 463
  45. lemma OAI.ZeroKey.trace_difference_le_norm line 468
  46. lemma OAI.ZeroKey.density_uniform_gap line 483
  47. theorem OAI.ZeroKey.class_factor_density_uniform_gap line 586
  48. lemma OAI.ZeroKey.real_trace_smul line 620
  49. def OAI.ZeroKey.BitDensity.changeMeasure line 628
  50. lemma OAI.ZeroKey.BitDensity.changeMeasure_mass line 639
  51. lemma OAI.ZeroKey.BitDensity.changeMeasure_idealBitError line 643
  52. lemma OAI.ZeroKey.eveBlock_smul_local line 656
  53. theorem OAI.ZeroKey.class_factor_gap_dominating_measure line 662
  54. lemma OAI.ZeroKey.BitProtocol.canonicalOutput_event line 713
  55. lemma OAI.ZeroKey.density_uniform_gap_ae line 735
  56. lemma OAI.ZeroKey.PositiveMatrixMeasure.integral_density line 847
  57. lemma OAI.ZeroKey.PositiveMatrixMeasure.density_eq_ae line 856
  58. lemma OAI.ZeroKey.PositiveMatrixMeasure.positiveDensity_eq_ae line 866
  59. lemma OAI.ZeroKey.PositiveMatrixMeasure.positiveDensity_trace_eq_one line 874
  60. lemma OAI.ZeroKey.PositiveMatrixMeasure.positiveDensity_integrable line 879
  61. lemma OAI.ZeroKey.PositiveMatrixMeasure.positiveDensity_integral line 884
  62. lemma OAI.ZeroKey.PositiveMatrixMeasure.positiveDensity_changeMeasure line 891
  63. lemma OAI.ZeroKey.BitDensity.idealBitError_congr line 909
  64. lemma OAI.ZeroKey.BitProtocol.canonicalOutput_ac line 958
  65. def OAI.ZeroKey.BitProtocol.outputDensity line 963
  66. lemma OAI.ZeroKey.BitProtocol.outputDensity_eq line 969
  67. def OAI.ZeroKey.BitProtocol.secretBitError line 981
  68. theorem OAI.ZeroKey.BitProtocol.uniform_gap line 988
  69. theorem OAI.ZeroKey.traceNorm_positive_tracePreserving line 1021
  70. lemma OAI.ZeroKey.traceNorm_sum_le line 1057
  71. def OAI.ZeroKey.firstBitBlocks line 1068
  72. theorem OAI.ZeroKey.firstBit_traceNorm_contracts line 1072
  73. def OAI.ZeroKey.idealKeyBlocks line 1093
  74. lemma OAI.ZeroKey.firstBit_idealKey line 1097
  75. def OAI.ZeroKey.idealBitBlocks line 1119
  76. def OAI.ZeroKey.cqBitError line 1122
  77. lemma OAI.ZeroKey.BitDensity.idealBitError_eq_cq line 1126
  78. lemma OAI.ZeroKey.idealFiniteBlocks_bit line 1143
  79. lemma OAI.ZeroKey.idealFiniteBlocks_bitSuffix line 1149
  80. theorem OAI.ZeroKey.cqDistance_firstBit_le line 1155
  81. lemma OAI.ZeroKey.idealFinite_measurable line 1204
  82. lemma OAI.ZeroKey.idealFinite_positive line 1211
  83. lemma OAI.ZeroKey.idealFinite_trace_integrable line 1218
  84. theorem OAI.ZeroKey.cqFirstBit_ideal_le line 1225
  85. lemma OAI.ZeroKey.cqDistance_nonneg line 1253
  86. lemma OAI.ZeroKey.cqDistance_triangle line 1257
  87. lemma OAI.ZeroKey.BitDensity.error_triangle line 1286
  88. theorem OAI.ZeroKey.BitDensity.gap_of_traceNorm_limit line 1296
  89. theorem OAI.ZeroKey.BitProtocol.uniform_gap_dominated line 1331