MovingWells.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Motion of secondary nuclei in capped backgrounds

The cap depends only on the fixed primary centre. On its nonzero support every permitted secondary pole is at least D/32 away. Thus its motion has a uniform D⁻² potential bound, before any isolated eigenstate is chosen.

theorem OAI.ContinuumCoulomb.cappedSitePotential_displacement_bound line 18
theorem OAI.ContinuumCoulomb.backgroundPotential_displacement_bound line 64
theorem OAI.ContinuumCoulomb.singlePoleEnergy_position_bound line 88
theorem OAI.ContinuumCoulomb.backgroundEnergy_displacement_bound line 106

theorem OAI.ContinuumCoulomb.isolatedWellForm_displacement_bound line 140

Source documentation

Motion of the own pole costs a kinetic term; motion of all the other poles costs only the small bounded-background term.

theorem isolatedWellForm_displacement_bound {m : ℕ} {D q q' delta : ℝ}
    (hD : 128 ≤ D) (hq : 0 ≤ q) (hq1 : q ≤ 1) (hq' : 0 ≤ q') (hq'1 : q' ≤ 1)
    (hdelta : 0 ≤ delta) (center a b : Fin m → Position)
    (ha : ∀ j, ‖a j‖ ≤ 4) (hb : ∀ j, ‖b j‖ ≤ 4)
    (hmove : ∀ j, ‖a j - b j‖ ≤ delta) (site : Fin m) (state : Coulomb.H1Vector 1) :
    |isolatedWellForm D q q' center a site state -
      isolatedWellForm D q q' center b site state| ≤
      16 * q' * ‖a site - b site‖ * Coulomb.kinetic state +
        (2048 * q' * m / D ^ 2 * delta) * Coulomb.mass state := by
…

Mentions: OAI.ContinuumCoulomb.Position, OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.isolatedWellForm, OAI.Coulomb.kinetic, OAI.Coulomb.mass