SplitIntegratedBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual integrated form bounds. The premises name only the published isolated-well and harmonic-oscillator spectral results.

theorem OAI.ContinuumCoulomb.splitPlanarForm_projection_lower line 13
theorem OAI.ContinuumCoulomb.splitVerticalForm_projection_lower line 41

theorem OAI.ContinuumCoulomb.split_test_spectral_lower line 68

Source documentation

Conditional on the two precisely stated published spectral inputs, this is a finite-rank lower bound for the actual split-coordinate Schrödinger form.

theorem split_test_spectral_lower
    (hp : PlanarSobolev.ManufacturedPlanarGroundGap)
    (hv : PublishedVerticalOscillatorGap) :
    ∃ γ : ℝ, 0 < γ ∧ γ ≤ 1/4 ∧ ∀ (m : ℕ) (D η freq S : ℝ),
      8 ≤ D → 0 < η → 0 < freq → 0 < S → 3*freq/2 ≤ freq^2*S^2/8 →
      ∀ u : Fin m → PlanarPosition, (∀ i j, i ≠ j → D ≤ ‖u i-u j‖) →
      γ*(1+η)*(1+m*localizedOverlapBound D) ≤ freq*(1+η) →
      ∀ f : SplitPosition → ℝ, ContDiff ℝ 1 f → HasCompactSupport f →
      (((-1/2:ℝ)+γ-planarSiteDerivativeBound D^2-
        γ*(1+η⁻¹)*m*planarSiteTailConstant*Real.exp (-(19/20:ℝ)*(D/8))) +
        (3*freq/2-verticalCutoffDerivativeBound S^2/2-
          freq*(1+η⁻¹)*verticalCutoffTailConstant freq*Real.exp (-freq*S^2/8)) -
…

Mentions: OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap, OAI.ContinuumCoulomb.PublishedVerticalOscillatorGap, OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.localizedOverlapBound, OAI.ContinuumCoulomb.SplitPosition, OAI.ContinuumCoulomb.planarSiteDerivativeBound, OAI.ContinuumCoulomb.planarSiteTailConstant, OAI.ContinuumCoulomb.verticalCutoffDerivativeBound, OAI.ContinuumCoulomb.verticalCutoffTailConstant