OAI/Analysis/HardSphere/Fourier/CharacterDerivativeFactor.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.configurationCharacter_smooth line 19
  2. lemma OAI.HardSphere.configurationCharacter_single_argument line 30
  3. lemma OAI.HardSphere.configurationCharacter_coordinateLine line 47
  4. def OAI.HardSphere.characterDerivativeFactor line 53
  5. lemma OAI.HardSphere.configurationCharacter_partial line 56
  6. lemma OAI.HardSphere.character_smoothPartial line 67
  7. lemma OAI.HardSphere.character_weak_derivative line 73
  8. lemma OAI.HardSphere.allowed_of_neg line 83
  9. def OAI.HardSphere.characterTest line 89
  10. lemma OAI.HardSphere.characterTest_jet line 105
  11. lemma OAI.HardSphere.character_factor_square line 122
  12. lemma OAI.HardSphere.character_form_pairing line 130
  13. lemma OAI.HardSphere.character_resolvent line 147
  14. lemma OAI.HardSphere.character_formHeat line 187
  15. lemma OAI.HardSphere.freeTransition_eq_formHeat line 202