OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/OrbitalCutoffTail.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Quantitative Sobolev tails of the localized orbitals. The 24th moments give a twelfth-power decay in the H1 norm of the removed tail.

  1. theorem OAI.ContinuumCoulomb.orbitalCutoff_fderiv_zero line 14
  2. theorem OAI.ContinuumCoulomb.localized_weighted_coefficient_tail line 22
  3. theorem OAI.ContinuumCoulomb.continuumLocalizedMode_centered_twentyFourth_moment_integrable line 52
  4. theorem OAI.ContinuumCoulomb.centered_deriv_moment line 57
  5. theorem OAI.ContinuumCoulomb.orbitalCutoff_value_tail line 62
  6. theorem OAI.ContinuumCoulomb.orbitalCutoff_deriv_tail line 76
  7. theorem OAI.ContinuumCoulomb.orbitalCutoff_deriv_remainder_tail line 99
  8. def OAI.ContinuumCoulomb.orbitalRemainder line 115
  9. theorem OAI.ContinuumCoulomb.orbitalRemainder_C1 line 118
  10. theorem OAI.ContinuumCoulomb.orbitalRemainder_deriv line 123
  11. theorem OAI.ContinuumCoulomb.orbitalRemainder_deriv_tail line 136
  12. theorem OAI.ContinuumCoulomb.orbitalRemainder_memLp line 171
  13. theorem OAI.ContinuumCoulomb.orbitalRemainder_deriv_memLp line 176