OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/VerticalCappedGap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The capped transverse oscillator inherits the published oscillator projection bound, with a proved IMS cost and a proved Gaussian cutoff error.

  1. theorem OAI.ContinuumCoulomb.verticalCutoff_mass line 12
  2. theorem OAI.ContinuumCoulomb.verticalCappedForm_outer_lower line 31
  3. theorem OAI.ContinuumCoulomb.verticalCappedForm_projection_lower line 66

    Source documentation

    The only input is the published harmonic-oscillator gap. The slab cutoff, exterior barrier and localization cost are explicit actual functions.

    theorem verticalCappedForm_projection_lower (hpublished : PublishedVerticalOscillatorGap)
    {freq S : ℝ} (hfreq : 0 < freq) (hS : 0 < S)
    (hbarrier : 3*freq/2 ≤ freq^2*S^2/8)
    (u : ℝ → ℝ) (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) :
    (3*freq/2) * (∫ z, u z^2) -
      freq * (∫ z, (verticalInnerCutoff S z*u z)*verticalMode freq z)^2 -
      (verticalCutoffDerivativeBound S^2/2) * (∫ z, u z^2) ≤
      verticalCappedForm freq S u := by
…

    Mentions: OAI.ContinuumCoulomb.PublishedVerticalOscillatorGap, OAI.ContinuumCoulomb.verticalInnerCutoff, OAI.ContinuumCoulomb.verticalMode, OAI.ContinuumCoulomb.verticalCutoffDerivativeBound, OAI.ContinuumCoulomb.verticalCappedForm

  4. theorem OAI.ContinuumCoulomb.vertical_add_sq_le line 99
  5. theorem OAI.ContinuumCoulomb.verticalCutoff_pair_bound line 109
  6. theorem OAI.ContinuumCoulomb.verticalCappedForm_global_projection_lower line 125

    Source documentation

    The capped form has a global finite-rank lower bound. Unlike the orthogonality corollary, this bound passes directly through approximation.

    theorem verticalCappedForm_global_projection_lower
    (hpublished : PublishedVerticalOscillatorGap)
    {freq S η : ℝ} (hfreq : 0 < freq) (hS : 0 < S) (hη : 0 < η)
    (hbarrier : 3*freq/2 ≤ freq^2*S^2/8)
    (u : ℝ → ℝ) (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u) :
    (3*freq/2 - verticalCutoffDerivativeBound S^2/2 -
      freq*(1+η⁻¹)*verticalCutoffTailConstant freq*Real.exp (-freq*S^2/8)) *
      (∫ z, u z^2) - freq*(1+η)*(∫ z, u z*verticalMode freq z)^2 ≤
        verticalCappedForm freq S u := by
…

    Mentions: OAI.ContinuumCoulomb.PublishedVerticalOscillatorGap, OAI.ContinuumCoulomb.verticalCutoffDerivativeBound, OAI.ContinuumCoulomb.verticalCutoffTailConstant, OAI.ContinuumCoulomb.verticalMode, OAI.ContinuumCoulomb.verticalCappedForm

  7. theorem OAI.ContinuumCoulomb.verticalCappedForm_complement_lower line 142

    Source documentation

    Orthogonality is to the actual uncut Gaussian; its cutoff error is accounted for quantitatively rather than inserted as a spectral premise.

    theorem verticalCappedForm_complement_lower (hpublished : PublishedVerticalOscillatorGap)
    {freq S : ℝ} (hfreq : 0 < freq) (hS : 0 < S)
    (hbarrier : 3*freq/2 ≤ freq^2*S^2/8)
    (u : ℝ → ℝ) (hu : ContDiff ℝ 1 u) (hc : HasCompactSupport u)
    (ho : (∫ z, u z*verticalMode freq z) = 0) :
    (3*freq/2 - verticalCutoffDerivativeBound S^2/2 -
      freq*verticalCutoffTailConstant freq*Real.exp (-freq*S^2/8)) * (∫ z, u z^2) ≤
      verticalCappedForm freq S u := by
…

    Mentions: OAI.ContinuumCoulomb.PublishedVerticalOscillatorGap, OAI.ContinuumCoulomb.verticalMode, OAI.ContinuumCoulomb.verticalCutoffDerivativeBound, OAI.ContinuumCoulomb.verticalCutoffTailConstant, OAI.ContinuumCoulomb.verticalCappedForm