PhysicalOneElectronLower.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

A finite-rank lower bound for the manufactured one-electron Coulomb field, obtained from the planar and vertical spectral estimates.

def OAI.ContinuumCoulomb.planarSpectralLevel line 17
def OAI.ContinuumCoulomb.verticalSpectralLevel line 21
def OAI.ContinuumCoulomb.physicalSeparablePotential line 25
theorem OAI.ContinuumCoulomb.physicalSeparablePotential_continuous line 29
theorem OAI.ContinuumCoulomb.positionRealForm_mono_shift line 35
theorem OAI.ContinuumCoulomb.physicalSeparable_test_lower line 55

theorem OAI.ContinuumCoulomb.manufacturedSlab_test_lower line 87

Source documentation

The actual Coulomb slab and compact counterterm well field have the same lower bound, up to the proved finite-slab and counterterm errors.

theorem manufacturedSlab_test_lower
    (hp : PlanarSobolev.ManufacturedPlanarGroundGap)
    (hv : PublishedVerticalOscillatorGap) :
    ∃ γ : ℝ, 0 < γ ∧ γ ≤ 1/4 ∧ ∀ (m : ℕ) (D η freq S rho H scale δ : ℝ),
      8 ≤ D → 0 < η → 0 < freq → 0 < S → 0 ≤ rho → 0 < H → 0 ≤ scale → 0 ≤ δ →
      freq^2 = 4*Real.pi*rho → 3*freq/2 ≤ freq^2*S^2/8 →
      ∀ u : Fin m → PlanarPosition, (∀ i j, i ≠ j → D ≤ ‖u i-u j‖) →
      (∀ i, 0 ≤ localizedCounterterm freq u i/scale ∧ localizedCounterterm freq u i/scale ≤ δ) →
      γ*(1+η)*(1+m*localizedOverlapBound D) ≤ freq*(1+η) →
      ∀ f : Position → ℂ, ContDiff ℝ 1 f → HasCompactSupport f →
      (planarSpectralLevel γ m D η+verticalSpectralLevel freq S η-freq*(1+η)-
        (δ*PlanarSobolev.wellBound+6*Real.pi*rho*S^3/H))*(∫ x, ‖f x‖^2) -
…

Mentions: OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap, OAI.ContinuumCoulomb.PublishedVerticalOscillatorGap, OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.localizedCounterterm, OAI.ContinuumCoulomb.localizedOverlapBound, OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.planarSpectralLevel, OAI.ContinuumCoulomb.verticalSpectralLevel, OAI.ContinuumCoulomb.PlanarSobolev.wellBound