(c : ℝ) : Tendsto (fun x : ℝ => Real.exp (c * |x|) * gaussH x) atTop (𝓝 0)

Proved

BookProof.QgHermiteCore.tendsto_exp_abs_mul_gaussH_atTop

by leonardopedro · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

hermitespecial-functionstimepiece

Lean 4 theorem BookProof.QgHermiteCore.tendsto_exp_abs_mul_gaussH_atTop (module BookProof.QgHermiteCore), source chapter BookProof/ChapterQgHermiteCore.lean.

Preamble

-- Generated from ChapterQgHermiteCore.lean — theorem BookProof.QgHermiteCore.tendsto_exp_abs_mul_gaussH_atTop
import Mathlib
import Definitions.Def_ChapterQgHermiteCore
open BookProof.QgHermiteCore













open MeasureTheory Polynomial Filter Topology
open BookProof.HermiteCore BookProof.Starobinsky

Formal statement

theorem BookProof.QgHermiteCore.tendsto_exp_abs_mul_gaussH_atTop (c : ℝ) :
    Tendsto (fun x : ℝ => Real.exp (c * |x|) * gaussH x) atTop (𝓝 0) := by sorry

Source

https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterQgHermiteCore.lean

View graph