OAI/Analysis/HardSphere/CondensationDefinitions.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Ground-state condensation in the dilute hard-sphere gas

The main result covers all pure ground states and all density operators supported on the ground space. In particular it covers the normalized ground-space projection. Only the definitions needed to state this result are retained below.

  1. abbrev OAI.HardSphere.Length line 17

    Also declared: ComparatorChallenges/HardSphere.lean:17 (same declaration text).

  2. instance OAI.HardSphere.lengthPositive line 19

    Also declared: ComparatorChallenges/HardSphere.lean:19 (same declaration text).

  3. abbrev OAI.HardSphere.Torus line 21

    Also declared: ComparatorChallenges/HardSphere.lean:21 (same declaration text).

  4. abbrev OAI.HardSphere.Configuration line 23

    Also declared: ComparatorChallenges/HardSphere.lean:23 (same declaration text).

  5. abbrev OAI.HardSphere.LiftedConfiguration line 25

    Also declared: ComparatorChallenges/HardSphere.lean:25 (same declaration text).

  6. abbrev OAI.HardSphere.Direction line 27

    Also declared: ComparatorChallenges/HardSphere.lean:27 (same declaration text).

  7. def OAI.HardSphere.torusDistance line 29

    Also declared: ComparatorChallenges/HardSphere.lean:29 (same declaration text).

  8. def OAI.HardSphere.allowed line 32

    Also declared: ComparatorChallenges/HardSphere.lean:32 (same declaration text).

  9. def OAI.HardSphere.project line 35

    Also declared: ComparatorChallenges/HardSphere.lean:35 (same declaration text).

  10. def OAI.HardSphere.representative line 38

    Also declared: ComparatorChallenges/HardSphere.lean:38 (same declaration text).

  11. def OAI.HardSphere.coordDerivative line 41

    Also declared: ComparatorChallenges/HardSphere.lean:41 (same declaration text).

  12. abbrev OAI.HardSphere.ScalarL2 line 46

    Also declared: ComparatorChallenges/HardSphere.lean:46 (same declaration text).

  13. abbrev OAI.HardSphere.Jet line 49

    Also declared: ComparatorChallenges/HardSphere.lean:49 (same declaration text).

  14. structure OAI.HardSphere.SmoothTest line 52

    Also declared: ComparatorChallenges/HardSphere.lean:52 (same declaration text).

  15. def OAI.HardSphere.SmoothTest.jet line 60

    Also declared: ComparatorChallenges/HardSphere.lean:60 (same declaration text).

  16. def OAI.HardSphere.dirichletDomain line 63

    Also declared: ComparatorChallenges/HardSphere.lean:63 (same declaration text).

  17. def OAI.HardSphere.energy line 66

    Also declared: ComparatorChallenges/HardSphere.lean:66 (same declaration text).

  18. def OAI.HardSphere.bosonic line 69

    Also declared: ComparatorChallenges/HardSphere.lean:69 (same declaration text).

  19. def OAI.HardSphere.IsGroundVector line 73

    Also declared: ComparatorChallenges/HardSphere.lean:73 (same declaration text).

  20. def OAI.HardSphere.insertFirst line 77

    Also declared: ComparatorChallenges/HardSphere.lean:77 (same declaration text).

  21. def OAI.HardSphere.occupation line 81

    Also declared: ComparatorChallenges/HardSphere.lean:81 (same declaration text).

  22. def OAI.HardSphere.Density.basisSet line 88

    Also declared: ComparatorChallenges/HardSphere.lean:88 (same declaration text).

  23. def OAI.HardSphere.Density.basis line 90

    Also declared: ComparatorChallenges/HardSphere.lean:90 (same declaration text).

  24. structure OAI.HardSphere.Density.Operator line 93

    Also declared: ComparatorChallenges/HardSphere.lean:93 (same declaration text).

  25. def OAI.HardSphere.Density.Operator.compressionTrace line 101

    Also declared: ComparatorChallenges/HardSphere.lean:101 (same declaration text).

  26. def OAI.HardSphere.Orbital.sliceIntegral line 110

    Also declared: ComparatorChallenges/HardSphere.lean:110 (same declaration text).

  27. def OAI.HardSphere.Orbital.map line 113

    Also declared: ComparatorChallenges/HardSphere.lean:113 (same declaration text).

  28. def OAI.HardSphere.Orbital.continuous line 190

    Also declared: ComparatorChallenges/HardSphere.lean:190 (same declaration text).

  29. def OAI.HardSphere.GroundSupported line 363

    Also declared: ComparatorChallenges/HardSphere.lean:363 (same declaration text).

  30. def OAI.HardSphere.mixedOccupation line 368

    Also declared: ComparatorChallenges/HardSphere.lean:368 (same declaration text).