OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/IsolatedPerturbation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual isolated-well perturbation on weak H¹ states

The difference from a unit hydrogen centre is the small change of primary charge, the weak secondary Coulomb pole, and the bounded capped background. No isolated eigenfunction or perturbative spectral conclusion is assumed.

  1. theorem OAI.ContinuumCoulomb.nuclear_mul_memLp line 19
  2. def OAI.ContinuumCoulomb.isolatedPerturbation line 34
  3. theorem OAI.ContinuumCoulomb.background_mul_memLp line 40
  4. theorem OAI.ContinuumCoulomb.isolatedPerturbation_mul_memLp line 55
  5. theorem OAI.ContinuumCoulomb.norm_sub_sub_sq_le line 73
  6. theorem OAI.ContinuumCoulomb.isolatedPerturbation_spin_norm_bound line 81
  7. theorem OAI.ContinuumCoulomb.isolatedPerturbation_norm_bound line 166

    Source documentation

    The operator estimate for an arbitrary one-electron spinful weak-H¹ state.

    theorem isolatedPerturbation_norm_bound {m : ℕ} {D q q' : ℝ} (hD : 128 ≤ D)
    (hq : 0 ≤ q) (hq1 : q ≤ 1) (hq' : 0 ≤ q') (hq'1 : q' ≤ 1)
    (center displacement : Fin m → Position) (hdisp : ∀ j, ‖displacement j‖ ≤ 4)
    (site : Fin m) (state : Coulomb.H1Vector 1) :
    (∑ spin, ∫ x, ‖(isolatedPerturbation D q q' center displacement site
      (Coulomb.position x 0) : ℂ) * state.value spin x‖ ^ 2) ≤
      24 * ((1 - q) ^ 2 + q' ^ 2) * Coulomb.kinetic state +
        3 * (48 * m / D) ^ 2 * Coulomb.mass state := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.Coulomb.H1Vector, OAI.ContinuumCoulomb.isolatedPerturbation, OAI.Coulomb.position, OAI.Coulomb.kinetic, OAI.Coulomb.mass

  8. theorem OAI.ContinuumCoulomb.isolatedPerturbation_small_norm_bound line 182