OAI/Probability/SignedSweeps/MarkedCompression.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.fiberBlock line 13
  2. lemma OAI.SignedSweeps.fiberBlock_positive line 16
  3. lemma OAI.SignedSweeps.fiber_resolution line 21
  4. lemma OAI.SignedSweeps.fiberBlock_mul line 33
  5. lemma OAI.SignedSweeps.fiberBlock_diagonal_mul line 45
  6. lemma OAI.SignedSweeps.trace_fiber_product line 59
  7. lemma OAI.SignedSweeps.markedWord_fiberBlock line 80
  8. lemma OAI.SignedSweeps.coefficient_fiberBlock line 92
  9. lemma OAI.SignedSweeps.marked_fiberBlock_viaEmbedding line 101
  10. theorem OAI.SignedSweeps.marked_coefficient_compression line 107
  11. def OAI.SignedSweeps.markedRoutes line 132
  12. lemma OAI.SignedSweeps.markedRoutes_preserved line 135
  13. lemma OAI.SignedSweeps.marked_coefficient_support line 141
  14. lemma OAI.SignedSweeps.marked_routes_injective line 156
  15. theorem OAI.SignedSweeps.marked_positive_product_trace_split line 165
  16. lemma OAI.SignedSweeps.marked_coefficient_compression_positive line 183