OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/VerticalCappedScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed slab width threshold makes both actual transverse cutoff losses smaller than half the oscillator gap.

  1. theorem OAI.ContinuumCoulomb.verticalCutoffDerivativeBound_tendsto line 13
  2. theorem OAI.ContinuumCoulomb.verticalCutoffLoss_tendsto line 20
  3. theorem OAI.ContinuumCoulomb.verticalCappedForm_uniform_complement_gap line 35

    Source documentation

    The actual capped oscillator keeps a fixed positive excitation gap for every sufficiently wide slab, uniformly over compact C1 tests.

    theorem verticalCappedForm_uniform_complement_gap
    (hpublished : PublishedVerticalOscillatorGap) {freq : ℝ} (hfreq : 0 < freq) :
    ∃ R : ℝ, 1 ≤ R ∧ ∀ S : ℝ, R ≤ S → ∀ u : ℝ → ℝ,
      ContDiff ℝ 1 u → HasCompactSupport u →
      (∫ z, u z*verticalMode freq z) = 0 →
      freq*(∫ z, u z^2) ≤ verticalCappedForm freq S u := by
…

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