leanprover-community/mathlib4

The Gaussian as a Schwartz function

Aperta

#33.072 aperta il 19 dic 2025

Vedi su GitHubGuida contributor
 (5 commenti) (0 reazioni) (0 assegnatari)Lean (1592 fork)github user discovery
good first issuet-analysis

Metriche repository

Star
 (3869 stelle)
Metriche merge PR
 (Nessuna PR mergiata in 30 g)

Descrizione

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.

Guida contributor

Direzione di ricerca
Studia le definizioni esistenti di funzioni di Schwartz in mathlib4 e la funzione gaussiana per forme bilineari definite positive. Inizia implementando il caso unidimensionale, poi generalizza. Guarda i file correlati e gli esempi per indicazioni.
Tech stack
Nessuno
Dominio
backend
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-3 ore
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Richiede indagine
Prerequisiti
Lean
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
40