OAI/InformationTheory/SecretKey/Construction.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroKey.tensorPi_trace line 21
  2. lemma OAI.ZeroKey.tensorPi_trace_mul line 26
  3. lemma OAI.ZeroKey.tensorPi_commute line 30
  4. def OAI.ZeroKey.Explicit.constructionMap line 44
  5. lemma OAI.ZeroKey.Explicit.contextParity_sq line 46
  6. lemma OAI.ZeroKey.Explicit.contextEigenvalue_product line 50
  7. lemma OAI.ZeroKey.Explicit.context_shared line 60
  8. theorem OAI.ZeroKey.Explicit.magic_parity line 64
  9. lemma OAI.ZeroKey.Explicit.sum_basis line 104
  10. lemma OAI.ZeroKey.Explicit.projection_trace_mul line 107
  11. lemma OAI.ZeroKey.Explicit.projection_orthogonal line 120
  12. lemma OAI.ZeroKey.Explicit.trace_product_nonneg line 135
  13. lemma OAI.ZeroKey.Explicit.local_trace_pos_of_global line 142
  14. def OAI.ZeroKey.booleanMonomial line 171
  15. def OAI.ZeroKey.booleanDegreeSpace line 174
  16. lemma OAI.ZeroKey.booleanMonomial_mul line 178
  17. lemma OAI.ZeroKey.booleanMonomial_mem line 185
  18. lemma OAI.ZeroKey.boolean_one_mem line 189
  19. lemma OAI.ZeroKey.boolean_mul_mem line 194
  20. lemma OAI.ZeroKey.boolean_pow_mem line 212
  21. def OAI.ZeroKey.intersectionSum line 218
  22. lemma OAI.ZeroKey.intersectionSum_mem line 221
  23. lemma OAI.ZeroKey.intersectionSum_apply line 228
  24. lemma OAI.ZeroKey.boolean_biorthogonal_bound line 237
  25. lemma OAI.ZeroKey.card_booleanMonomials line 255
  26. lemma OAI.ZeroKey.modular_intersection_bound line 277
  27. lemma OAI.ZeroKey.Explicit.overlap_product line 305
  28. lemma OAI.ZeroKey.Explicit.base_no_orthogonal_bound line 313
  29. def OAI.ZeroKey.OrProduct line 357
  30. lemma OAI.ZeroKey.two_fibers_clique line 362
  31. lemma OAI.ZeroKey.rich_fiber_bound line 385
  32. def OAI.ZeroKey.Explicit.BaseOrthogonal line 457
  33. lemma OAI.ZeroKey.Explicit.base_orthogonal_symm line 459
  34. lemma OAI.ZeroKey.Explicit.base_no_two_bound line 463
  35. lemma OAI.ZeroKey.Explicit.pair_no_four_bound line 482
  36. lemma OAI.ZeroKey.Explicit.triple_no_eight_bound line 491
  37. def OAI.ZeroKey.Explicit.questionTriple line 501
  38. lemma OAI.ZeroKey.Explicit.questionTriple_apply line 511
  39. lemma OAI.ZeroKey.Explicit.overlap_zero_iff line 514
  40. lemma OAI.ZeroKey.Explicit.no_clique_image line 525
  41. theorem OAI.ZeroKey.Explicit.vector_family_bound line 544
  42. lemma OAI.ZeroKey.Explicit.vector_family_strict line 553
  43. lemma OAI.ZeroKey.Explicit.projection_orthogonal_of_question_eq line 563
  44. lemma OAI.ZeroKey.Explicit.localProjection_ordered line 573
  45. lemma OAI.ZeroKey.Explicit.clique_no_eight line 583
  46. theorem OAI.ZeroKey.Explicit.projection_clique_bound line 611
  47. lemma OAI.ZeroKey.Explicit.rawOutput_compression line 623
  48. lemma OAI.ZeroKey.Explicit.projection_idem line 641
  49. lemma OAI.ZeroKey.Explicit.rawOutput_compression_trace line 644
  50. lemma OAI.ZeroKey.Explicit.rawOutput_compression_total line 651
  51. def OAI.ZeroKey.sepOuter line 680
  52. lemma OAI.ZeroKey.normSq_sum_le_support line 686
  53. lemma OAI.ZeroKey.pure_decomposition_certificate line 710
  54. lemma OAI.ZeroKey.sqrt_column_decomposition line 762
  55. lemma OAI.ZeroKey.separable_has_pure_decomposition line 770
  56. theorem OAI.ZeroKey.separable_support_certificate line 794
  57. theorem OAI.ZeroKey.not_separable_of_support_certificate line 803
  58. lemma OAI.ZeroKey.frame_potential_rearrange line 824
  59. theorem OAI.ZeroKey.frame_potential_bound line 849
  60. lemma OAI.ZeroKey.Explicit.K_pos line 872
  61. lemma OAI.ZeroKey.Explicit.card_vectorIndex line 874
  62. theorem OAI.ZeroKey.Explicit.rawOutput_not_separable line 880
  63. lemma OAI.ZeroKey.Explicit.blockFin_transpose line 922
  64. lemma OAI.ZeroKey.Explicit.trace_transpose_left line 927
  65. lemma OAI.ZeroKey.Explicit.constructionMapFin_transpose line 931
  66. lemma OAI.ZeroKey.Explicit.constructionMapFin_ppt line 936
  67. lemma OAI.ZeroKey.Separable.smul line 945
  68. lemma OAI.ZeroKey.Separable.submatrix line 951
  69. lemma OAI.ZeroKey.Explicit.rawOutputFin_not_separable line 964
  70. lemma OAI.ZeroKey.Explicit.rhoFin_not_separable line 973
  71. lemma OAI.ZeroKey.Explicit.rhoFin_inClass line 980
  72. theorem OAI.ZeroKey.Explicit.explicit_entangled_class_state line 998