Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

bibkey: loges2026gaussianschwartz authors: Gregory J. Loges year: 2026 title: Gaussians in inner product spaces as Schwartz maps doi: null url: https://github.com/HEPLean/PhysLean/blob/b9043cc548ef6d63a28454cf3a57fb12a0c2e142/Physlib/Mathematics/InnerProductSpace/Gaussian.lean claim: The standard real Gaussian is a Schwartz map on every real inner product space. strata_touched:

  • D5/S3/Quantum/Analysis/GaussianSchwartz license: Apache-2.0 triage: anchor

Gaussian Schwartz construction

Verified locator

https://github.com/HEPLean/PhysLean/blob/b9043cc548ef6d63a28454cf3a57fb12a0c2e142/Physlib/Mathematics/InnerProductSpace/Gaussian.lean

Gregory J. Loges, HEPLean/PhysLean, revision b9043cc548ef6d63a28454cf3a57fb12a0c2e142, Physlib/Mathematics/InnerProductSpace/Gaussian.lean. The selected original construction is realStdGaussian, together with its higher-derivative and exponential-decay estimates. The full Apache-2.0 license is in docs/reports/oscillator-suppliers/physlib-LICENSE.txt. The authenticated donor tree has no NOTICE-named file.

The receiving construction makes the two estimates local in one existence proof. The donor copyright and grant header are preserved verbatim. No originality is claimed for this construction. At this repository’s own Mathlib pin, an equivalent directly applicable Gaussian Schwartz constructor supersedes this source recovery when its analytic consumers validate against it.