OAI/RepresentationTheory/FiniteUnitary/Sampling.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeShuffle.sampleLaw line 10
  2. lemma OAI.CubeShuffle.sampleLaw_nonneg line 14
  3. lemma OAI.CubeShuffle.sampleLaw_sum line 17
  4. lemma OAI.CubeShuffle.sampleLaw_pos_iff line 23
  5. lemma OAI.CubeShuffle.sampleLaw_equiv line 34
  6. lemma OAI.CubeShuffle.sampleLaw_inverse line 42
  7. lemma OAI.CubeShuffle.sampleLaw_symmetric line 49
  8. def OAI.CubeShuffle.UnitaryFinite.sampleOperator line 64

    Distinct definitions of this name: ComparatorChallenges/WeightedSweepMoments.lean:254 (same statement text; different proof or body). Qualify references as OAI.CubeShuffle.UnitaryFinite.sampleOperator@path.

  9. lemma OAI.CubeShuffle.UnitaryFinite.continuousRepresentation_comp line 68
  10. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_comp line 73
  11. lemma OAI.CubeShuffle.UnitaryFinite.unitary_comp line 78
  12. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_commute line 83
  13. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_weighted line 95
  14. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_norm_le line 112
  15. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_equiv line 118
  16. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_prod line 124
  17. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_inv line 136
  18. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_one line 142
  19. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_uniform line 148
  20. lemma OAI.CubeShuffle.UnitaryFinite.sampleOperator_uniform_mul line 152
  21. lemma OAI.CubeShuffle.UnitaryFinite.averageMap_zero line 171
  22. lemma OAI.CubeShuffle.UnitaryFinite.coefficient_cross_orthogonality line 180
  23. def OAI.CubeShuffle.UnitaryFinite.regularAction line 198
  24. lemma OAI.CubeShuffle.UnitaryFinite.regular_transitive line 204
  25. lemma OAI.CubeShuffle.UnitaryFinite.regular_fixed line 209
  26. def OAI.CubeShuffle.UnitaryFinite.regularCoefficient line 215
  27. lemma OAI.CubeShuffle.UnitaryFinite.regularCoefficient_apply line 219
  28. lemma OAI.CubeShuffle.UnitaryFinite.regularCoefficient_inner line 227
  29. lemma OAI.CubeShuffle.UnitaryFinite.regularCoefficient_cross line 236