OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/GaussianPoincare.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

One-dimensional Gaussian Poincare inequality derived from the Brascamp–Lieb theorem. This is the spectral input needed for the transverse oscillator; no spectral assertion is assumed here.

  1. def OAI.ContinuumCoulomb.gaussianPotential line 16
  2. theorem OAI.ContinuumCoulomb.gaussianPotential_derivative line 18
  3. theorem OAI.ContinuumCoulomb.gaussianPotential_hessian line 29
  4. theorem OAI.ContinuumCoulomb.gaussianPotential_regular line 36
  5. theorem OAI.ContinuumCoulomb.gaussianPotential_integrable line 44
  6. theorem OAI.ContinuumCoulomb.gaussian_weight_integrable line 53
  7. theorem OAI.ContinuumCoulomb.gaussian_poincare_test line 59

    Source documentation

    Gaussian variance is bounded by its Dirichlet form with the exact oscillator gap constant.

    theorem gaussian_poincare_test {freq : ℝ} (hf : 0 < freq)
    (f : Space 1 → ℝ) (hs : ContDiff ℝ ∞ f) (hc : HasCompactSupport f) :
    (2*freq)*variance (potentialMeasure (fun x : Space 1 => freq*‖x‖^2)) f ≤
      dirichletEnergy (potentialMeasure (fun x : Space 1 => freq*‖x‖^2)) f :=
…