leanprover-community/mathlib4

The Gaussian as a Schwartz function

Ouverte

#33 072 ouverte le 19 déc. 2025

Voir sur GitHubGuide contributeur
 (5 commentaires) (0 réaction) (0 personne assignée)Lean (1 592 forks)github user discovery
good first issuet-analysis

Métriques du dépôt

Stars
 (3 869 étoiles)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

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.

Guide contributeur

Direction de recherche
Étudiez les définitions existantes des fonctions de Schwartz dans mathlib4 et la fonction gaussienne pour les formes bilinéaires définies positives. Commencez par implémenter le cas unidimensionnel, puis généralisez. Consultez les fichiers et exemples connexes pour obtenir des conseils.
Stack technique
Aucun
Domaine
backend
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-3 heures
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Investigation requise
Prérequis
Lean
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
40