OAI/Probability/BinarySweep/TensorBounds/TensorReduction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Density.reshape line 17
  2. def OAI.BinaryCoordinateSweeps.Density.kraus line 20
  3. def OAI.BinaryCoordinateSweeps.Density.densityChannel line 23
  4. lemma OAI.BinaryCoordinateSweeps.Density.densityChannel_psd line 27
  5. lemma OAI.BinaryCoordinateSweeps.Density.densityChannel_sub line 32
  6. lemma OAI.BinaryCoordinateSweeps.Density.densityChannel_smul line 37
  7. lemma OAI.BinaryCoordinateSweeps.Density.densityChannel_sum line 42
  8. lemma OAI.BinaryCoordinateSweeps.Density.kraus_mulVec line 48
  9. lemma OAI.BinaryCoordinateSweeps.Density.densityChannel_rankOne line 54
  10. lemma OAI.BinaryCoordinateSweeps.Density.reshape_injective_apply line 62
  11. lemma OAI.BinaryCoordinateSweeps.Density.reshape_outside line 67
  12. def OAI.BinaryCoordinateSweeps.Density.wordPair line 73
  13. lemma OAI.BinaryCoordinateSweeps.Density.wordPair_eq_iff line 77
  14. lemma OAI.BinaryCoordinateSweeps.Density.wordPair_injective line 83
  15. lemma OAI.BinaryCoordinateSweeps.Density.reshape_tensor line 91
  16. def OAI.BinaryCoordinateSweeps.Density.matrixTensorPower line 107
  17. def OAI.BinaryCoordinateSweeps.Density.matrixTensorRect line 110
  18. lemma OAI.BinaryCoordinateSweeps.Density.tensor_gram line 114
  19. lemma OAI.BinaryCoordinateSweeps.Density.densityChannel_tensorRankOne line 123
  20. lemma OAI.BinaryCoordinateSweeps.Density.reshape_trace line 144
  21. lemma OAI.BinaryCoordinateSweeps.Density.gram_psd line 158
  22. lemma OAI.BinaryCoordinateSweeps.Density.reshape_even line 163
  23. def OAI.BinaryCoordinateSweeps.Density.reducedPhaseDensity line 183
  24. lemma OAI.BinaryCoordinateSweeps.Density.reducedPhaseDensity_psd line 188
  25. lemma OAI.BinaryCoordinateSweeps.Density.reducedPhaseDensity_trace line 191
  26. lemma OAI.BinaryCoordinateSweeps.Density.reducedPhaseDensity_even line 198