OAI/GroupTheory/SimpleAmenable/RandomFields/FiniteOrthogonalEnergy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.integral_finite_energy line 15
  2. theorem OAI.SimpleAmenable.integral_product_le_half_energy line 25
  3. theorem OAI.SimpleAmenable.finite_overlap_energy line 42
  4. def OAI.SimpleAmenable.rawNoiseBump line 85
  5. def OAI.SimpleAmenable.rawNoiseMass line 88
  6. theorem OAI.SimpleAmenable.rawNoiseMass_pos line 90
  7. def OAI.SimpleAmenable.smoothNoiseRoot line 102
  8. theorem OAI.SimpleAmenable.smoothNoiseRoot_nonneg line 104
  9. theorem OAI.SimpleAmenable.smoothNoiseRoot_even line 107
  10. theorem OAI.SimpleAmenable.smoothNoiseRoot_contDiff line 111
  11. theorem OAI.SimpleAmenable.smoothNoiseRoot_compact line 114
  12. theorem OAI.SimpleAmenable.smoothNoiseRoot_zero line 117
  13. theorem OAI.SimpleAmenable.smoothNoiseRoot_pos line 123
  14. theorem OAI.SimpleAmenable.smoothNoiseRoot_normalized line 128
  15. def OAI.SimpleAmenable.noiseEnergy line 139
  16. theorem OAI.SimpleAmenable.noiseEnergy_nonneg line 142
  17. theorem OAI.SimpleAmenable.noise_centered_energy line 145
  18. def OAI.SimpleAmenable.singletonNoise line 188
  19. theorem OAI.SimpleAmenable.singletonNoise_energy_bound line 191
  20. def OAI.SimpleAmenable.NoisePair line 207
  21. instance OAI.SimpleAmenable.(instance at line 209) line 209
  22. def OAI.SimpleAmenable.noisePairSwap line 212
  23. theorem OAI.SimpleAmenable.noisePair_card line 214
  24. def OAI.SimpleAmenable.pairNoise line 235
  25. theorem OAI.SimpleAmenable.pairNoise_energy_bound line 239