OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/LocalizedTransition.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual transition densities of localized three-dimensional modes have normalized mass bounds and exponentially small off-site L1 mass.

  1. def OAI.ContinuumCoulomb.localizedTransition line 13
  2. theorem OAI.ContinuumCoulomb.localizedTransition_continuous line 16
  3. theorem OAI.ContinuumCoulomb.localizedTransition_nonnegative line 20
  4. theorem OAI.ContinuumCoulomb.localizedTransition_integrable line 24
  5. theorem OAI.ContinuumCoulomb.localizedTransition_bound line 28
  6. theorem OAI.ContinuumCoulomb.localizedTransition_mass line 35
  7. theorem OAI.ContinuumCoulomb.localizedTransition_mass_le_one line 51
  8. theorem OAI.ContinuumCoulomb.localizedTransition_norm_mass line 63
  9. theorem OAI.ContinuumCoulomb.localizedTransition_L1_decay line 68
  10. def OAI.ContinuumCoulomb.localizedTransitionPacket line 74