OAI/Analysis/HardSphere/Comparison/PermutationPullbackComp.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.permutationPullback_comp line 16
2. lemma OAI.HardSphere.inner_permutationPullback line 24
3. lemma OAI.HardSphere.gradientPairing_permutationJet line 29
4. theorem OAI.HardSphere.IsGroundVector.permutationInvariant line 39
5. lemma OAI.HardSphere.bosonic_sum_permutationPullback line 52
6. lemma OAI.HardSphere.gradientPairing_sum_right line 59
7. theorem OAI.HardSphere.IsGroundVector.full_first_variation line 66