OAI/InformationTheory/SecretKey/MatrixMeasure.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ZeroKey.exists_local_instrument_sampler line 15
  2. def OAI.ZeroKey.LocalOutcomeSampler.instrumentKernel line 41
  3. instance OAI.ZeroKey.LocalOutcomeSampler.instrumentKernel_markov line 50
  4. lemma OAI.ZeroKey.LocalOutcomeSampler.causal_step_law line 57
  5. lemma OAI.ZeroKey.PositiveMatrixMeasure.integrable_density line 86
  6. theorem OAI.ZeroKey.positive_matrix_martingale_extension line 111
  7. lemma OAI.ZeroKey.keepReference_pos line 198
  8. lemma OAI.ZeroKey.trace_keepReference line 206
  9. def OAI.ZeroKey.localAction line 218
  10. lemma OAI.ZeroKey.localAction_refFilter line 222
  11. lemma OAI.ZeroKey.localAction_positive line 252
  12. lemma OAI.ZeroKey.PositiveMatrixMeasure.traceMeasure_real line 269
  13. lemma OAI.ZeroKey.PositiveMatrixMeasure.value_zero_of_traceMeasure_zero line 274
  14. def OAI.ZeroKey.PositiveMatrixMeasure.sum line 285
  15. lemma OAI.ZeroKey.PositiveMatrixMeasure.sum_value line 297
  16. lemma OAI.ZeroKey.PositiveMatrixMeasure.value_zero_of_sum_trace_zero line 303
  17. lemma OAI.ZeroKey.PositiveMatrixMeasure.sum_trace_density_one line 319
  18. lemma OAI.ZeroKey.PositiveMatrixMeasure.integrable_test_density line 342
  19. lemma OAI.ZeroKey.PositiveMatrixMeasure.integral_test_density line 350
  20. lemma OAI.ZeroKey.referenceFilter_pos line 372
  21. lemma OAI.ZeroKey.localAction_product line 385
  22. lemma OAI.ZeroKey.keepReference_localAction line 396
  23. lemma OAI.ZeroKey.trace_localAction line 403
  24. structure OAI.ZeroKey.QuantumInstrument line 413
  25. def OAI.ZeroKey.PositiveMatrixMeasure.retainReference line 428
  26. lemma OAI.ZeroKey.PositiveMatrixMeasure.retainReference_value line 439
  27. lemma OAI.ZeroKey.PositiveMatrixMeasure.pushforward_filter line 445
  28. lemma OAI.ZeroKey.PositiveMatrixMeasure.normalized_density line 452
  29. lemma OAI.ZeroKey.QuantumInstrument.operation_apply line 479
  30. def OAI.ZeroKey.QuantumInstrument.withReference line 490
  31. lemma OAI.ZeroKey.QuantumInstrument.withReference_value line 506
  32. lemma OAI.ZeroKey.QuantumInstrument.total_reference_unchanged line 516
  33. lemma OAI.ZeroKey.QuantumInstrument.normalized_outcome_measure line 524
  34. lemma OAI.ZeroKey.QuantumInstrument.withReference_filter line 536
  35. def OAI.ZeroKey.QuantumInstrument.referenceLaw line 546
  36. lemma OAI.ZeroKey.QuantumInstrument.referenceLaw_value line 552
  37. lemma OAI.ZeroKey.QuantumInstrument.referenceLaw_filter line 559
  38. lemma OAI.ZeroKey.QuantumInstrument.reference_test_born line 570
  39. theorem OAI.ZeroKey.QuantumInstrument.reference_posterior_mean line 582
  40. theorem OAI.ZeroKey.instrument_history_reference_extension line 635