OAI/Analysis/FreeEntropy/MicrostatesSelection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.matrixVolumeEntropy line 9
  2. theorem OAI.FiniteEntropySeparation.matrixVolumeEntropy_ne_bot_volume line 11
  3. theorem OAI.FiniteEntropySeparation.matrixVolumeEntropy_coe line 16
  4. theorem OAI.FiniteEntropySeparation.exists_strictMono_diagonal line 21
  5. def OAI.FiniteEntropySeparation.diagonalMicrostates line 33
  6. theorem OAI.FiniteEntropySeparation.exists_microstate_dimensions line 35
  7. theorem OAI.FiniteEntropySeparation.diagonalMicrostates_moments line 48
  8. theorem OAI.FiniteEntropySeparation.diagonalMicrostates_measurable line 57
  9. theorem OAI.FiniteEntropySeparation.diagonalMicrostates_uniform_probability line 59