OAI/InformationTheory/SecretKey/Model.lean

GitHub source file

590 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ZeroKey.exists_isometry_comp_of_norm_eq line 17
  2. lemma OAI.ZeroKey.norm_eq_of_gram_eq line 39
  3. theorem OAI.ZeroKey.exists_unitary_mul_of_gram_eq line 51
  4. def OAI.ZeroKey.traceNorm line 72
  5. def OAI.ZeroKey.matrixVector line 77
  6. abbrev OAI.ZeroKey.Mat line 81
  7. def OAI.ZeroKey.matrixUnit line 85
  8. def OAI.ZeroKey.amplify line 88
  9. def OAI.ZeroKey.CompletelyPositive line 93
  10. def OAI.ZeroKey.transposeLinear line 96
  11. def OAI.ZeroKey.PPTType line 101
  12. def OAI.ZeroKey.tensorMap line 104
  13. def OAI.ZeroKey.outer line 112
  14. def OAI.ZeroKey.Density line 117
  15. def OAI.ZeroKey.amplifyIndex line 122
  16. lemma OAI.ZeroKey.cp_amplifyIndex line 129
  17. lemma OAI.ZeroKey.matrix_sum_units line 141
  18. lemma OAI.ZeroKey.linearMap_matrix_units line 146
  19. lemma OAI.ZeroKey.linearMap_matrix_units_apply line 151
  20. lemma OAI.ZeroKey.tensorMap_apply line 156
  21. lemma OAI.ZeroKey.tensorMap_positive line 182
  22. lemma OAI.ZeroKey.outer_posSemidef line 195
  23. lemma OAI.ZeroKey.cp_of_kraus_representation line 200
  24. def OAI.ZeroKey.tensorPi line 233
  25. lemma OAI.ZeroKey.tensorPi_mul line 237
  26. lemma OAI.ZeroKey.tensorPi_one line 247
  27. lemma OAI.ZeroKey.tensorPi_star line 258
  28. lemma OAI.ZeroKey.tensorPi_projection line 263
  29. lemma OAI.ZeroKey.tensorPi_sum line 280
  30. abbrev OAI.ZeroKey.Explicit.p line 294
  31. abbrev OAI.ZeroKey.Explicit.k line 296
  32. def OAI.ZeroKey.Explicit.b line 298
  33. def OAI.ZeroKey.Explicit.Q line 300
  34. def OAI.ZeroKey.Explicit.K line 302
  35. def OAI.ZeroKey.Explicit.dimensionFunction line 304
  36. lemma OAI.ZeroKey.Explicit.dimensionFunction_eq line 306
  37. def OAI.ZeroKey.Explicit.D line 308
  38. lemma OAI.ZeroKey.Explicit.D_eq line 310
  39. def OAI.ZeroKey.Explicit.outputDimensionFunction line 314
  40. lemma OAI.ZeroKey.Explicit.outputDimensionFunction_eq line 316
  41. def OAI.ZeroKey.Explicit.m line 318
  42. lemma OAI.ZeroKey.Explicit.m_eq line 320
  43. def OAI.ZeroKey.Explicit.Base line 324
  44. instance OAI.ZeroKey.Explicit.(instance at line 326) line 326
  45. instance OAI.ZeroKey.Explicit.(instance at line 328) line 328
  46. instance OAI.ZeroKey.Explicit.(instance at line 330) line 330
  47. instance OAI.ZeroKey.Explicit.(instance at line 332) line 332
  48. def OAI.ZeroKey.Explicit.Question line 337
  49. instance OAI.ZeroKey.Explicit.(instance at line 339) line 339
  50. instance OAI.ZeroKey.Explicit.(instance at line 341) line 341
  51. instance OAI.ZeroKey.Explicit.(instance at line 343) line 343
  52. instance OAI.ZeroKey.Explicit.(instance at line 345) line 345
  53. def OAI.ZeroKey.Explicit.baseVector line 347
  54. def OAI.ZeroKey.Explicit.vector line 350
  55. def OAI.ZeroKey.Explicit.overlap line 353
  56. def OAI.ZeroKey.Explicit.EightSet line 355
  57. instance OAI.ZeroKey.Explicit.(instance at line 357) line 357
  58. instance OAI.ZeroKey.Explicit.(instance at line 359) line 359
  59. instance OAI.ZeroKey.Explicit.(instance at line 361) line 361
  60. instance OAI.ZeroKey.Explicit.(instance at line 363) line 363
  61. def OAI.ZeroKey.Explicit.PairwiseOrthogonal line 369
  62. abbrev OAI.ZeroKey.Explicit.Sign line 372
  63. def OAI.ZeroKey.Explicit.signValue line 374
  64. abbrev OAI.ZeroKey.Explicit.Outcome line 376
  65. abbrev OAI.ZeroKey.Explicit.LocalBasis line 378
  66. def OAI.ZeroKey.Explicit.pauliX line 380
  67. def OAI.ZeroKey.Explicit.pauliY line 382
  68. def OAI.ZeroKey.Explicit.pauliZ line 384
  69. def OAI.ZeroKey.Explicit.tensor₂ line 386
  70. def OAI.ZeroKey.Explicit.observable line 389
  71. def OAI.ZeroKey.Explicit.contextObservable line 400
  72. def OAI.ZeroKey.Explicit.contextProjection line 404
  73. def OAI.ZeroKey.Explicit.trivialProjection line 408
  74. def OAI.ZeroKey.Explicit.localProjection line 411
  75. def OAI.ZeroKey.Explicit.Basis line 424
  76. instance OAI.ZeroKey.Explicit.(instance at line 426) line 426
  77. instance OAI.ZeroKey.Explicit.(instance at line 428) line 428
  78. instance OAI.ZeroKey.Explicit.(instance at line 430) line 430
  79. instance OAI.ZeroKey.Explicit.(instance at line 432) line 432
  80. def OAI.ZeroKey.Explicit.OutcomeString line 434
  81. instance OAI.ZeroKey.Explicit.(instance at line 436) line 436
  82. instance OAI.ZeroKey.Explicit.(instance at line 438) line 438
  83. instance OAI.ZeroKey.Explicit.(instance at line 440) line 440
  84. instance OAI.ZeroKey.Explicit.(instance at line 442) line 442
  85. def OAI.ZeroKey.Explicit.Label line 444
  86. instance OAI.ZeroKey.Explicit.(instance at line 446) line 446
  87. instance OAI.ZeroKey.Explicit.(instance at line 448) line 448
  88. instance OAI.ZeroKey.Explicit.(instance at line 450) line 450
  89. instance OAI.ZeroKey.Explicit.(instance at line 452) line 452
  90. def OAI.ZeroKey.Explicit.projection line 454
  91. def OAI.ZeroKey.Explicit.block line 457
  92. def OAI.ZeroKey.Explicit.traceBlockMap line 462
  93. def OAI.ZeroKey.Explicit.rawOutput line 475
  94. def OAI.ZeroKey.Explicit.rho line 478
  95. lemma OAI.ZeroKey.Explicit.tensor₂_apply line 481
  96. lemma OAI.ZeroKey.Explicit.sum_localBasis line 484
  97. lemma OAI.ZeroKey.Explicit.signValue_sq line 489
  98. lemma OAI.ZeroKey.Explicit.signValue_conj line 492
  99. lemma OAI.ZeroKey.Explicit.localBasis_one_apply line 495
  100. lemma OAI.ZeroKey.Explicit.context_hermitian line 499
  101. lemma OAI.ZeroKey.Explicit.context_real line 513
  102. lemma OAI.ZeroKey.Explicit.context_involution line 525
  103. lemma OAI.ZeroKey.Explicit.context_commute line 539
  104. def OAI.ZeroKey.Explicit.contextParity line 553
  105. lemma OAI.ZeroKey.Explicit.context_third line 555
  106. def OAI.ZeroKey.Explicit.spectralSign line 568
  107. lemma OAI.ZeroKey.Explicit.sign_eigen_aux line 571
  108. lemma OAI.ZeroKey.Explicit.spectralSign_projection line 577
  109. lemma OAI.ZeroKey.Explicit.spectralSign_commute line 591
  110. lemma OAI.ZeroKey.Explicit.contextProjection_factor line 597
  111. lemma OAI.ZeroKey.Explicit.contextProjection_projection line 603
  112. lemma OAI.ZeroKey.Explicit.contextProjection_real line 610
  113. lemma OAI.ZeroKey.Explicit.contextParity_conj line 617
  114. def OAI.ZeroKey.Explicit.contextEigenvalue line 621
  115. lemma OAI.ZeroKey.Explicit.context_eigen_first line 625
  116. lemma OAI.ZeroKey.Explicit.context_eigen_second line 632
  117. lemma OAI.ZeroKey.Explicit.context_eigen line 643
  118. lemma OAI.ZeroKey.Explicit.contextEigenvalue_conj line 657
  119. lemma OAI.ZeroKey.Explicit.context_eigen_right line 661
  120. lemma OAI.ZeroKey.Explicit.spectralSign_sum line 668
  121. lemma OAI.ZeroKey.Explicit.contextProjection_sum line 674
  122. lemma OAI.ZeroKey.Explicit.eigenvalues_agree line 683
  123. lemma OAI.ZeroKey.Explicit.signValue_injective line 690
  124. lemma OAI.ZeroKey.Explicit.contextProjection_orthogonal line 694
  125. lemma OAI.ZeroKey.Explicit.trivialProjection_projection line 705
  126. lemma OAI.ZeroKey.Explicit.trivialProjection_sum line 709
  127. lemma OAI.ZeroKey.Explicit.trivialProjection_orthogonal line 717
  128. lemma OAI.ZeroKey.Explicit.localProjection_type line 724
  129. lemma OAI.ZeroKey.Explicit.localProjection_projection line 738
  130. lemma OAI.ZeroKey.Explicit.localProjection_real line 744
  131. lemma OAI.ZeroKey.Explicit.localProjection_sum line 752
  132. lemma OAI.ZeroKey.Explicit.localProjection_orthogonal line 758
  133. lemma OAI.ZeroKey.Explicit.projection_tensor line 764
  134. lemma OAI.ZeroKey.Explicit.projection_projection line 768
  135. lemma OAI.ZeroKey.Explicit.projection_real line 780
  136. lemma OAI.ZeroKey.Explicit.projection_sum line 786
  137. lemma OAI.ZeroKey.Explicit.projection_mul_apply line 801
  138. lemma OAI.ZeroKey.Explicit.trivialProjection_commute line 812
  139. lemma OAI.ZeroKey.Explicit.localProjection_self_commute line 817
  140. lemma OAI.ZeroKey.Explicit.localProjection_trivial_of_not_orthogonal line 825
  141. lemma OAI.ZeroKey.Explicit.localProjection_trivial_of_not_mem line 830
  142. lemma OAI.ZeroKey.Explicit.localProjection_commute line 835
  143. lemma OAI.ZeroKey.Explicit.projection_commute line 849
  144. lemma OAI.ZeroKey.Explicit.card_subsets_containing line 860
  145. lemma OAI.ZeroKey.Explicit.card_base line 874
  146. lemma OAI.ZeroKey.Explicit.card_question line 883
  147. lemma OAI.ZeroKey.Explicit.signed_overlap line 891
  148. lemma OAI.ZeroKey.Explicit.base_inner line 905
  149. lemma OAI.ZeroKey.Explicit.base_unit line 914
  150. lemma OAI.ZeroKey.Explicit.vector_unit line 918
  151. def OAI.ZeroKey.Explicit.a₀ line 925
  152. lemma OAI.ZeroKey.Explicit.choose_mono_small line 929
  153. lemma OAI.ZeroKey.Explicit.a₀_upper line 936
  154. lemma OAI.ZeroKey.Explicit.binomial_term_le line 945
  155. lemma OAI.ZeroKey.Explicit.choose_upper line 951
  156. lemma OAI.ZeroKey.Explicit.double_b line 963
  157. lemma OAI.ZeroKey.Explicit.b_lower line 975
  158. lemma OAI.ZeroKey.Explicit.strict_parameter_bound line 982
  159. lemma OAI.ZeroKey.Explicit.b_pos line 1002
  160. lemma OAI.ZeroKey.Explicit.card_subsets line 1008
  161. lemma OAI.ZeroKey.Explicit.card_eightSet line 1016
  162. lemma OAI.ZeroKey.Explicit.card_basis_aux line 1020
  163. lemma OAI.ZeroKey.Explicit.card_localBasis line 1024
  164. lemma OAI.ZeroKey.Explicit.card_basis line 1028
  165. lemma OAI.ZeroKey.Explicit.card_outcomeString line 1031
  166. lemma OAI.ZeroKey.Explicit.card_label line 1034
  167. def OAI.ZeroKey.Explicit.basisOrder line 1039
  168. def OAI.ZeroKey.Explicit.labelOrder line 1041
  169. def OAI.ZeroKey.Explicit.rhoFin line 1105
  170. lemma OAI.ZeroKey.Explicit.overlap_symm line 1108
  171. lemma OAI.ZeroKey.Explicit.projection_transpose line 1112
  172. lemma OAI.ZeroKey.Explicit.block_swap line 1118
  173. lemma OAI.ZeroKey.Explicit.block_transpose line 1125
  174. lemma OAI.ZeroKey.Explicit.block_diag line 1132
  175. lemma OAI.ZeroKey.Explicit.rawOutput_trace line 1136
  176. lemma OAI.ZeroKey.Explicit.rawOutput_crossed_diagonal line 1141
  177. def OAI.ZeroKey.Explicit.makeLabel line 1145
  178. lemma OAI.ZeroKey.Explicit.projection_sum_makeLabel line 1147
  179. lemma OAI.ZeroKey.Explicit.sum_label line 1151
  180. lemma OAI.ZeroKey.Explicit.sum_projection_pair_trace line 1156
  181. lemma OAI.ZeroKey.Explicit.rawOutput_trace_total line 1166
  182. def OAI.ZeroKey.Separable line 1186
  183. lemma OAI.ZeroKey.Explicit.Q_pos line 1195
  184. lemma OAI.ZeroKey.Explicit.D_pos line 1197
  185. def OAI.ZeroKey.projectionKraus line 1211
  186. lemma OAI.ZeroKey.projectionKraus_coeff line 1215
  187. lemma OAI.ZeroKey.projectionKraus_formula line 1230
  188. def OAI.ZeroKey.Explicit.questionFin line 1256
  189. def OAI.ZeroKey.Explicit.projectionFin line 1258
  190. def OAI.ZeroKey.Explicit.blockFin line 1260
  191. def OAI.ZeroKey.Explicit.constructionMapFin line 1262
  192. lemma OAI.ZeroKey.Explicit.projectionFin_hermitian line 1264
  193. lemma OAI.ZeroKey.Explicit.blockFin_swap line 1268
  194. lemma OAI.ZeroKey.Explicit.blockFin_formula line 1272
  195. lemma OAI.ZeroKey.Explicit.constructionMapFin_kraus line 1281
  196. lemma OAI.ZeroKey.Explicit.constructionMapFin_cp line 1295
  197. lemma OAI.ZeroKey.Explicit.constructionMapFin_unit line 1298
  198. def OAI.ZeroKey.Explicit.omegaVector line 1303
  199. def OAI.ZeroKey.Explicit.rawOutputFin line 1305
  200. lemma OAI.ZeroKey.Explicit.rawOutputFin_tensor line 1308
  201. lemma OAI.ZeroKey.Explicit.rawOutputFin_psd line 1324
  202. lemma OAI.ZeroKey.Explicit.rawOutputFin_trace line 1328
  203. lemma OAI.ZeroKey.Explicit.rhoFin_eq line 1334
  204. lemma OAI.ZeroKey.Explicit.symbolic_normalization_ne_zero line 1336
  205. lemma OAI.ZeroKey.Explicit.normalization_ne_zero line 1340
  206. lemma OAI.ZeroKey.Explicit.rhoFin_density line 1343
  207. abbrev OAI.UnrestrictedQuantum.ReferenceFunctional line 1368
  208. def OAI.UnrestrictedQuantum.PositiveFunctional line 1371
  209. structure OAI.UnrestrictedQuantum.ObservableInstrument line 1376
  210. structure OAI.UnrestrictedQuantum.InstrumentRun line 1388
  211. theorem OAI.UnrestrictedQuantum.InstrumentRun.reference_mean line 1403
  212. theorem OAI.ZeroKey.sample_instrument_kernel line 1424
  213. abbrev OAI.ZeroKey.UniformTape line 1444
  214. def OAI.ZeroKey.uniformTapeLaw line 1446
  215. instance OAI.ZeroKey.(instance at line 1449) line 1449
  216. lemma OAI.ZeroKey.indicator_one_mul line 1466
  217. lemma OAI.ZeroKey.indicator_inter_one line 1471
  218. lemma OAI.ZeroKey.condIndep_condExp_right line 1477
  219. lemma OAI.ZeroKey.condIndep_local_refinement line 1512
  220. def OAI.ZeroKey.recordInterFamily line 1553
  221. lemma OAI.ZeroKey.recordInterFamily_pi line 1556
  222. lemma OAI.ZeroKey.recordInterFamily_generate line 1563
  223. lemma OAI.ZeroKey.condIndep_join_public_right line 1578
  224. lemma OAI.ZeroKey.condIndep_local_message line 1621
  225. lemma OAI.ZeroKey.condFactor_full_transcript line 1635
  226. lemma OAI.ZeroKey.condIndep_full_transcript line 1646
  227. lemma OAI.ZeroKey.indep_condIndep_bot line 1668
  228. structure OAI.ZeroKey.LocalTapeProgram line 1683
  229. def OAI.ZeroKey.LocalTapeProgram.publicPrefix line 1698
  230. structure OAI.ZeroKey.LocalOutcomeSampler line 1711
  231. def OAI.ZeroKey.LocalOutcomeSampler.privatePrefix line 1729
  232. def OAI.ZeroKey.LocalOutcomeSampler.extractPrivate line 1738
  233. def OAI.ZeroKey.LocalOutcomeSampler.publicFrom line 1741
  234. instance OAI.ZeroKey.matrixMeasurableSpace line 1763
  235. instance OAI.ZeroKey.matrixBorelSpace line 1769
  236. structure OAI.ZeroKey.PositiveMatrixMeasure line 1778
  237. def OAI.ZeroKey.PositiveMatrixMeasure.value line 1784
  238. def OAI.ZeroKey.PositiveMatrixMeasure.density line 1786
  239. lemma OAI.ZeroKey.PositiveMatrixMeasure.measurable_density line 1790
  240. lemma OAI.ZeroKey.PositiveMatrixMeasure.integrable_entry line 1806
  241. lemma OAI.ZeroKey.PositiveMatrixMeasure.entry_absolutelyContinuous line 1810
  242. lemma OAI.ZeroKey.PositiveMatrixMeasure.integral_density_entry line 1819
  243. lemma OAI.ZeroKey.ae_complex_nonneg_of_integral_nonneg line 1841
  244. def OAI.ZeroKey.quadraticValue line 1859
  245. lemma OAI.ZeroKey.quadraticValue_eq line 1863
  246. lemma OAI.ZeroKey.integrable_quadraticValue line 1868
  247. lemma OAI.ZeroKey.integral_quadraticValue line 1876
  248. lemma OAI.ZeroKey.density_posSemidef_ae line 1887
  249. lemma OAI.ZeroKey.psd_entry_norm_le_trace line 1934
  250. lemma OAI.ZeroKey.uniformIntegrable_of_ae_norm_le_one line 1962
  251. lemma OAI.ZeroKey.bounded_martingale_limit line 1980
  252. lemma OAI.ZeroKey.integrable_matrix_of_entries line 1999
  253. lemma OAI.ZeroKey.integral_matrix_entry line 2007
  254. def OAI.ZeroKey.positiveMatrixMeasureOfDensity line 2012
  255. lemma OAI.ZeroKey.positiveMatrixMeasureOfDensity_value line 2023
  256. def OAI.ZeroKey.keepReference line 2045
  257. def OAI.ZeroKey.referenceFilter line 2048
  258. lemma OAI.ZeroKey.referenceFilter_apply line 2053
  259. lemma OAI.ZeroKey.keepReference_filter line 2061
  260. def OAI.ZeroKey.vectorize line 2071
  261. lemma OAI.ZeroKey.keepReference_vectorize line 2074
  262. lemma OAI.ZeroKey.referenceFilter_vectorize line 2081
  263. def OAI.ZeroKey.localProbe line 2093
  264. def OAI.ZeroKey.canonicalPurification line 2096
  265. def OAI.ZeroKey.preparationFilter line 2098
  266. lemma OAI.ZeroKey.preparation_filter_identity line 2101
  267. lemma OAI.ZeroKey.canonical_reference line 2111
  268. def OAI.ZeroKey.PositiveMatrixMeasure.traceSigned line 2130
  269. lemma OAI.ZeroKey.PositiveMatrixMeasure.traceSigned_apply line 2134
  270. lemma OAI.ZeroKey.PositiveMatrixMeasure.traceSigned_nonneg line 2139
  271. def OAI.ZeroKey.PositiveMatrixMeasure.traceMeasure line 2148
  272. instance OAI.ZeroKey.PositiveMatrixMeasure.traceMeasure_finite line 2162
  273. lemma OAI.ZeroKey.PositiveMatrixMeasure.integrable_trace_density line 2166
  274. lemma OAI.ZeroKey.PositiveMatrixMeasure.integral_trace_density line 2170
  275. def OAI.ZeroKey.PositiveMatrixMeasure.filter line 2181
  276. lemma OAI.ZeroKey.PositiveMatrixMeasure.filter_value line 2201
  277. def OAI.ZeroKey.PositiveMatrixMeasure.pushforward line 2224
  278. lemma OAI.ZeroKey.PositiveMatrixMeasure.pushforward_value line 2233
  279. def OAI.ZeroKey.historyPrefix line 2250
  280. lemma OAI.ZeroKey.measurable_historyPrefix line 2252
  281. def OAI.ZeroKey.historyFiltration line 2256
  282. lemma OAI.ZeroKey.historyPrefix_adapted line 2269
  283. lemma OAI.ZeroKey.historyFiltration_generates line 2273
  284. lemma OAI.ZeroKey.density_entry_bound line 2291
  285. lemma OAI.ZeroKey.integrable_density_entry line 2299
  286. lemma OAI.ZeroKey.reference_history_step_integral line 2318
  287. lemma OAI.ZeroKey.reference_history_integral line 2374
  288. lemma OAI.ZeroKey.reference_history_measurable line 2386
  289. lemma OAI.ZeroKey.reference_history_integrable line 2391
  290. lemma OAI.ZeroKey.reference_history_martingale_re line 2398
  291. lemma OAI.ZeroKey.reference_history_martingale_im line 2415
  292. theorem OAI.ZeroKey.local_reference_limit line 2443
  293. abbrev OAI.UnrestrictedQuantum.LocalHistory line 2557
  294. def OAI.UnrestrictedQuantum.localActive line 2562
  295. def OAI.UnrestrictedQuantum.localPassive line 2568
  296. structure OAI.UnrestrictedQuantum.LocalObservableExecution line 2581
  297. def OAI.UnrestrictedQuantum.LocalObservableExecution.reference line 2602
  298. lemma OAI.UnrestrictedQuantum.LocalObservableExecution.reference_density line 2605
  299. lemma OAI.UnrestrictedQuantum.LocalObservableExecution.reference_measurable line 2610
  300. lemma OAI.UnrestrictedQuantum.LocalObservableExecution.active_mean line 2612
  301. lemma OAI.UnrestrictedQuantum.LocalObservableExecution.passive_reference line 2625
  302. theorem OAI.ZeroKey.condIndep_adaptive_public_message line 2641
  303. theorem OAI.ZeroKey.adaptive_tapes_given_full_transcript line 2708
  304. structure OAI.ZeroKey.AdaptiveTapeProgram line 2737
  305. def OAI.ZeroKey.AdaptiveTapeProgram.publicPrefix line 2753
  306. def OAI.ZeroKey.AdaptiveTapeProgram.message line 2758
  307. lemma OAI.ZeroKey.AdaptiveTapeProgram.prefix_succ line 2761
  308. lemma OAI.ZeroKey.AdaptiveTapeProgram.measurable_prefix line 2764
  309. lemma OAI.ZeroKey.AdaptiveTapeProgram.measurable_message line 2778
  310. abbrev OAI.ZeroKey.AdaptiveTapeProgram.field line 2783
  311. lemma OAI.ZeroKey.AdaptiveTapeProgram.field_le line 2786
  312. lemma OAI.ZeroKey.AdaptiveTapeProgram.field_mono line 2788
  313. def OAI.ZeroKey.AdaptiveTapeProgram.filtration line 2800
  314. lemma OAI.ZeroKey.AdaptiveTapeProgram.field_zero line 2805
  315. lemma OAI.ZeroKey.AdaptiveTapeProgram.field_succ line 2808
  316. theorem OAI.ZeroKey.AdaptiveTapeProgram.tapes_conditionally_independent line 2828
  317. def OAI.ZeroKey.AdaptiveTapeProgram.record line 2854
  318. lemma OAI.ZeroKey.AdaptiveTapeProgram.measurable_record line 2856
  319. lemma OAI.ZeroKey.AdaptiveTapeProgram.prefix_eq_record line 2859
  320. lemma OAI.ZeroKey.AdaptiveTapeProgram.full_record_field line 2868
  321. theorem OAI.ZeroKey.AdaptiveTapeProgram.final_records_conditionally_independent line 2889
  322. def OAI.ZeroKey.noiseTapeLaw line 2929
  323. instance OAI.ZeroKey.noiseTapeLaw_probability line 2931
  324. lemma OAI.ZeroKey.noise_prefix_fresh_independent line 2935
  325. lemma OAI.ZeroKey.noise_tape_eval line 2947
  326. structure OAI.ZeroKey.NoiseSampler line 2952
  327. def OAI.ZeroKey.NoiseSampler.finiteHistory line 2964
  328. lemma OAI.ZeroKey.NoiseSampler.measurable_finiteHistory line 2969
  329. def OAI.ZeroKey.NoiseSampler.history line 2982
  330. lemma OAI.ZeroKey.NoiseSampler.measurable_prefix line 2985
  331. lemma OAI.ZeroKey.NoiseSampler.prefix_succ line 2988
  332. lemma OAI.ZeroKey.NoiseSampler.prefix_fresh_independent line 2991
  333. lemma OAI.ZeroKey.NoiseSampler.prefix_fresh_law line 2995
  334. theorem OAI.ZeroKey.NoiseSampler.prefix_law_succ line 3002
  335. def OAI.ZeroKey.NoiseSampler.record line 3035
  336. lemma OAI.ZeroKey.NoiseSampler.measurable_record line 3037
  337. lemma OAI.ZeroKey.NoiseSampler.prefix_eq_record line 3041
  338. theorem OAI.ZeroKey.NoiseSampler.finite_law_unique line 3051
  339. theorem OAI.ZeroKey.NoiseSampler.record_law_unique line 3071
  340. structure OAI.ZeroKey.AdaptiveOutcomeSampler line 3105
  341. def OAI.ZeroKey.AdaptiveOutcomeSampler.privatePrefix line 3126
  342. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_privatePrefix line 3135
  343. def OAI.ZeroKey.AdaptiveOutcomeSampler.tapeProgram line 3158
  344. def OAI.ZeroKey.AdaptiveOutcomeSampler.replay line 3174
  345. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_snoc line 3186
  346. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_replay line 3196
  347. def OAI.ZeroKey.AdaptiveOutcomeSampler.extractPrivate line 3210
  348. def OAI.ZeroKey.AdaptiveOutcomeSampler.publicFrom line 3213
  349. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_extractPrivate line 3215
  350. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_publicFrom line 3220
  351. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.extractPrivate_snoc line 3222
  352. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.publicFrom_snoc line 3228
  353. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.privatePrefix_snoc line 3235
  354. def OAI.ZeroKey.AdaptiveOutcomeSampler.causalStep line 3243

    Source documentation

    The sampled outcome history, without a bundled measurability certificate.

    def causalStep (n : ℕ) (pair : (Fin n → O) × (I × I)) : O :=
…
  355. def OAI.ZeroKey.AdaptiveOutcomeSampler.causalHistory line 3248
  356. def OAI.ZeroKey.AdaptiveOutcomeSampler.causalRecord line 3253
  357. def OAI.ZeroKey.AdaptiveOutcomeSampler.causal line 3256
  358. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.causalRecord_eq line 3267
  359. def OAI.ZeroKey.AdaptiveOutcomeSampler.pairedTape line 3281
  360. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_pairedTape line 3283
  361. theorem OAI.ZeroKey.AdaptiveOutcomeSampler.replay_matches line 3285
  362. def OAI.ZeroKey.AdaptiveOutcomeSampler.instrumentKernel line 3325
  363. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.instrumentKernel_apply line 3336
  364. instance OAI.ZeroKey.AdaptiveOutcomeSampler.instrumentKernel_markov line 3346
  365. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.causal_step_law line 3353
  366. def OAI.ZeroKey.AdaptiveQuantum.globalLocalReferenceA line 3403
  367. def OAI.ZeroKey.AdaptiveQuantum.globalLocalReferenceB line 3406
  368. lemma OAI.ZeroKey.AdaptiveQuantum.globalLocalReferenceA_measurable line 3410
  369. lemma OAI.ZeroKey.AdaptiveQuantum.globalLocalReferenceB_measurable line 3416
  370. lemma OAI.ZeroKey.AdaptiveQuantum.globalLocalReferenceA_mean line 3422
  371. lemma OAI.ZeroKey.AdaptiveQuantum.globalLocalReferenceB_mean line 3442
  372. def OAI.ZeroKey.AdaptiveQuantum.jointReference line 3461
  373. lemma OAI.ZeroKey.AdaptiveQuantum.jointReference_density line 3465
  374. lemma OAI.ZeroKey.AdaptiveQuantum.jointReference_measurable line 3471
  375. lemma OAI.ZeroKey.AdaptiveQuantum.jointReference_mean line 3485
  376. theorem OAI.ZeroKey.paired_tapes_law line 3523
  377. theorem OAI.ZeroKey.condIndepFun_of_joint_law line 3562
  378. def OAI.ZeroKey.AdaptiveOutcomeSampler.privateRecord line 3611
  379. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_privateRecord line 3614
  380. theorem OAI.ZeroKey.AdaptiveOutcomeSampler.final_records_independent line 3621
  381. def OAI.ZeroKey.AdaptiveOutcomeSampler.outcomeRecord line 3636
  382. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_outcomeRecord line 3639
  383. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.outcomeRecord_law line 3642
  384. def OAI.ZeroKey.AdaptiveOutcomeSampler.publicRecord line 3656
  385. def OAI.ZeroKey.AdaptiveOutcomeSampler.localRecord line 3659
  386. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_publicRecord line 3662
  387. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.measurable_localRecord line 3667
  388. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.publicRecord_replay line 3672
  389. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.localRecord_replay line 3684
  390. theorem OAI.ZeroKey.AdaptiveOutcomeSampler.full_readout_law line 3701
  391. theorem OAI.ZeroKey.AdaptiveOutcomeSampler.actual_records_independent line 3732
  392. lemma OAI.ZeroKey.continuous_matrix_kronecker line 3774
  393. lemma OAI.ZeroKey.measurable_matrix_kronecker line 3785
  394. lemma OAI.ZeroKey.density_kronecker line 3792
  395. theorem OAI.ZeroKey.local_product_reference_extension line 3802
  396. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.publicFrom_eq_record line 3863
  397. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.extractPrivate_eq_record line 3873
  398. abbrev OAI.ZeroKey.AdaptiveOutcomeSampler.localField line 3883
  399. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.localField_le line 3886
  400. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.local_history_measurable line 3889
  401. lemma OAI.ZeroKey.AdaptiveOutcomeSampler.localFields_independent line 3905
  402. theorem OAI.ZeroKey.AdaptiveQuantum.full_reference_extension line 3957
  403. lemma OAI.ZeroKey.condIndepFun_ae_indep_complex line 4012
  404. lemma OAI.ZeroKey.condIndepFun_kernel_integral_mul line 4025
  405. def OAI.ZeroKey.publicMatrix line 4045
  406. lemma OAI.ZeroKey.publicMatrix_measurable line 4050
  407. lemma OAI.ZeroKey.publicMatrix_entry line 4054
  408. theorem OAI.ZeroKey.condIndep_publicMatrix_kronecker line 4059
  409. def OAI.ZeroKey.Subdensity line 4103
  410. lemma OAI.ZeroKey.subdensity_zero line 4106
  411. lemma OAI.ZeroKey.subdensity_kronecker line 4110
  412. lemma OAI.ZeroKey.integrable_subdensity line 4120
  413. lemma OAI.ZeroKey.integral_subdensity line 4132
  414. lemma OAI.ZeroKey.measurable_positive_factor line 4150
  415. theorem OAI.ZeroKey.terminal_public_factors line 4183
  416. lemma OAI.ZeroKey.PositiveMatrixMeasure.ext_on_generating_piSystem line 4231
  417. lemma OAI.ZeroKey.PositiveMatrixMeasure.ext_on_filtration line 4245
  418. def OAI.UnrestrictedQuantum.bitReference line 4283
  419. lemma OAI.UnrestrictedQuantum.bitReference_positive line 4286
  420. lemma OAI.UnrestrictedQuantum.bitReference_entry line 4291
  421. theorem OAI.UnrestrictedQuantum.bitReference_sum line 4296
  422. lemma OAI.ZeroKey.density_subdensity line 4325
  423. theorem OAI.ZeroKey.reference_density_unique_on_filtration line 4328
  424. structure OAI.UnrestrictedQuantum.IncomingObservableProcess line 4372
  425. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.reference_density line 4385
  426. structure OAI.UnrestrictedQuantum.IncomingObservableProcess.BitReadout line 4388
  427. def OAI.UnrestrictedQuantum.IncomingObservableProcess.BitReadout.value line 4400
  428. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.BitReadout.positive line 4402
  429. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.BitReadout.sum line 4405
  430. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.BitReadout.subdensity line 4408
  431. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.BitReadout.measurable line 4418
  432. lemma OAI.ZeroKey.setIntegral_publicMatrix line 4443
  433. lemma OAI.ZeroKey.public_factor_event line 4451
  434. theorem OAI.ZeroKey.AdaptiveQuantum.incoming_joint_reference_consistency line 4506
  435. theorem OAI.ZeroKey.AdaptiveQuantum.genuine_terminal_public_factors line 4534
  436. theorem OAI.ZeroKey.AdaptiveQuantum.terminal_reference_total line 4591
  437. theorem OAI.ZeroKey.AdaptiveQuantum.terminal_public_normalization line 4619
  438. lemma OAI.ZeroKey.localProbe_reference line 4654
  439. lemma OAI.ZeroKey.localProbe_reference_product line 4667
  440. structure OAI.ZeroKey.Discussion line 4687
  441. def OAI.ZeroKey.Discussion.sampler line 4708
  442. lemma OAI.ZeroKey.Discussion.sampler_law line 4738
  443. def OAI.ZeroKey.Discussion.probeLaw line 4747
  444. instance OAI.ZeroKey.Discussion.probeLaw_probability line 4750
  445. lemma OAI.ZeroKey.Discussion.probeLaw_prefix line 4753
  446. def OAI.ZeroKey.Discussion.transcriptLaw line 4764
  447. instance OAI.ZeroKey.Discussion.transcriptLaw_probability line 4766
  448. lemma OAI.ZeroKey.preparationFilter_product line 4783
  449. def OAI.ZeroKey.eveBlock line 4816
  450. structure OAI.ZeroKey.BitDensity line 4829
  451. def OAI.ZeroKey.BitDensity.mass line 4839
  452. def OAI.ZeroKey.BitDensity.idealBitError line 4842
  453. def OAI.ZeroKey.matrixFilterLinear line 4863
  454. lemma OAI.ZeroKey.integral_filter line 4868
  455. lemma OAI.ZeroKey.integrable_filter line 4873
  456. lemma OAI.ZeroKey.integral_realTrace line 4877
  457. lemma OAI.ZeroKey.preparationFilter_probe_reference line 4884
  458. lemma OAI.ZeroKey.public_product_integrable line 4904
  459. def OAI.ZeroKey.filteredPublicDensity line 4908
  460. lemma OAI.ZeroKey.filteredPublicDensity_common_factors line 4935
  461. structure OAI.ZeroKey.BitProtocol line 4970
  462. def OAI.ZeroKey.BitProtocol.completeReference line 4992
  463. lemma OAI.ZeroKey.BitProtocol.completeReference_positive line 4996
  464. lemma OAI.ZeroKey.BitProtocol.completeReference_measurable line 5001
  465. lemma OAI.ZeroKey.BitProtocol.completeReference_integrable line 5006
  466. lemma OAI.ZeroKey.BitProtocol.completeReference_entry_integrable line 5011
  467. def OAI.ZeroKey.BitProtocol.probeOutput line 5016
  468. lemma OAI.ZeroKey.BitProtocol.probeOutput_event line 5021
  469. lemma OAI.ZeroKey.BitProtocol.initial_joint_reference line 5028
  470. theorem OAI.ZeroKey.BitProtocol.public_factors line 5042
  471. def OAI.ZeroKey.BitProtocol.canonicalOutput line 5061
  472. def OAI.ZeroKey.PositiveMatrixMeasure.positiveDensity line 5079
  473. lemma OAI.ZeroKey.PositiveMatrixMeasure.positiveDensity_pos line 5083
  474. lemma OAI.ZeroKey.PositiveMatrixMeasure.measurable_positiveDensity line 5090
  475. lemma OAI.ZeroKey.PositiveMatrixMeasure.positiveDensity_ae line 5100
  476. lemma OAI.ZeroKey.PositiveMatrixMeasure.integrable_positiveDensity_trace line 5106
  477. lemma OAI.ZeroKey.PositiveMatrixMeasure.integral_positiveDensity_trace line 5114
  478. def OAI.ZeroKey.PositiveMatrixMeasure.toBitDensity line 5129
  479. theorem OAI.ZeroKey.BitProtocol.canonical_density_representation line 5176
  480. lemma OAI.ZeroKey.BitProtocol.canonicalOutput_normalized line 5201
  481. def OAI.ZeroKey.cqDistance line 5225
  482. def OAI.ZeroKey.idealFiniteBlocks line 5228
  483. def OAI.ZeroKey.compressReference line 5243
  484. lemma OAI.ZeroKey.compressReference_pos line 5250
  485. lemma OAI.ZeroKey.compressReference_trace line 5256
  486. lemma OAI.ZeroKey.compressReference_right line 5264
  487. lemma OAI.ZeroKey.padded_purification_unitary line 5269
  488. def OAI.ZeroKey.embedReference line 5277
  489. lemma OAI.ZeroKey.embedReference_pos line 5283
  490. lemma OAI.ZeroKey.embedReference_trace line 5291
  491. def OAI.ZeroKey.refSandwich line 5295
  492. lemma OAI.ZeroKey.padded_purification_blocks line 5300
  493. theorem OAI.ZeroKey.purification_recovery line 5322
  494. theorem OAI.ZeroKey.purification_recovery_transpose line 5361
  495. def OAI.ZeroKey.purificationFilter line 5396
  496. def OAI.ZeroKey.publicPurifiedEntries line 5402

    Source documentation

    Matrix-valued output entries after purification and publication of the transcript.

    def publicPurifiedEntries {Ω T K : Type*} [MeasurableSpace Ω] [MeasurableSpace T]
    (μ : Measure Ω) (record : Ω → T) (W : K → K → Ω → Matrix ι ι ℂ)
    (P : Matrix ι κ ℂ) (a b : K) (x y : κ) : ComplexMeasure T :=
…
  497. def OAI.ZeroKey.positiveEntryDensity line 5409

    Source documentation

    The positive representative of the entrywise Radon–Nikodym derivative.

    def positiveEntryDensity {Ω : Type*} [MeasurableSpace Ω]
    (W : ι → ι → ComplexMeasure Ω) (μ : Measure Ω) (t : Ω) : Matrix ι ι ℂ := by
…
  498. lemma OAI.ZeroKey.purificationFilter_block line 5416
  499. lemma OAI.ZeroKey.preparationFilter_eq_purificationFilter line 5429
  500. theorem OAI.ZeroKey.purification_filter_recovery line 5432
  501. def OAI.ZeroKey.BitProtocol.purifiedOutput line 5475
  502. lemma OAI.ZeroKey.BitProtocol.purifiedOutput_ac line 5479
  503. lemma OAI.ZeroKey.BitProtocol.purifiedOutput_recovery line 5488
  504. lemma OAI.ZeroKey.BitProtocol.purifiedOutput_normalized line 5499
  505. def OAI.ZeroKey.BitProtocol.purifiedDensity line 5510
  506. def OAI.ZeroKey.BitProtocol.rawPurifiedSecretBitError line 5517

    Source documentation

    The operational bit error written directly in terms of the output entries.

    def rawPurifiedSecretBitError (P : Matrix (ι × η) κ ℂ)
    (sigma : PositiveMatrixMeasure (ℕ → M) κ) : ℝ :=
…

    Mentions: OAI.ZeroKey.PositiveMatrixMeasure

  507. def OAI.ZeroKey.BitProtocol.purifiedSecretBitError line 5528
  508. lemma OAI.ZeroKey.BitProtocol.rawPurifiedSecretBitError_eq line 5533
  509. def OAI.UnrestrictedQuantum.ObservableInstrument.postprocess line 5556
  510. lemma OAI.UnrestrictedQuantum.InstrumentRun.event_trace line 5570
  511. lemma OAI.UnrestrictedQuantum.InstrumentRun.event_zero line 5582
  512. def OAI.UnrestrictedQuantum.InstrumentRun.coarseMass line 5590
  513. def OAI.UnrestrictedQuantum.InstrumentRun.coarsePosterior line 5592
  514. lemma OAI.UnrestrictedQuantum.InstrumentRun.coarsePosterior_positive line 5599
  515. lemma OAI.UnrestrictedQuantum.InstrumentRun.coarsePosterior_trace line 5608
  516. lemma OAI.UnrestrictedQuantum.InstrumentRun.coarsePosterior_weighted line 5619
  517. lemma OAI.UnrestrictedQuantum.InstrumentRun.coarsePosterior_singleton line 5632
  518. lemma OAI.UnrestrictedQuantum.InstrumentRun.coarsePosterior_integral line 5642
  519. def OAI.UnrestrictedQuantum.InstrumentRun.postprocess line 5679
  520. lemma OAI.UnrestrictedQuantum.InstrumentRun.event_finset line 5706
  521. lemma OAI.UnrestrictedQuantum.InstrumentRun.event_total line 5717
  522. structure OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout line 5728
  523. def OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.value line 5738
  524. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.measurable line 5741
  525. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.positive line 5744
  526. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.sum line 5747
  527. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.subdensity line 5749
  528. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.event_finset line 5757
  529. lemma OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.eventMeasurable line 5761
  530. def OAI.UnrestrictedQuantum.IncomingObservableProcess.FiniteReadout.postprocess line 5766
  531. structure OAI.ZeroKey.FiniteProtocol line 5812
  532. def OAI.ZeroKey.FiniteProtocol.toBit line 5834
  533. def OAI.ZeroKey.FiniteProtocol.completeReference line 5844
  534. lemma OAI.ZeroKey.FiniteProtocol.completeReference_positive line 5848
  535. lemma OAI.ZeroKey.FiniteProtocol.completeReference_measurable line 5853
  536. lemma OAI.ZeroKey.FiniteProtocol.completeReference_integrable line 5858
  537. lemma OAI.ZeroKey.FiniteProtocol.completeReference_entry_integrable line 5863
  538. def OAI.ZeroKey.FiniteProtocol.probeOutput line 5868
  539. lemma OAI.ZeroKey.FiniteProtocol.probeOutput_event line 5873
  540. def OAI.ZeroKey.FiniteProtocol.canonicalOutput line 5879
  541. lemma OAI.ZeroKey.FiniteProtocol.canonicalOutput_event line 5883
  542. lemma OAI.ZeroKey.FiniteProtocol.completeReference_sum line 5922
  543. lemma OAI.ZeroKey.FiniteProtocol.completeReference_total line 5931
  544. lemma OAI.ZeroKey.FiniteProtocol.canonicalOutput_sum line 5951
  545. lemma OAI.ZeroKey.FiniteProtocol.canonicalOutput_normalized line 5960
  546. def OAI.ZeroKey.FiniteProtocol.purifiedOutput line 5999
  547. lemma OAI.ZeroKey.FiniteProtocol.purifiedOutput_event line 6003
  548. lemma OAI.ZeroKey.FiniteProtocol.purifiedOutput_ac line 6011
  549. lemma OAI.ZeroKey.FiniteProtocol.purifiedOutput_normalized line 6018
  550. def OAI.ZeroKey.FiniteProtocol.purifiedOutputDensity line 6030
  551. structure OAI.ZeroKey.KeyDensity line 6050
  552. structure OAI.ZeroKey.EveDensity line 6059
  553. def OAI.ZeroKey.KeyDensity.idealError line 6070
  554. def OAI.ZeroKey.KeyDensity.distance line 6072
  555. def OAI.ZeroKey.FiniteProtocol.purifiedKeyDensity line 6103
  556. def OAI.ZeroKey.KeyWord line 6130
  557. instance OAI.ZeroKey.keyWordFintype line 6134
  558. instance OAI.ZeroKey.keyWordDecidableEq line 6139
  559. instance OAI.ZeroKey.keyWordNonempty line 6144
  560. instance OAI.ZeroKey.keyWordMeasurableSpace line 6149
  561. instance OAI.ZeroKey.keyWordMeasurableSingletonClass line 6154
  562. structure OAI.ZeroKey.QuantumMemory line 6159
  563. instance OAI.ZeroKey.(instance at line 6168) line 6168
  564. structure OAI.ZeroKey.ClassicalRecordSpace line 6170
  565. instance OAI.ZeroKey.(instance at line 6178) line 6178
  566. structure OAI.ZeroKey.KeyImplementation line 6188
  567. def OAI.ZeroKey.KeyImplementation.output line 6210
  568. def OAI.ZeroKey.IsCompletedKeyOutput line 6215
  569. theorem OAI.ZeroKey.isCompletedKeyOutput_iff_original line 6228
  570. structure OAI.ZeroKey.CompletedKeyTrial line 6240
  571. def OAI.ZeroKey.CompletedKeyTrial.error line 6261
  572. def OAI.ZeroKey.groupIndex line 6273
  573. def OAI.ZeroKey.groupTensor line 6282
  574. lemma OAI.ZeroKey.trace_groupTensor line 6288
  575. lemma OAI.ZeroKey.Density.groupTensor line 6295
  576. def OAI.ZeroKey.copyDim line 6302
  577. lemma OAI.ZeroKey.copyDim_eq line 6306
  578. def OAI.ZeroKey.positiveCopies line 6311
  579. lemma OAI.ZeroKey.Density.positiveCopies line 6327
  580. instance OAI.ZeroKey.positiveCopy_nonempty line 6334
  581. structure OAI.ZeroKey.CompletedKeyScheme line 6341
  582. def OAI.ZeroKey.CompletedKeyScheme.error line 6361
  583. def OAI.ZeroKey.CompletedKeyScheme.Secure line 6363
  584. def OAI.ZeroKey.CompletedKeyScheme.lowerRate line 6365
  585. def OAI.ZeroKey.distillableSecretKey line 6369
  586. def OAI.ZeroKey.UniformProtocolGap line 6381
  587. def OAI.ZeroKey.UniformCompletedGap line 6400
  588. lemma OAI.ZeroKey.Explicit.m_pos line 6417
  589. instance OAI.ZeroKey.Explicit.output_nonempty line 6419
  590. def OAI.ZeroKey.Explicit.MainClaim line 6430