OAI/Analysis/CoulombRadii/FieldAnalysis/SpinCubeEquiv.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.measurePreserving_const_uncurry line 13
2. lemma OAI.Coulomb.measure_pi_count line 31
3. def OAI.Coulomb.spinCubeEquiv line 38
4. lemma OAI.Coulomb.spinCubeEquiv_measurePreserving line 43
5. instance OAI.Coulomb.finiteCubeMeasure_isFinite line 53
6. instance OAI.Coulomb.spinCubeMeasure_isFinite line 57
7. def OAI.Coulomb.cubeState line 61
8. lemma OAI.Coulomb.H1Vector.spinCube_memLp line 65
9. lemma OAI.Coulomb.H1Vector.cubeState_memLp line 80
10. lemma OAI.Coulomb.cubeState_mass line 84
11. lemma OAI.Coulomb.cubeState_antisymmetric line 92
12. lemma OAI.Coulomb.spinCube_tensor_delta line 106
13. lemma OAI.Coulomb.cubeState_coefficient line 127