OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/VerticalOscillatorGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Discharge of the published transverse-oscillator input. The normalized Gaussian Poincare inequality and an exact compact-support integration by parts give precisely the projection inequality used by the continuum reduction.

  1. theorem OAI.ContinuumCoulomb.vertical_quotient_deriv line 15
  2. theorem OAI.ContinuumCoulomb.publishedVerticalOscillatorGap line 26

    Source documentation

    The exact harmonic-oscillator projection inequality.

    theorem publishedVerticalOscillatorGap : PublishedVerticalOscillatorGap := by
…

    Mentions: OAI.ContinuumCoulomb.PublishedVerticalOscillatorGap