OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/CorrectedOneElectronProjection.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The corrected orbital span lies in the actual one-electron weak-H1 domain, with arbitrary complex coefficients in each spin component.

  1. def OAI.ContinuumCoulomb.correctedOneElectronValue line 14
  2. theorem OAI.ContinuumCoulomb.lifted_corrected_mode_C1 line 18
  3. theorem OAI.ContinuumCoulomb.lifted_corrected_mode_partial line 25
  4. theorem OAI.ContinuumCoulomb.correctedOneElectronValue_C1 line 41
  5. theorem OAI.ContinuumCoulomb.correctedOneElectronValue_memLp line 46
  6. theorem OAI.ContinuumCoulomb.correctedOneElectronValue_partial line 53
  7. theorem OAI.ContinuumCoulomb.correctedOneElectronValue_partial_memLp line 65
  8. def OAI.ContinuumCoulomb.correctedOneElectronState line 78
  9. theorem OAI.ContinuumCoulomb.correctedOneElectronOrbital_orthonormal line 83
  10. theorem OAI.ContinuumCoulomb.correctedOneElectronState_coordinate line 113
  11. def OAI.ContinuumCoulomb.correctedOneElectronCoefficients line 143
  12. def OAI.ContinuumCoulomb.correctedOneElectronProjection line 149
  13. def OAI.ContinuumCoulomb.correctedOneElectronRemainder line 153
  14. theorem OAI.ContinuumCoulomb.correctedOneElectronRemainder_coordinate line 157
  15. theorem OAI.ContinuumCoulomb.correctedOneElectronRemainder_orthogonal line 184
  16. theorem OAI.ContinuumCoulomb.orthonormal_combination_norm line 196
  17. theorem OAI.ContinuumCoulomb.correctedOneElectronState_mass line 211
  18. theorem OAI.ContinuumCoulomb.correctedOneElectronProjection_mass line 222
  19. theorem OAI.ContinuumCoulomb.correctedOneElectron_mass_decomposition line 230