OAI/Probability/SignedSweeps/GroupedDensity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.groupedWordMatrix_hull line 14
  2. lemma OAI.SignedSweeps.wordMatrix_toContinuous_hull line 41
  3. lemma OAI.SignedSweeps.wordContinuous_toMatrix_hull line 54
  4. lemma OAI.SignedSweeps.groupedWordMatrix_domination line 72
  5. lemma OAI.SignedSweeps.wordMatrix_scaled_sub_positive line 85
  6. def OAI.SignedSweeps.pairCarrierCost line 104
  7. lemma OAI.SignedSweeps.pairCarrierCost_pos line 110
  8. def OAI.SignedSweeps.groupedPairTypeProjection line 125
  9. lemma OAI.SignedSweeps.groupedPairTypeProjection_positive line 130
  10. lemma OAI.SignedSweeps.groupedPairTypeProjection_idempotent line 135
  11. def OAI.SignedSweeps.groupedEvenTensor line 141
  12. lemma OAI.SignedSweeps.groupedEvenTensor_eq line 145
  13. lemma OAI.SignedSweeps.evenColorMatrix_positive line 151
  14. lemma OAI.SignedSweeps.groupedEvenTensor_positive line 163
  15. theorem OAI.SignedSweeps.grouped_even_density_domination line 170