OAI/Probability/BinarySweep/TensorBounds/TensorPhases.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.Density.wordCounts_le line 16
  2. lemma OAI.BinaryCoordinateSweeps.Density.phase_star line 21
  3. lemma OAI.BinaryCoordinateSweeps.Density.phase_sum_prod line 28
  4. lemma OAI.BinaryCoordinateSweeps.Density.phase_sum line 35
  5. def OAI.BinaryCoordinateSweeps.Density.tensorPhase line 48
  6. lemma OAI.BinaryCoordinateSweeps.Density.tensorPhase_counts line 51
  7. lemma OAI.BinaryCoordinateSweeps.Density.phase_pair_sum line 57
  8. def OAI.BinaryCoordinateSweeps.Density.rankOne line 88
  9. lemma OAI.BinaryCoordinateSweeps.Density.rankOne_psd line 91
  10. def OAI.BinaryCoordinateSweeps.Density.typeVector line 100
  11. def OAI.BinaryCoordinateSweeps.Density.typeOnes line 102
  12. lemma OAI.BinaryCoordinateSweeps.Density.typeOnes_apply line 105
  13. lemma OAI.BinaryCoordinateSweeps.Density.typeOnes_psd line 111
  14. lemma OAI.BinaryCoordinateSweeps.Density.sum_typeOnes line 114
  15. lemma OAI.BinaryCoordinateSweeps.Density.typeKernel_psd line 124
  16. lemma OAI.BinaryCoordinateSweeps.Density.typeKernel_mono line 132
  17. abbrev OAI.BinaryCoordinateSweeps.Density.WordType line 146
  18. def OAI.BinaryCoordinateSweeps.Density.wordType line 149
  19. lemma OAI.BinaryCoordinateSweeps.Density.wordType_eq_iff line 152
  20. lemma OAI.BinaryCoordinateSweeps.Density.wordType_total line 156
  21. lemma OAI.BinaryCoordinateSweeps.Density.card_wordType line 159
  22. def OAI.BinaryCoordinateSweeps.Density.symmetricProjector line 166
  23. lemma OAI.BinaryCoordinateSweeps.Density.symmetricProjector_psd line 170