OAI/Analysis/FreeEntropy/TensorFreeness.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.FreeTensor.labelSpace line 12
  2. theorem OAI.FiniteEntropySeparation.FreeTensor.basis_mem_labelSpace line 16
  3. theorem OAI.FiniteEntropySeparation.FreeTensor.labelSpace_action line 20
  4. theorem OAI.FiniteEntropySeparation.FreeTensor.centered_labelSpace_suffix line 29
  5. theorem OAI.FiniteEntropySeparation.FreeTensor.labelSpace_vacuum_zero line 59
  6. theorem OAI.FiniteEntropySeparation.FreeTensor.trace_eq_vacuum_coefficient line 70
  7. theorem OAI.FiniteEntropySeparation.FreeTensor.annihilationB_preserves_supported line 74
  8. theorem OAI.FiniteEntropySeparation.FreeTensor.annihilationN_preserves_supported line 85
  9. theorem OAI.FiniteEntropySeparation.FreeTensor.background_preserves_supported line 98
  10. theorem OAI.FiniteEntropySeparation.FreeTensor.removeB_concat_noise line 130
  11. theorem OAI.FiniteEntropySeparation.FreeTensor.removeN_concat_noise line 146
  12. theorem OAI.FiniteEntropySeparation.FreeTensor.annihilationB_suffix_noise line 161
  13. theorem OAI.FiniteEntropySeparation.FreeTensor.annihilationN_suffix_noise line 172
  14. theorem OAI.FiniteEntropySeparation.FreeTensor.background_commutes_suffix line 184
  15. theorem OAI.FiniteEntropySeparation.FreeTensor.centered_background_basis line 198
  16. def OAI.FiniteEntropySeparation.FreeTensor.PureSupported line 214
  17. def OAI.FiniteEntropySeparation.FreeTensor.StartsNoiseIn line 217
  18. theorem OAI.FiniteEntropySeparation.FreeTensor.removeN_none_iff line 220
  19. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_basis_leftN line 232
  20. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_basis_not_starts line 237
  21. theorem OAI.FiniteEntropySeparation.FreeTensor.pureSupported_empty line 243
  22. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_preserves_pureSupported line 246
  23. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_pureSuffix line 266
  24. theorem OAI.FiniteEntropySeparation.FreeTensor.noise_adjoin_suffix line 290
  25. theorem OAI.FiniteEntropySeparation.FreeTensor.pureSupported_ne_empty_concat line 313
  26. theorem OAI.FiniteEntropySeparation.FreeTensor.centered_noise_basis line 321
  27. theorem OAI.FiniteEntropySeparation.FreeTensor.centered_coordinate_basis line 334
  28. theorem OAI.FiniteEntropySeparation.FreeTensor.centered_background_vacuum line 345
  29. theorem OAI.FiniteEntropySeparation.FreeTensor.startsNoise_injective line 363
  30. theorem OAI.FiniteEntropySeparation.FreeTensor.not_startsNoise_empty line 371
  31. theorem OAI.FiniteEntropySeparation.FreeTensor.not_startsBackground_empty line 375
  32. def OAI.FiniteEntropySeparation.FreeTensor.noiseAlgebras line 380
  33. def OAI.FiniteEntropySeparation.FreeTensor.StartsColor line 385
  34. theorem OAI.FiniteEntropySeparation.FreeTensor.centered_noiseAlgebras_vacuum line 389
  35. theorem OAI.FiniteEntropySeparation.FreeTensor.centered_noiseAlgebras_starts line 397
  36. theorem OAI.FiniteEntropySeparation.FreeTensor.alternating_noise_product_starts line 418
  37. theorem OAI.FiniteEntropySeparation.FreeTensor.free_noiseAlgebras line 442
  38. theorem OAI.FiniteEntropySeparation.FreeTensor.freeStandardNoise line 452