OAI/Analysis/CoulombRadii/FieldAnalysis/SpinMode.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Coulomb.SpinMode line 17
  2. theorem OAI.Coulomb.spin_lattice_count line 19
  3. lemma OAI.Coulomb.latticeRadius_nonneg line 35
  4. theorem OAI.Coulomb.ordered_lattice_radius_lower line 37
  5. lemma OAI.Coulomb.sum_two_thirds_lower line 61
  6. lemma OAI.Coulomb.sum_one_third_upper line 73
  7. lemma OAI.Coulomb.square_lower_of_shift line 87
  8. lemma OAI.Coulomb.finite_sort_values line 95
  9. def OAI.Coulomb.neumannLeading line 132
  10. def OAI.Coulomb.neumannBoundary line 133
  11. theorem OAI.Coulomb.neumann_radii_sum_lower line 135
  12. def OAI.Coulomb.thomasFermiCoefficient line 188
  13. lemma OAI.Coulomb.neumann_coefficient_exact line 191
  14. theorem OAI.Coulomb.neumann_kinetic_sum_lower line 203
  15. def OAI.Coulomb.finiteCubeMeasure line 223
  16. def OAI.Coulomb.finiteCubeMode line 226
  17. def OAI.Coulomb.reindexCube line 229
  18. lemma OAI.Coulomb.reindexCube_apply line 233
  19. lemma OAI.Coulomb.reindexCube_measurePreserving line 239
  20. lemma OAI.Coulomb.finiteCubeMode_reindex line 244
  21. lemma OAI.Coulomb.euclidean_reindex_toLp line 250
  22. lemma OAI.Coulomb.euclidean_reindex_toLp_cancel line 257
  23. lemma OAI.Coulomb.finiteCube_integral_reindex line 264
  24. lemma OAI.Coulomb.finiteCube_coefficient_reindex line 276
  25. lemma OAI.Coulomb.euclidean_weak_reindex line 289
  26. theorem OAI.Coulomb.finiteCube_weak_spectral_lower line 326
  27. def OAI.Coulomb.spinDelta line 371
  28. lemma OAI.Coulomb.spinDelta_memLp line 373
  29. lemma OAI.Coulomb.spinDelta_inner line 377
  30. lemma OAI.Coulomb.spinDelta_complete line 383
  31. lemma OAI.Coulomb.cubeMode_complete line 390
  32. def OAI.Coulomb.spinCubeMeasure line 394
  33. def OAI.Coulomb.spinCubeMode line 397
  34. lemma OAI.Coulomb.cubeMode_memLp line 400
  35. lemma OAI.Coulomb.spinCubeMode_memLp line 404
  36. lemma OAI.Coulomb.spinCubeMode_complete line 408