OAI/Analysis/FreeEntropy/TensorConcat.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.FreeTensor.atomMul line 12
  2. def OAI.FiniteEntropySeparation.FreeTensor.concatAux line 14
  3. def OAI.FiniteEntropySeparation.FreeTensor.concat line 18
  4. theorem OAI.FiniteEntropySeparation.FreeTensor.concat_nil line 20
  5. theorem OAI.FiniteEntropySeparation.FreeTensor.concat_push line 23
  6. theorem OAI.FiniteEntropySeparation.FreeTensor.concat_empty_left line 26
  7. theorem OAI.FiniteEntropySeparation.FreeTensor.concat_empty_right line 30
  8. theorem OAI.FiniteEntropySeparation.FreeTensor.concat_tail_length line 40
  9. theorem OAI.FiniteEntropySeparation.FreeTensor.atomMul_right_injective line 51
  10. theorem OAI.FiniteEntropySeparation.FreeTensor.concat_right_injective line 55
  11. theorem OAI.FiniteEntropySeparation.FreeTensor.leftB_concat line 82
  12. theorem OAI.FiniteEntropySeparation.FreeTensor.leftN_concat line 87
  13. theorem OAI.FiniteEntropySeparation.FreeTensor.leftG_concat line 90
  14. theorem OAI.FiniteEntropySeparation.FreeTensor.concat_noiseWord_cons line 97
  15. def OAI.FiniteEntropySeparation.FreeTensor.suffixEmbedding line 102
  16. theorem OAI.FiniteEntropySeparation.FreeTensor.suffixEmbedding_single line 105
  17. theorem OAI.FiniteEntropySeparation.FreeTensor.suffixEmbedding_basis line 109
  18. theorem OAI.FiniteEntropySeparation.FreeTensor.creationB_suffix line 112
  19. theorem OAI.FiniteEntropySeparation.FreeTensor.creationN_suffix line 118
  20. theorem OAI.FiniteEntropySeparation.FreeTensor.unitaryG_suffix line 124
  21. def OAI.FiniteEntropySeparation.FreeTensor.StartsNoise line 130
  22. def OAI.FiniteEntropySeparation.FreeTensor.Supported line 133
  23. def OAI.FiniteEntropySeparation.FreeTensor.StartsBackground line 136
  24. theorem OAI.FiniteEntropySeparation.FreeTensor.supported_empty line 140
  25. theorem OAI.FiniteEntropySeparation.FreeTensor.supported_leftB line 144
  26. theorem OAI.FiniteEntropySeparation.FreeTensor.supported_leftG line 148
  27. theorem OAI.FiniteEntropySeparation.FreeTensor.supported_leftN line 152
  28. theorem OAI.FiniteEntropySeparation.FreeTensor.supported_ne_empty_starts line 157
  29. theorem OAI.FiniteEntropySeparation.FreeTensor.startsBackground_concat line 170
  30. theorem OAI.FiniteEntropySeparation.FreeTensor.startsBackground_not_noise line 183