leanprover-community/mathlib4

The Gaussian as a Schwartz function

オープン

#33,072 opened on 2025/12/19

GitHub で見るコントリビューターガイド
 (5 件のコメント) (0 件のリアクション) (0 人の担当者)Lean (1,381 件のフォーク)github user discovery
good first issuet-analysis

Repository metrics

Stars
 (3,405 個のスター)
PR merge metrics
 (30d に merged PR はありません)

説明

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.

コントリビューターガイド

調査方針
mathlib4 にある既存の Schwartz 関数の定義と正定値双線形形式のガウス関数を調べてください。最初に1次元の場合を実装し、その後一般化します。関連するファイルや例を参考にしてください。
技術スタック
なし
領域
backend
Issue 種別
機能
難度新しい貢献者にとっての実装難度です。1 は非常に小さな変更、5 は専門的な作業です。
3
推定時間経験ある貢献者が調査、実装、テスト、pull request 準備にかけるおおよその時間範囲です。
1-3時間
活動状況Issue が今どれだけ取り組みやすいかを示します。新しい、活発、古い、ブロック中、またはメンテナー入力待ちなどです。
アクティブ
明確さ期待される変更、受け入れ条件、次の手順がどれだけ明確かを示します。
調査が必要
前提条件
Lean
初心者向け度初回貢献者にどれだけ取り組みやすいかを 1-100 で推定したスコアです。
40