OAI/Analysis/CoulombRadii/FieldAnalysis/Space.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Coulomb.Space line 12

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:125 (same declaration text).

  2. abbrev OAI.Coulomb.Configuration line 13

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:126 (same declaration text).

  3. abbrev OAI.Coulomb.Spins line 14

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:127 (same declaration text).

  4. structure OAI.Coulomb.Nuclei line 16

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:129 (same declaration text).

  5. def OAI.Coulomb.totalCharge line 23
  6. def OAI.Coulomb.position line 25

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:136 (same declaration text).

  7. def OAI.Coulomb.coulombKernel line 28

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:139 (same declaration text).

  8. def OAI.Coulomb.attraction line 30

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:141 (same declaration text).

  9. def OAI.Coulomb.permute line 33

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:144 (same declaration text).

  10. structure OAI.Coulomb.H1Vector line 37

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:148 (same declaration text).

  11. def OAI.Coulomb.Antisymmetric line 47

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:158 (same declaration text).

  12. def OAI.Coulomb.mass line 52

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:163 (same declaration text).

  13. def OAI.Coulomb.kinetic line 55

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:166 (same declaration text).

  14. def OAI.Coulomb.nuclearEnergy line 58

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:169 (same declaration text).

  15. def OAI.Coulomb.pairEnergy line 61

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:172 (same declaration text).

  16. def OAI.Coulomb.form line 66

    Also declared: ComparatorChallenges/ContinuumCoulombHardness.lean:177 (same declaration text).

  17. def OAI.Coulomb.energy line 69
  18. def OAI.Coulomb.GroundState line 73
  19. def OAI.Coulomb.atom line 76
  20. def OAI.Coulomb.exteriorMass line 83
  21. def OAI.Coulomb.outerRadius line 87
  22. theorem OAI.Coulomb.bounded_quadratic_bootstrap line 90
  23. theorem OAI.Coulomb.geometric_quadratic_bootstrap line 112
  24. theorem OAI.Coulomb.memLp_two_real_mul line 147
  25. def OAI.Coulomb.H1Vector.smoothMul line 157
  26. theorem OAI.Coulomb.H1Vector.smoothMul_antisymmetric line 212
  27. lemma OAI.Coulomb.norm_real_mul_sq line 224
  28. lemma OAI.Coulomb.norm_real_mul_add_sq line 229
  29. theorem OAI.Coulomb.quadratic_partition_derivative line 237
  30. theorem OAI.Coulomb.ims_pointwise line 260
  31. theorem OAI.Coulomb.mass_smooth_partition line 279
  32. theorem OAI.Coulomb.kinetic_smooth_partition line 303
  33. structure OAI.Coulomb.HardyCoordinates line 358
  34. def OAI.Coulomb.blockRadiusSq line 364
  35. lemma OAI.Coulomb.blockRadiusSq_nonneg line 367
  36. lemma OAI.Coulomb.contDiff_blockRadiusSq line 370
  37. lemma OAI.Coulomb.fderiv_blockRadiusSq line 376