GaussianScalar.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Normalized Gaussian variance and energy on the real line.

theorem OAI.ContinuumCoulomb.gaussianLine_expectation line 13

theorem OAI.ContinuumCoulomb.gaussian_scalar_poincare_smooth line 38

Source documentation

The exact weighted Poincare constant for compact smooth real functions.

theorem gaussian_scalar_poincare_smooth {freq : ℝ} (hf : 0 < freq)
    (f : ℝ → ℝ) (hs : ContDiff ℝ ∞ f) (hc : HasCompactSupport f) :
    (2*freq)*((∫ z : ℝ, verticalMode freq z^2*f z^2) -
      (∫ z : ℝ, verticalMode freq z^2*f z)^2) ≤
        ∫ z : ℝ, verticalMode freq z^2*(deriv f z)^2 := by
…

Mentions: OAI.ContinuumCoulomb.verticalMode