OAI/Analysis/HardSphere/Fourier/ArgumentAdd.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.FreeFourier.argument_add line 16
  2. lemma OAI.HardSphere.FreeFourier.gaussian_character line 20
  3. def OAI.HardSphere.configurationCharacter line 49
  4. lemma OAI.HardSphere.configurationCharacter_norm line 54
  5. lemma OAI.HardSphere.configurationCharacter_add_argument line 59
  6. lemma OAI.HardSphere.wiener_endpoint_law line 66
  7. lemma OAI.HardSphere.wiener_character line 69
  8. def OAI.HardSphere.fourierEnergy line 77
  9. lemma OAI.HardSphere.fourierEnergy_nonneg line 80
  10. lemma OAI.HardSphere.freeTrajectory_character_integral line 83
  11. lemma OAI.HardSphere.configurationCharacter_neg line 108
  12. lemma OAI.HardSphere.configurationCharacter_add line 113
  13. lemma OAI.HardSphere.configurationCharacter_zero line 120
  14. lemma OAI.HardSphere.configurationCharacter_single line 126
  15. def OAI.HardSphere.characterAlgebra line 137
  16. lemma OAI.HardSphere.characterAlgebra_eq_span line 148
  17. lemma OAI.HardSphere.characterAlgebra_separates line 157
  18. lemma OAI.HardSphere.character_span_dense line 169
  19. def OAI.HardSphere.characterL2 line 182
  20. lemma OAI.HardSphere.characterL2_ae line 190
  21. lemma OAI.HardSphere.characterL2_span_dense line 194