OAI/GroupTheory/SimpleAmenable/RandomFields/FieldHS.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.sourceFlagMatrix_HS_tendsto line 18
  2. theorem OAI.SimpleAmenable.smallTransportParameters line 61
  3. def OAI.SimpleAmenable.fieldReindex line 100
  4. theorem OAI.SimpleAmenable.fieldReindex_measurable line 103
  5. theorem OAI.SimpleAmenable.independentSmoothNoiseLaw_reindex line 106
  6. theorem OAI.SimpleAmenable.finiteCoefficientField_enlarge line 114
  7. theorem OAI.SimpleAmenable.finiteCoefficientField_covariance line 122
  8. theorem OAI.SimpleAmenable.sourceFlagMatrix_posSemidef line 152
  9. theorem OAI.SimpleAmenable.sourceFlagMatrix_box_support line 162
  10. def OAI.SimpleAmenable.sourceSmoothFieldLaw line 174
  11. instance OAI.SimpleAmenable.sourceSmoothFieldLaw_probability line 181
  12. def OAI.SimpleAmenable.sourceCommonSites line 187
  13. theorem OAI.SimpleAmenable.sourceSmoothFieldLaw_as_common line 192
  14. theorem OAI.SimpleAmenable.sourceSmoothFieldLaw_transported line 207