OAI/Analysis/CoulombRadii/FieldAnalysis/CubeLabelEquiv.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.spinCubeMode_inner line 17
  2. lemma OAI.Coulomb.finiteCubeMeasure_le_volume line 45
  3. lemma OAI.Coulomb.finiteCubeMode_memLp line 51
  4. lemma OAI.Coulomb.finiteCubeMode_inner line 62
  5. lemma OAI.Coulomb.finiteCubeMode_complete line 77
  6. def OAI.Coulomb.cubeLabelEquiv line 94
  7. def OAI.Coulomb.cubeFermionCoefficient line 101
  8. def OAI.Coulomb.cubeMass line 107
  9. lemma OAI.Coulomb.H1Vector.cube_memLp line 111
  10. lemma OAI.Coulomb.finiteCubeCoefficient_summable line 117
  11. lemma OAI.Coulomb.cubeFermionCoefficient_summable line 128
  12. lemma OAI.Coulomb.cubeFermionCoefficient_parseval line 142
  13. lemma OAI.Coulomb.cubeFermionCoefficient_antisymmetric line 160
  14. def OAI.Coulomb.cubeKinetic line 186
  15. def OAI.Coulomb.cubeSpectralWeight line 190
  16. lemma OAI.Coulomb.cubeSpectralWeight_nonneg line 193
  17. lemma OAI.Coulomb.configuration_nonempty_equiv line 198
  18. lemma OAI.Coulomb.cubeFermionCoefficient_finite_energy line 205
  19. lemma OAI.Coulomb.cubeFermionCoefficient_energy_summable line 241
  20. lemma OAI.Coulomb.cubeFermionCoefficient_energy_le line 247
  21. lemma OAI.Coulomb.cubeSpectralWeight_eq_neumann line 254
  22. theorem OAI.Coulomb.fermionic_cube_kinetic_lower line 268