IsolatedForms.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Isolated-well energy forms on the actual weak H¹ domain

The perturbation bounds here concern the full one-electron form, including both Coulomb poles and the capped background. They give the shifted relative form comparison used before constructing isolated eigenfunctions.

def OAI.ContinuumCoulomb.singlePoleEnergy line 18
def OAI.ContinuumCoulomb.hydrogenForm line 22
def OAI.ContinuumCoulomb.backgroundEnergy line 25
def OAI.ContinuumCoulomb.isolatedWellForm line 30
theorem OAI.ContinuumCoulomb.singlePoleEnergy_nonneg line 36
theorem OAI.ContinuumCoulomb.singlePoleEnergy_bound line 42
theorem OAI.ContinuumCoulomb.hydrogenForm_coercive line 53
theorem OAI.ContinuumCoulomb.background_energy_integrable line 60
theorem OAI.ContinuumCoulomb.backgroundEnergy_bounds line 81
theorem OAI.ContinuumCoulomb.isolatedWellForm_coercive line 105
theorem OAI.ContinuumCoulomb.isolatedWellForm_difference line 123
theorem OAI.ContinuumCoulomb.isolatedWellForm_small_difference line 177

theorem OAI.ContinuumCoulomb.isolatedWellForm_relative line 222

Source documentation

The actual isolated well is a small relative perturbation of the shifted hydrogen form. This holds on every spinful weak-H¹ state.

theorem isolatedWellForm_relative {m : ℕ} {D q q' epsilon : ℝ}
    (hD : 128 ≤ D) (hq : 0 ≤ q) (hq1 : q ≤ 1) (hq' : 0 ≤ q') (hq'1 : q' ≤ 1)
    (hprimary : |1 - q| ≤ epsilon) (hsecondary : q' ≤ epsilon)
    (hbackground : 48 * m / D ≤ epsilon)
    (center displacement : Fin m → Position) (hdisp : ∀ j, ‖displacement j‖ ≤ 4)
    (site : Fin m) (state : Coulomb.H1Vector 1) :
    |isolatedWellForm D q q' center displacement site state - hydrogenForm (center site) state| ≤
      10 * epsilon * (hydrogenForm (center site) state + 5 * Coulomb.mass state) := by
…

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