OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedMomentTail.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Translated fourth/eighth moments and the weighted tails used in the finite-slab operator estimate.

  1. def OAI.ContinuumCoulomb.localizedDensityMoment line 12
  2. theorem OAI.ContinuumCoulomb.localizedDensityMoment_nonnegative line 15
  3. theorem OAI.ContinuumCoulomb.translated_moment line 20
  4. theorem OAI.ContinuumCoulomb.localizedDensity_fourth_moment_translate line 58
  5. theorem OAI.ContinuumCoulomb.localizedDensity_eighth_moment_translate line 65
  6. theorem OAI.ContinuumCoulomb.localizedDensity_twentyFourth_moment_translate line 72
  7. theorem OAI.ContinuumCoulomb.localizedDensity_seventySecond_moment_translate line 79
  8. theorem OAI.ContinuumCoulomb.weighted_tail line 86
  9. theorem OAI.ContinuumCoulomb.localizedDensity_mass_tail_eighth line 106
  10. theorem OAI.ContinuumCoulomb.localizedDensity_fourth_tail_eighth line 114
  11. theorem OAI.ContinuumCoulomb.localizedDensity_mass_tail_twentyFourth line 121
  12. theorem OAI.ContinuumCoulomb.localizedDensity_fourth_tail_twentyFourth line 129
  13. theorem OAI.ContinuumCoulomb.localizedDensity_mass_tail_seventySecond line 136
  14. theorem OAI.ContinuumCoulomb.localizedDensity_fourth_tail_seventySecond line 144