OAI/GroupTheory/SimpleAmenable/RandomFields/NoiseTensor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.noiseTensor line 14
  2. theorem OAI.SimpleAmenable.noiseTensor_inner line 17
  3. theorem OAI.SimpleAmenable.noiseTensor_integrable_inner line 22
  4. theorem OAI.SimpleAmenable.noiseTensor_energy line 27
  5. def OAI.SimpleAmenable.centeredNoiseTensor line 31
  6. theorem OAI.SimpleAmenable.centeredNoiseTensor_orthogonal line 35
  7. theorem OAI.SimpleAmenable.centeredNoiseTensor_energy line 49
  8. inductive OAI.SimpleAmenable.NoiseFactor line 67
  9. def OAI.SimpleAmenable.noiseFactor line 71
  10. theorem OAI.SimpleAmenable.noiseFactor_continuous line 77
  11. theorem OAI.SimpleAmenable.noiseFactor_compact line 83
  12. theorem OAI.SimpleAmenable.noiseFactor_integrable_product line 93
  13. theorem OAI.SimpleAmenable.noiseFactor_centered line 99