OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/ClockPathBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Elementary quantitative propagation estimates for the finite clock. They compare every clock slice to its initial slice.

  1. def OAI.ContinuumCoulomb.clockPathEnergy line 13
  2. theorem OAI.ContinuumCoulomb.clockPathEnergy_nonneg line 16
  3. theorem OAI.ContinuumCoulomb.clock_path_anchor_bound line 20
  4. theorem OAI.ContinuumCoulomb.clock_path_mass_bound line 39