OAI/Analysis/CoulombRadii/FieldAnalysis/GroupFermionicCoefficients.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.GroupFermionicCoefficients line 122
  2. lemma OAI.Coulomb.GroupFermionicCoefficients.vanish_of_repeat line 127
  3. def OAI.Coulomb.groupNeumannLower line 151
  4. lemma OAI.Coulomb.grouped_neumann_spectral_lower line 158
  5. lemma OAI.Coulomb.GroupFermionicCoefficients.spectral_lower line 190
  6. def OAI.Coulomb.GroupAntisymmetric line 208
  7. lemma OAI.Coulomb.cubeFermionCoefficient_group_antisymmetric line 213
  8. lemma OAI.Coulomb.grouped_fermionic_cube_kinetic_lower line 240
  9. lemma OAI.Coulomb.translate_group_antisymmetric line 251
  10. lemma OAI.Coulomb.assigned_cube_kinetic_lower line 265
  11. def OAI.Coulomb.gridBox line 276
  12. lemma OAI.Coulomb.gridBox_measurable line 279
  13. lemma OAI.Coulomb.gridBox_disjoint line 283
  14. lemma OAI.Coulomb.gridBox_iUnion line 301
  15. lemma OAI.Coulomb.finiteCubeMeasure_eq_restrict line 319
  16. lemma OAI.Coulomb.gridBox_preimage_add line 325
  17. lemma OAI.Coulomb.gridBox_integral_eq_cube line 334
  18. lemma OAI.Coulomb.gridBox_hasSum_integral line 342
  19. lemma OAI.Coulomb.sum_fiber_card line 353
  20. lemma OAI.Coulomb.sum_power_le_power_sum line 361
  21. lemma OAI.Coulomb.sum_fiber_power_le line 379
  22. lemma OAI.Coulomb.thomasFermiCoefficient_pos line 386
  23. lemma OAI.Coulomb.neumannBoundary_nonneg line 390
  24. def OAI.Coulomb.groupLeadingCount line 394
  25. lemma OAI.Coulomb.groupLeadingCount_nonneg line 398
  26. lemma OAI.Coulomb.groupLeadingCount_le line 402
  27. lemma OAI.Coulomb.groupNeumannLower_uniform line 406
  28. abbrev OAI.Coulomb.GridAssignment line 418
  29. def OAI.Coulomb.gridCell line 420
  30. def OAI.Coulomb.gridLeadingCount line 423
  31. def OAI.Coulomb.gridShift line 426
  32. lemma OAI.Coulomb.grid_cube_kinetic_lower line 429
  33. lemma OAI.Coulomb.gridShift_hasSum_integral line 443
  34. lemma OAI.Coulomb.grid_hasSum_mass line 454
  35. lemma OAI.Coulomb.grid_hasSum_kinetic line 461