OAI/Analysis/FreeEntropy/EquidiscreteSignal.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.equidiscreteAtom line 10
  2. theorem OAI.FiniteEntropySeparation.equidiscreteAtom_rev line 12
  3. theorem OAI.FiniteEntropySeparation.sum_equidiscreteAtom line 26
  4. theorem OAI.FiniteEntropySeparation.equidiscreteAtom_abs_le line 31
  5. def OAI.FiniteEntropySeparation.FreeTensor.dualIndex line 49
  6. def OAI.FiniteEntropySeparation.FreeTensor.equidiscreteSignal line 52
  7. theorem OAI.FiniteEntropySeparation.FreeTensor.equidiscreteSignal_selfAdjoint line 55
  8. theorem OAI.FiniteEntropySeparation.FreeTensor.equidiscreteSignal_mem line 58
  9. theorem OAI.FiniteEntropySeparation.FreeTensor.equidiscreteSignal_norm_le line 61
  10. theorem OAI.FiniteEntropySeparation.FreeTensor.equidiscreteSignal_moments line 65
  11. theorem OAI.FiniteEntropySeparation.FreeTensor.trace_equidiscreteSignal line 73
  12. theorem OAI.FiniteEntropySeparation.FreeTensor.characterProjection_mem_background line 78
  13. theorem OAI.FiniteEntropySeparation.FreeTensor.equidiscreteSignal_mem_background line 87
  14. theorem OAI.FiniteEntropySeparation.FreeTensor.characterProjection_commutes_B line 93
  15. theorem OAI.FiniteEntropySeparation.FreeTensor.equidiscreteSignal_commutes_B line 101
  16. theorem OAI.FiniteEntropySeparation.FreeTensor.tensor_characterProjection_moment line 107
  17. theorem OAI.FiniteEntropySeparation.FreeTensor.tensor_equidiscrete_moment line 119