OAI/Probability/SignedSweeps/MarkedWords.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.markedTargetTransport line 12
  2. lemma OAI.SignedSweeps.markedTargetTransport_one line 15
  3. lemma OAI.SignedSweeps.markedTargetTransport_mul line 19
  4. lemma OAI.SignedSweeps.markedTargetTransport_at line 25
  5. abbrev OAI.SignedSweeps.MarkedWordSpace line 32
  6. def OAI.SignedSweeps.markedWordLinear line 35
  7. lemma OAI.SignedSweeps.markedWordLinear_apply line 43
  8. def OAI.SignedSweeps.markedWordRepresentation line 49
  9. lemma OAI.SignedSweeps.markedWordRepresentation_apply line 67
  10. lemma OAI.SignedSweeps.markedWordRepresentation_norm line 73
  11. lemma OAI.SignedSweeps.markedWordRepresentation_insertion line 81
  12. def OAI.SignedSweeps.markedTypeProjection line 99
  13. lemma OAI.SignedSweeps.markedTypeProjection_positive line 104
  14. lemma OAI.SignedSweeps.markedTypeProjection_idempotent line 109
  15. lemma OAI.SignedSweeps.markedTypeProjection_commute line 115
  16. def OAI.SignedSweeps.markedTypeSubrepresentation line 126
  17. lemma OAI.SignedSweeps.markedWordRepresentation_pointwise line 132