leanprover-community/mathlib4

The Gaussian as a Schwartz function

Open

#33,072 opened on Dec 19, 2025

View on GitHub
 (5 comments) (0 reactions) (0 assignees)Lean (1,381 forks)github user discovery
good first issuet-analysis

Repository metrics

Stars
 (3,405 stars)
PR merge metrics
 (No merged PRs in 30d)

Description

Define the Gaussian (for an arbitrary positive definite bilinear form) as a Schwartz function. It might be necessary to do the 1-d case first and then do the general case as a second step.

Contributor guide

Research direction
Study the existing Schwartz function definitions in mathlib4 and the Gaussian function for positive definite bilinear forms. Start by implementing the 1 dimensional case, then generalize. Look at related files and examples for guidance.
Tech stack
None
Domain
backend
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-3 hours
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Needs investigation
Prerequisites
Lean
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
40