OAI/GroupTheory/SimpleAmenable/RandomFields/AffineNoiseEnergy.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.noise_centered_integrable_product line 15
  2. theorem OAI.SimpleAmenable.integrable_sum_product line 30
  3. theorem OAI.SimpleAmenable.integrable_three_energy line 37
  4. def OAI.SimpleAmenable.affineNoiseGenerator line 64
  5. def OAI.SimpleAmenable.affineNoiseEnergyConstant line 70
  6. theorem OAI.SimpleAmenable.affineNoiseEnergyConstant_nonneg line 73
  7. theorem OAI.SimpleAmenable.noise_sum_integrable_product line 80
  8. theorem OAI.SimpleAmenable.affineNoiseGenerator_energy line 94
  9. def OAI.SimpleAmenable.smoothNoiseDensity line 154
  10. def OAI.SimpleAmenable.smoothNoiseLaw line 156
  11. theorem OAI.SimpleAmenable.smoothNoiseDensity_measurable line 158
  12. instance OAI.SimpleAmenable.smoothNoiseLaw_probability line 161
  13. theorem OAI.SimpleAmenable.smoothNoiseLaw_bounded line 174
  14. theorem OAI.SimpleAmenable.smoothNoiseLaw_centered line 184
  15. def OAI.SimpleAmenable.independentSmoothNoiseLaw line 196
  16. instance OAI.SimpleAmenable.independentSmoothNoiseLaw_probability line 199
  17. theorem OAI.SimpleAmenable.independentSmoothNoiseLaw_independent line 204
  18. theorem OAI.SimpleAmenable.independentSmoothNoiseLaw_map line 208
  19. theorem OAI.SimpleAmenable.independentSmoothNoiseLaw_bounded line 212
  20. theorem OAI.SimpleAmenable.independentSmoothNoiseLaw_centered line 218