OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/PlanarWellBottom.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact variational bottom of the manufactured planar well on its closed Sobolev graph. This is an analytic component of the continuum construction; it does not assert the hardness reduction.

  1. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_mass line 20
  2. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_kinetic line 30
  3. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_form line 44
  4. theorem OAI.ContinuumCoulomb.PlanarSobolev.form_smul line 59
  5. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_energy line 66
  6. theorem OAI.ContinuumCoulomb.PlanarSobolev.mode_mass_positive line 70
  7. def OAI.ContinuumCoulomb.PlanarSobolev.normalizedMode line 74
  8. theorem OAI.ContinuumCoulomb.PlanarSobolev.normalizedMode_mass line 76
  9. theorem OAI.ContinuumCoulomb.PlanarSobolev.normalizedMode_energy line 81
  10. def OAI.ContinuumCoulomb.PlanarSobolev.groundEnergy line 88
  11. theorem OAI.ContinuumCoulomb.PlanarSobolev.groundEnergy_eq line 92

    Source documentation

    Exact manufactured-well bottom, proved without a published spectral input.

    theorem groundEnergy_eq : groundEnergy = ((-1 / 2 : ℝ) : EReal) := by
…

    Mentions: OAI.ContinuumCoulomb.PlanarSobolev.groundEnergy