OAI/GroupTheory/SimpleAmenable/RandomFields/ThresholdField.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.thresholdField line 15
  2. theorem OAI.SimpleAmenable.thresholdField_measurable line 18
  3. theorem OAI.SimpleAmenable.thresholdField_reindex line 24
  4. def OAI.SimpleAmenable.signalSuccess line 27
  5. theorem OAI.SimpleAmenable.signalSuccess_measurable line 30
  6. theorem OAI.SimpleAmenable.signalSuccess_of_noise line 35
  7. theorem OAI.SimpleAmenable.sourceSmoothFieldLaw_close line 60
  8. def OAI.SimpleAmenable.sourceBitFieldLaw line 104
  9. instance OAI.SimpleAmenable.sourceBitFieldLaw_probability line 109
  10. theorem OAI.SimpleAmenable.sourceBitFieldLaw_success line 115
  11. def OAI.SimpleAmenable.extendFiniteBits line 147
  12. theorem OAI.SimpleAmenable.finiteBitWindow_finite line 150
  13. theorem OAI.SimpleAmenable.sourceBitFieldLaw_finite_support line 160